pairwiseDisjoint_𝔘₄

lemma pairwiseDisjoint_𝔘₄ : univ.PairwiseDisjoint (𝔘₄ (X := X) k n j) := by  intro l hl m hm hml  apply disjoint_iff_forall_ne.2 (fun x hx y hy ↦ ?_)  simp only [𝔘₄, mem_Ico, mem_iUnion, exists_prop] at hx hy  rcases hx with ⟨a, ⟨ha, h'a⟩, xa⟩  rcases hy with ⟨b, ⟨hb, h'b⟩, yb⟩  have h : a ≠ b := by    rcases lt_or_gt_of_ne hml with h | h    · exact (h'a.trans_le (le_trans (mul_le_mul' h le_rfl) hb)).ne    · exact (h'b.trans_le (le_trans (mul_le_mul' h le_rfl) ha)).ne'  have := pairwiseDisjoint_iteratedMaximalSubfamily (𝔘₃ (X := X) k n j) (mem_univ a) (mem_univ b) h  exact disjoint_iff_forall_ne.1 this xa yb