Construction.Ω_disjoint

lemma Ω_disjoint {p p' : 𝔓 X} (hn : p ≠ p') (h𝓘 : 𝓘 p = 𝓘 p') : Disjoint (Ω p) (Ω p') := by  change p.1 = p'.1 at h𝓘; obtain ⟨I, y⟩ := p; obtain ⟨_, z⟩ := p'  subst h𝓘; dsimp only at hn z ⊢  replace hn : y ≠ z := fun e ↦ hn (congrArg (Sigma.mk I) e)  induction I using Grid.induction with  | base I maxI =>    unfold Ω; simp only [maxI, dite_true]    contrapose! hn; rw [not_disjoint_iff_nonempty_inter] at hn    exact disjoint_frequency_cubes hn  | ind I nmaxI ih =>    unfold Ω; simp only [nmaxI, dite_false]    have dj := (disjoint_frequency_cubes (f := y) (g := z)).mt hn    rw [← not_disjoint_iff_nonempty_inter, not_not] at dj    rw [disjoint_union_left]; constructor <;> (rw [disjoint_union_right]; constructor)    · have binc : ∀ x, ball_{I} x.1 CΩ ⊆ Ω₁ ⟨I, x⟩ := fun x ↦        (ball_subset_ball (by norm_num)).trans (ball_subset_Ω₁ ⟨I, x⟩)      exact (dj.mono_left (binc y)).mono_right (binc z)    · exact Ω_disjoint_aux nmaxI hn    · exact (Ω_disjoint_aux nmaxI hn.symm).symm    · rw [disjoint_iUnion₂_left]; intro a ⟨ma₁, ma₂⟩      rw [disjoint_iUnion₂_right]; intro b ⟨mb₁, mb₂⟩      exact ih ⟨a, ma₁⟩ ⟨b, mb₁⟩ (by simp [dj.ne_of_mem ma₂ mb₂])