urel_of_not_disjoint

lemma urel_of_not_disjoint {x y : 𝔓 X} (my : y ∈ 𝔘₂ k n j) (xye : 𝓘 x = 𝓘 y)    (nd : ¬Disjoint (ball_(x) (𝒬 x) 100) (ball_(y) (𝒬 y) 100)) : URel k n j y x := by  rw [not_disjoint_iff] at nd  obtain ⟨(ϑ : Θ X), (ϑx : ϑ ∈ ball_{𝓘 x} (𝒬 x) 100), (ϑy : ϑ ∈ ball_{𝓘 y} (𝒬 y) 100)⟩ := nd  rw [𝔘₂, mem_setOf, not_disjoint_iff] at my; obtain ⟨p, hp, _⟩ := my.2  suffices w : ball_(x) (𝒬 x) 1 ⊆ ball_(y) (𝒬 y) 500 by    right; use p, hp; obtain ⟨_, np, sl⟩ := hp    have hpy : smul 10 p ≤ smul 500 y :=      (smul_mono_left (by norm_num)).trans (wiggle_order_500 sl np)    exact ⟨(xye ▸ sl.1 : 𝓘 p ≤ 𝓘 x), hpy.2.trans w⟩  intro (q : Θ X) (mq : q ∈ ball_{𝓘 x} (𝒬 x) 1)  calc    _ ≤ dist_(y) q ϑ + dist_(y) ϑ (𝒬 y) := dist_triangle ..    _ ≤ dist_(y) q (𝒬 x) + dist_(y) ϑ (𝒬 x) + dist_(y) ϑ (𝒬 y) := by      gcongr; apply dist_triangle_right    _ < 1 + 100 + 100 := by      have hϑy : dist_(y) ϑ (𝒬 y) < 100 := ϑy      have hc : 𝔠 x = 𝔠 y := congr_arg c xye      have hs : 𝔰 x = 𝔰 y := congr_arg s xye      gcongr      · rw [← hc, ← hs]        exact mq      · rw [← hc, ← hs]        exact mem_ball.mp ϑx    _ < _ := by norm_num