TileStructure.Forest.thin_scale_impact_prelims

lemma thin_scale_impact_prelims (hu₁ : u₁ ∈ t) (hJ : J ∈ 𝓙₆ t u₁)    (hd : ¬Disjoint (ball (𝔠 p) (8 * D ^ 𝔰 p)) (ball (c J) (8 * D ^ s J)))    (h : s J - C7_6_3 a n < 𝔰 p) :    dist (𝔠 p) (c J) < 16 * D ^ (𝔰 p + C7_6_3 a n + 2) ∧    ∃ J', J < J' ∧ s J' = s J + 1 ∧      ∃ p ∈ t u₁, ↑(𝓘 p) ⊆ ball (c J') (100 * D ^ (s J' + 1)) := by  have b1 : dist (𝔠 p) (c J) < 16 * D ^ (𝔰 p + C7_6_3 a n + 2) := by    calc      _ < 8 * (D : ℝ) ^ 𝔰 p + 8 * D ^ s J := dist_lt_of_not_disjoint_ball hd      _ ≤ 8 * D ^ (𝔰 p + C7_6_3 a n + 2) + 8 * D ^ (𝔰 p + C7_6_3 a n + 2) := by        simp_rw [← Real.rpow_intCast]; gcongr (8 : ℝ) * D ^ ?_ + 8 * D ^ ?_        · exact one_le_realD _        · rw [add_assoc, le_add_iff_nonneg_right]; exact nonneg_C7_6_3_add_two        · exact one_le_realD _        · linarith      _ ≤ _ := by rw [← two_mul, ← mul_assoc]; norm_num  obtain ⟨q, mq⟩ := t.nonempty hu₁  have qlt : 𝓘 q < 𝓘 u₁ := lt_of_le_of_ne (t.smul_four_le hu₁ mq).1 (t.𝓘_ne_𝓘 hu₁ mq)  have u₁nm : 𝓘 u₁ ∉ 𝓙₆ t u₁ := by    simp_rw [𝓙₆, mem_inter_iff, mem_Iic, le_rfl, and_true, 𝓙, mem_setOf, Maximal, not_and_or]; left    rw [𝓙₀, mem_setOf]; push Not; rw [Grid.lt_def] at qlt    refine ⟨(scale_mem_Icc.1.trans_lt qlt.2).ne',      ⟨q, mq, qlt.1.trans <| Grid_subset_ball.trans <| ball_subset_ball ?_⟩⟩    change 4 * (D : ℝ) ^ (𝔰 u₁) ≤ 100 * D ^ (𝔰 u₁ + 1); gcongr    exacts [by norm_num, one_le_realD _, by lia]  have Jlt : J < 𝓘 u₁ := by apply lt_of_le_of_ne hJ.2; by_contra hh; subst hh; exact u₁nm hJ  rw [Grid.lt_def] at Jlt; obtain ⟨J', lJ', sJ'⟩ := Grid.exists_scale_succ Jlt.2  replace lJ' : J < J' := Grid.lt_def.mpr ⟨lJ'.1, by lia⟩  have J'nm : J' ∉ 𝓙₀ (t u₁) := by    by_contra hh; apply absurd hJ.1.2; push Not; use J', hh, lJ'.le, not_le_of_gt lJ'  rw [𝓙₀, mem_setOf] at J'nm; push Not at J'nm; obtain ⟨p', mp', sp'⟩ := J'nm.2  exact ⟨b1, ⟨J', lJ', sJ', ⟨p', mp', sp'⟩⟩⟩