forest_geometry

lemma forest_geometry (hu : u ∈ 𝔘₃ k n j) (hp : p ∈ 𝔗₂ k n j u) : smul 4 p ≤ smul 1 u := by  rw [𝔗₂, mem_inter_iff, mem_iUnion₂] at hp  obtain ⟨_, u', mu', w⟩ := hp; rw [mem_iUnion] at w; obtain ⟨ru, mp'⟩ := w  rw [𝔗₁, mem_setOf] at mp'; obtain ⟨_, np, sl⟩ := mp'  have xye := URel.eq (EquivalenceOn.reprs_subset hu) mu' ru  have huu' := URel.not_disjoint (EquivalenceOn.reprs_subset hu) mu' ru  rw [not_disjoint_iff] at huu'  obtain ⟨(ϑ : Θ X), (ϑx : ϑ ∈ ball_{𝓘 u} (𝒬 u) 100), (ϑy : ϑ ∈ ball_{𝓘 u'} (𝒬 u') 100)⟩ := huu'  suffices ball_(u) (𝒬 u) 1 ⊆ ball_(u') (𝒬 u') 500 by    have w : smul 4 p ≤ smul 500 u' := (wiggle_order_500 sl np)    exact ⟨(xye ▸ sl.1 : 𝓘 p ≤ 𝓘 u), w.2.trans this⟩  intro (q : Θ X) (mq : q ∈ ball_{𝓘 u} (𝒬 u) 1)  calc    _ ≤ dist_(u') q ϑ + dist_(u') ϑ (𝒬 u') := dist_triangle ..    _ ≤ dist_(u') q (𝒬 u) + dist_(u') ϑ (𝒬 u) + dist_(u') ϑ (𝒬 u') := by      gcongr; apply dist_triangle_right    _ < 1 + 100 + 100 := by      change dist_(u') ϑ (𝒬 u') < 100 at ϑy      have hc : 𝔠 u = 𝔠 u' := congrArg c xye      have hs : 𝔰 u = 𝔰 u' := congrArg s xye      gcongr      · rw [← hc, ← hs]; exact mq      · rw [← hc, ← hs]; exact ϑx    _ < _ := by norm_num