tile_disjointness

lemma tile_disjointness {𝔄 : Set (𝔓 X)} (h𝔄 : IsAntichain (· ≤ ·) (𝔄 : Set (𝔓 X)))     {p p' : 𝔓 X} (hp : p ∈ 𝔄) (hp' : p' ∈ 𝔄) (hE : ¬Disjoint (E p) (E p')) : p = p' := by  wlog h𝔰 : 𝔰 p ≤ 𝔰 p'  · have hE' : ¬Disjoint (E p') (E p) := by rwa [disjoint_comm]    exact (this h𝔄 hp' hp hE' (not_le.mp h𝔰).le).symm  obtain ⟨x, hx, hx'⟩ := not_disjoint_iff.mp hE  obtain ⟨hx𝓓p, hxΩp, -⟩ := hx; obtain ⟨hx𝓓p', hxΩp', -⟩ := hx'  have h𝓓 : 𝓘 p ≤ 𝓘 p' :=    (or_iff_left (not_disjoint_iff.mpr ⟨x, hx𝓓p, hx𝓓p'⟩)).mp (le_or_disjoint h𝔰)  have hΩ : Ω p' ≤ Ω p :=    (or_iff_right (not_disjoint_iff.mpr ⟨Q x, hxΩp, hxΩp'⟩)).mp (relative_fundamental_dyadic h𝓓)  exact h𝔄.eq hp hp' ⟨h𝓓, hΩ⟩