TileStructure.Forest.disjoint_of_ne_of_mem

lemma disjoint_of_ne_of_mem {i j : ℕ} {u u' : 𝔓 X} (hne : u ≠ u') (hu : u ∈ t.rowDecomp i) (hu' : u' ∈ t.rowDecomp j)  {p p' : 𝔓 X} (hp : p ∈ t u) (hp' : p' ∈ t u') : Disjoint (E p) (E p') := by  classical  wlog hsle : 𝔰 p ≤ 𝔰 p'  · exact (this hne.symm hu' hu hp' hp (Int.le_of_not_le hsle)).symm  -- if x is in the inter, both `Disjoint (Ω p) (Ω p')` and `Q x ∈ Ω p ∩ Ω p'`  refine _root_.not_imp_self.mp (fun h => disjoint_impl ?_)  simp only [Set.disjoint_iff, subset_def, mem_inter_iff, mem_empty_iff_false, imp_false, not_and,    not_forall, Decidable.not_not] at h  obtain ⟨x,hxp, hxp'⟩ := h  rw [← rowDecomp_apply (j := j)] at hp'  have 𝓘_p_le : 𝓘 p ≤ 𝓘 p' := by    exact ⟨(fundamental_dyadic hsle).resolve_right <|      Set.Nonempty.not_disjoint <|      Set.nonempty_of_mem ⟨E_subset_𝓘 hxp,E_subset_𝓘 hxp'⟩, hsle⟩  have : 2 ^ (Z * (n + 1)) < dist_(p) (𝒬 p) (𝒬 u') := lt_dist t    (mem_forest_of_mem hu') (mem_forest_of_mem hu) hne.symm hp    <| le_trans 𝓘_p_le (𝓘_le_𝓘 _ hu' hp')  have := calc 2 ^ (Z * (n + 1)) - 4    _ < dist_(p) (𝒬 p) (𝒬 u') - dist_(p) (𝒬 p') (𝒬 u') :=      sub_lt_sub this <| lt_of_le_of_lt (Grid.dist_mono 𝓘_p_le) <| dist_lt_four _ hu' hp'    _ ≤ dist_(p) (𝒬 p) (𝒬 p') := by      exact le_trans (le_abs_self _) <|        abs_dist_sub_le (α := WithFunctionDistance (𝔠 p) (↑D ^ 𝔰 p / 4)) _ _ _  have : 𝒬 p' ∉ ball_(p) (𝒬 p) 1 := by    intro hmem    apply not_lt_of_ge (le_trans (calculation_7_7_4 (X := X)) this.le) (mem_ball'.mp hmem)  have : ¬(Ω p' ⊆ Ω p) := (fun hx => this <| subset_cball <| hx 𝒬_mem_Ω)  exact (relative_fundamental_dyadic 𝓘_p_le).resolve_right this