pairwiseDisjoint_E1

lemma pairwiseDisjoint_E1 : (𝔐 (X := X) k n).PairwiseDisjoint E₁ := fun p mp p' mp' h ↦ by  change Disjoint _ _  contrapose! h  have h𝓘 := (Disjoint.mono (E₁_subset p) (E₁_subset p')).mt h  wlog hs : s (𝓘 p') ≤ s (𝓘 p) generalizing p p'  · rw [disjoint_comm] at h h𝓘; rw [not_le] at hs; rw [this p' mp' p mp h h𝓘 hs.le]  obtain ⟨x, ⟨-, mxp⟩, ⟨-, mxp'⟩⟩ := not_disjoint_iff.mp h  rw [mem_preimage] at mxp mxp'  have l𝓘 := Grid.le_def.mpr ⟨(fundamental_dyadic hs).resolve_right (disjoint_comm.not.mpr h𝓘), hs⟩  have sΩ := (relative_fundamental_dyadic l𝓘).resolve_left <| not_disjoint_iff.mpr ⟨_, mxp', mxp⟩  rw [𝔐, mem_setOf] at mp mp'  exact mp'.eq_of_ge mp.prop ⟨l𝓘, sΩ⟩