forest_separation

lemma forest_separation (hu : u ∈ 𝔘₃ k n j) (hu' : u' ∈ 𝔘₃ k n j) (huu' : u ≠ u')    (hp : p ∈ 𝔗₂ k n j u') (h : 𝓘 p ≤ 𝓘 u) : 2 ^ (Z * (n + 1)) < dist_(p) (𝒬 p) (𝒬 u) := by  simp_rw [𝔗₂, mem_inter_iff, mem_iUnion₂, mem_iUnion] at hp  obtain ⟨mp₆, v, mv, rv, ⟨-, np, sl⟩⟩ := hp  obtain ⟨p', mp', lp', sp'⟩ := exists_scale_add_le_of_mem_layersAbove <|    (ℭ₆_subset_ℭ₅ |>.trans ℭ₅_subset_ℭ₄ |>.trans ℭ₄_subset_ℭ₃ |>.trans ℭ₃_subset_ℭ₂) mp₆  have np'u : ¬URel k n j v u := by    by_contra h; apply absurd (Eq.symm _) huu'    replace h := equivalenceOn_urel.trans (𝔘₃_subset_𝔘₂ hu') mv (𝔘₃_subset_𝔘₂ hu) rv h    exact EquivalenceOn.reprs_inj hu' hu h  have vnu : v ≠ u := by by_contra h; subst h; exact absurd URel.rfl np'u  simp_rw [URel, vnu, false_or, not_exists, not_and] at np'u  have mpt : p' ∈ 𝔗₁ k n j v := by    refine ⟨minLayer_subset mp', ?_, ?_⟩    · exact (lp'.1.trans_lt (lt_of_le_of_ne sl.1 np)).ne    · exact (wiggle_order_11_10 lp' (C5_3_3_le (X := X).trans (by norm_num))).trans sl  specialize np'u p' mpt  have 𝓘p'u : 𝓘 p' ≤ 𝓘 u := lp'.1.trans h  simp_rw [TileLike.le_def, smul_fst, 𝓘p'u, true_and] at np'u  obtain ⟨(q : Θ X), mq, nq⟩ := Set.not_subset.mp np'u  change dist_(u) q (𝒬 u) < 1 at mq; change ¬ dist_(p') q (𝒬 p') < 10 at nq; rw [not_lt] at nq  have d8 : 8 < dist_(p') (𝒬 p) (𝒬 u) :=    calc      _ = 10 - 1 - 1 := by norm_num      _ < 10 - 1 - dist_(u) q (𝒬 u) := by gcongr      _ ≤ 10 - 1 - dist_(p') q (𝒬 u) := tsub_le_tsub_left (Grid.dist_mono 𝓘p'u) _      _ ≤ dist_(p') q (𝒬 p') - 1 - dist_(p') q (𝒬 u) := by gcongr      _ < dist_(p') q (𝒬 p') - dist_(p') (𝒬 p) (𝒬 p') - dist_(p') q (𝒬 u) := by        gcongr; rw [← @mem_ball]; exact subset_cball (lp'.2 𝒬_mem_Ω)      _ ≤ _ := by        rw [sub_le_iff_le_add', sub_le_iff_le_add]        nth_rw 3 [dist_comm]; apply dist_triangle4  have Znpos : 0 < Z * (n + 1) := by rw [defaultZ]; positivity  let d : ℕ := (𝔰 p - 𝔰 p').toNat  have sd : 𝔰 p' + d = 𝔰 p := by simp_rw [d]; rw [Int.toNat_sub_of_le] <;> lia  have d1 : dist_(p') (𝒬 p) (𝒬 u) ≤ C2_1_2 a ^ d * dist_(p) (𝒬 p) (𝒬 u) :=    Grid.dist_strictMono_iterate lp'.1 sd  have Cdpos : 0 < C2_1_2 a ^ d := by rw [C2_1_2]; positivity  have Cidpos : 0 < (C2_1_2 a)⁻¹ ^ d := by rw [C2_1_2]; positivity  calc    _ ≤ (C2_1_2 a)⁻¹ ^ (Z * (n + 1)) := by      refine pow_le_pow_left₀ zero_le_two ?_ _      nth_rw 1 [C2_1_2, ← Real.inv_rpow zero_le_two, ← Real.rpow_neg_one,        ← Real.rpow_mul zero_le_two, neg_one_mul, ← Real.rpow_one 2]      apply Real.rpow_le_rpow_of_exponent_le one_le_two      simp only [add_mul, neg_mul, neg_add_rev, neg_neg, le_neg_add_iff_add_le]      norm_cast      have : 7 * a ≤ 𝕔 * a := by gcongr; exact seven_le_c      linarith [four_le_a X]    _ ≤ (C2_1_2 a)⁻¹ ^ d := by      refine pow_le_pow_right₀ ?_ (by lia)      simp_rw [one_le_inv_iff₀, C2_1_2_le_one (X := X), and_true, C2_1_2]; positivity    _ ≤ (C2_1_2 a)⁻¹ ^ d * 8 := by nth_rw 1 [← mul_one (_ ^ d)]; gcongr; norm_num    _ < (C2_1_2 a)⁻¹ ^ d * dist_(p') (𝒬 p) (𝒬 u) := by gcongr    _ ≤ _ := by      rwa [← mul_le_mul_iff_of_pos_left Cdpos, inv_pow, ← mul_assoc, mul_inv_cancel₀ Cdpos.ne',        one_mul]