forest_inner

lemma forest_inner (hu : u ∈ 𝔘₃ k n j) (hp : p ∈ 𝔗₂ k n j u) :    ball (𝔠 p) (8 * D ^ 𝔰 p) ⊆ 𝓘 u := by  have p₄ := (𝔗₂_subset_ℭ₆.trans ℭ₆_subset_ℭ₅ |>.trans ℭ₅_subset_ℭ₄) hp  have p₁ := (ℭ₄_subset_ℭ₃.trans ℭ₃_subset_ℭ₂ |>.trans ℭ₂_subset_ℭ₁) p₄  obtain ⟨q, mq, lq, sq⟩ := exists_le_add_scale_of_mem_layersBelow p₄  obtain ⟨-, u'', mu'', nu'', sl⟩ := ℭ₃_def.mp (maxLayer_subset mq)  replace nu'' : 𝓘 q < 𝓘 u'' := lt_of_le_of_ne sl.1 nu''  have s2 : smul 2 p ≤ smul 2 q := wiggle_order_11_10 lq (C5_3_3_le (X := X).trans (by norm_num))  have s2' : smul 2 p ≤ smul 1 u'' := s2.trans sl  have s10 : smul 10 p ≤ smul 1 u'' := smul_mono s2' le_rfl (by norm_num)  simp_rw [𝔗₂, mem_inter_iff, mem_iUnion₂, mem_iUnion] at hp  obtain ⟨p₆, u', mu', ru', pu'⟩ := hp  have ur : URel k n j u' u'' := Or.inr ⟨p, pu', s10⟩  have hu'' : u'' ∈ 𝔘₂ k n j := by    rw [𝔘₂, mem_setOf, not_disjoint_iff]    exact ⟨mu'', ⟨p, ⟨p₁, (lq.1.trans_lt nu'').ne, s2'⟩, p₆⟩⟩  have ru'' : URel k n j u u'' := equivalenceOn_urel.trans (𝔘₃_subset_𝔘₂ hu) mu' hu'' ru' ur  have qlu : 𝓘 q < 𝓘 u := URel.eq (𝔘₃_subset_𝔘₂ hu) hu'' ru'' ▸ nu''  have squ : 𝔰 q < 𝔰 u := (Grid.lt_def.mp qlu).2  have spu : 𝔰 p ≤ 𝔰 u - (Z * (n + 1) : ℕ) - 1 := by lia  have ⟨I, sI, plI, Ilu⟩ : ∃ I, s I = 𝔰 u - (Z * (n + 1) : ℕ) - 1 ∧ 𝓘 p ≤ I ∧ I ≤ 𝓘 u := by    apply Grid.exists_sandwiched (lq.1.trans qlu.le) (𝔰 u - (Z * (n + 1) : ℕ) - 1)    refine ⟨spu, ?_⟩    change _ ≤ 𝔰 u    lia  have bI : I ∉ 𝓛 n u := by    have p₅ := ℭ₆_subset_ℭ₅ p₆    rw [ℭ₅_def] at p₅; replace p₅ := p₅.2; contrapose! p₅    use u, (𝔘₃_subset_𝔘₂.trans 𝔘₂_subset_𝔘₁) hu, plI.1.trans (subset_biUnion_of_mem p₅)  rw [𝓛, mem_setOf, not_and] at bI; specialize bI Ilu  rw [not_and, not_not] at bI; specialize bI (by lia); rw [← sI] at spu  rcases spu.eq_or_lt with h | h  · have hI : 𝓘 p = I := by      apply eq_of_le_of_not_lt plI; rw [Grid.lt_def, not_and_or, not_lt]; exact Or.inr h.symm.le    rwa [← hI] at bI  · apply subset_trans (ball_subset_ball' _) bI    have ds : c (𝓘 p) ∈ ball (c I) (4 * D ^ s I) := (plI.1.trans Grid_subset_ball) Grid.c_mem_Grid    rw [mem_ball] at ds    calc      _ ≤ 4 * D * (D : ℝ) ^ 𝔰 p + 4 * D ^ s I := by        gcongr        · linarith [four_le_realD X]        · exact ds.le      _ = 4 * D ^ (𝔰 p + 1) + 4 * D ^ s I := by        rw [mul_assoc]; congr; rw [mul_comm, ← zpow_add_one₀ (realD_pos _).ne']      _ ≤ 4 * D ^ s I + 4 * D ^ s I := by        gcongr        · exact one_le_realD a        · lia      _ = _ := by ring