iUnion_czPartition

lemma iUnion_czPartition {hX : GeneralCase f α} :    ⋃ i, czPartition hX i = globalMaximalFunction volume 1 f ⁻¹' Ioi α := by  rw [← iUnion_czBall3 (hX := hX)]  refine ext fun x ↦ ⟨fun hx ↦ ?_, fun hx ↦ ?_⟩  · have : ⋃ i, czPartition hX i ⊆ ⋃ i, czBall3 hX i := fun y hy ↦      have ⟨r, hr⟩ := mem_iUnion.mp hy      mem_iUnion_of_mem r (czPartition_subset_czBall3 hr)    exact this hx  · rw [mem_iUnion] at hx ⊢    by_contra! hp    obtain ⟨g, hg⟩ := hx    have ⟨t, ht⟩ : ∃ i, x ∈ (⋃ j < i, czPartition hX j) ∪ ⋃ j > i, czBall hX j := by      by_contra! hb      absurd hp g      rw [czPartition, Set.mem_sdiff]      exact ⟨hg, hb g⟩    have : ⋃ j > t, czBall hX j ⊆ ⋃ j > t, czPartition hX j :=      iUnion₂_mono fun i j ↦ czBall_subset_czPartition (i := i)    have := (mem_or_mem_of_mem_union ht).imp_right (this ·)    simp_all