equivalenceOn_urel

lemma equivalenceOn_urel : EquivalenceOn (URel (X := X) k n j) (𝔘₂ k n j) where  refl _ _ := .rfl  trans {x y z} mx my mz xy yz := by    by_cases xny : x = y; · rwa [xny]    have xye := URel.eq mx my xy    have hxy := URel.not_disjoint mx my xy    rw [not_disjoint_iff] at hxy    obtain ⟨(ϑ : Θ X), (ϑx : ϑ ∈ ball_{𝓘 x} (𝒬 x) 100), (ϑy : ϑ ∈ ball_{𝓘 y} (𝒬 y) 100)⟩ := hxy    have yze := URel.eq my mz yz    have hyz := URel.not_disjoint my mz yz    rw [not_disjoint_iff] at hyz    obtain ⟨(θ : Θ X), (θy : θ ∈ ball_{𝓘 y} (𝒬 y) 100), (θz : θ ∈ ball_{𝓘 z} (𝒬 z) 100)⟩ := hyz    simp_rw [URel, xny, false_or] at xy; obtain ⟨p, mp, sp⟩ := xy    suffices ball_(z) (𝒬 z) 1 ⊆ ball_(x) (𝒬 x) 500 by      right; use p, mp; obtain ⟨_, np, sl⟩ := mp      have w : ball_(x) (𝒬 x) 500 ⊆ ball_(p) (𝒬 p) 4 := (wiggle_order_500 sl np).2      exact ⟨(yze ▸ xye ▸ sl.1 : 𝓘 p ≤ 𝓘 z), (this.trans w).trans (ball_subset_ball (by norm_num))⟩    intro (q : Θ X) (mq : q ∈ ball_{𝓘 z} (𝒬 z) 1)    calc      _ ≤ dist_(x) q ϑ + dist_(x) ϑ (𝒬 x) := dist_triangle ..      _ < dist_(x) q ϑ + 100 := by        change dist_(x) ϑ (𝒬 x) < 100 at ϑx        gcongr      _ ≤ dist_(x) q (𝒬 y) + dist_(x) ϑ (𝒬 y) + 100 := by        gcongr        exact dist_triangle_right ..      _ < dist_(x) q (𝒬 y) + 100 + 100 := by        have : dist_(x) ϑ (𝒬 y) < 100 := by rwa [← xye] at ϑy        gcongr      _ ≤ dist_(x) q θ + dist_(x) θ (𝒬 y) + 100 + 100 := by gcongr; exact dist_triangle ..      _ < dist_(x) q θ + 100 + 100 + 100 := by        have : dist_(x) θ (𝒬 y) < 100 := by rwa [← xye] at θy        gcongr      _ ≤ dist_(x) q (𝒬 z) + dist_(x) θ (𝒬 z) + 100 + 100 + 100 := by        gcongr; exact dist_triangle_right ..      _ < 1 + 100 + 100 + 100 + 100 := by        have : dist_(x) θ (𝒬 z) < 100 := by rwa [← yze, ← xye] at θz        gcongr        have hc : 𝔠 x = 𝔠 z := (congr_arg c xye).trans (congr_arg c yze)        have hs : 𝔰 x = 𝔰 z := (congr_arg s xye).trans (congr_arg s yze)        rw [hc, hs]        exact mq      _ < _ := by norm_num  symm {x y} mx my xy := urel_of_not_disjoint my (URel.eq mx my xy) (URel.not_disjoint mx my xy)