URel.not_disjoint

lemma URel.not_disjoint (hu : u ∈ 𝔘₂ k n j) (hu' : u' ∈ 𝔘₂ k n j) (huu' : URel k n j u u') :    ¬Disjoint (ball_(u) (𝒬 u) 100) (ball_(u') (𝒬 u') 100) := by  classical  by_cases e : u = u'  · rw [e]    exact not_disjoint_iff.mpr ⟨𝒬 u', mem_ball_self (by positivity), mem_ball_self (by positivity)⟩  simp_rw [URel, e, false_or] at huu'; obtain ⟨p, ⟨mp, np, sl₁⟩, sl₂⟩ := huu'  by_cases e' : 𝓘 p = 𝓘 u'  · refine not_disjoint_iff.mpr ⟨𝒬 u, mem_ball_self (by positivity), ?_⟩    have i1 : ball_{𝓘 u} (𝒬 u) 1 ⊆ ball_{𝓘 p} (𝒬 p) 2 := sl₁.2    have i2 : ball_{𝓘 u'} (𝒬 u') 1 ⊆ ball_{𝓘 p} (𝒬 p) 10 := sl₂.2    replace i1 : 𝒬 u ∈ ball_{𝓘 p} (𝒬 p) 2 := i1 (mem_ball_self zero_lt_one)    replace i2 : 𝒬 u' ∈ ball_{𝓘 p} (𝒬 p) 10 := i2 (mem_ball_self zero_lt_one)    rw [e'] at i1 i2    calc      _ ≤ dist_{𝓘 u'} (𝒬 u) (𝒬 p) + dist_{𝓘 u'} (𝒬 u') (𝒬 p) := dist_triangle_right ..      _ < 2 + 10 := add_lt_add i1 i2      _ < 100 := by norm_num  have plu : smul 100 p ≤ smul 100 u := wiggle_order_100 (smul_mono sl₁ le_rfl (by norm_num)) np  have plu' : smul 100 p ≤ smul 100 u' := wiggle_order_100 sl₂ e'  by_contra h  have 𝔅dj : Disjoint (𝔅 k n u) (𝔅 k n u') := by    simp_rw [𝔅, disjoint_left, mem_setOf, not_and]; intro q ⟨_, sl⟩ _    simp_rw [TileLike.le_def, smul_fst, smul_snd, not_and_or] at sl ⊢; right    have := disjoint_left.mp (h.mono_left sl.2) (mem_ball_self zero_lt_one)    rw [not_subset]; use 𝒬 q, mem_ball_self zero_lt_one  have usp : 𝔅 k n u ⊆ 𝔅 k n p := fun q mq ↦ by    rw [𝔅, mem_setOf] at mq ⊢; exact ⟨mq.1, plu.trans mq.2⟩  have u'sp : 𝔅 k n u' ⊆ 𝔅 k n p := fun q mq ↦ by    rw [𝔅, mem_setOf] at mq ⊢; exact ⟨mq.1, plu'.trans mq.2⟩  rw [𝔘₂, mem_setOf, 𝔘₁, mem_setOf] at hu hu'  apply absurd (card_𝔅_of_mem_ℭ₁ mp).2; rw [not_lt]  calc    _ = 2 ^ j + 2 ^ j := Nat.two_pow_succ j    _ ≤ (𝔅 k n u).toFinset.card + (𝔅 k n u').toFinset.card :=      add_le_add (card_𝔅_of_mem_ℭ₁ hu.1.1).1 (card_𝔅_of_mem_ℭ₁ hu'.1.1).1    _ = (𝔅 k n u ∪ 𝔅 k n u').toFinset.card := by      rw [toFinset_union]; refine (Finset.card_union_of_disjoint ?_).symm      rwa [Set.disjoint_toFinset]    _ ≤ _ := by      apply Finset.card_le_card      simp_rw [toFinset_union, subset_toFinset, Finset.coe_union, coe_toFinset, union_subset_iff]      exact ⟨usp, u'sp⟩