czPartition_pairwiseDisjoint

lemma czPartition_pairwiseDisjoint {hX : GeneralCase f α} :    univ.PairwiseDisjoint fun i ↦ czPartition hX i := by  simp only [pairwiseDisjoint_iff, mem_univ, forall_const]  intro i k hik  have ⟨x, hxi, hxk⟩ := inter_nonempty.mp hik  have (t d) (hx : x ∈ czPartition hX t) (hd : t < d) : x ∉ czPartition hX d := by    have : czPartition hX t ⊆ ⋃ j < d, czPartition hX j := subset_biUnion_of_mem hd    rw [czPartition]    exact notMem_sdiff_of_mem <| mem_union_left _ (this hx)  have : _ ∧ _ := ⟨this i k hxi |>.mt (· hxk), this k i hxk |>.mt (· hxi)⟩  lia