aemeasurable_czApproximation

lemma aemeasurable_czApproximation {hf : AEMeasurable f} : AEMeasurable (czApproximation f α) := by  by_cases hX : GeneralCase f α; swap  · unfold czApproximation; simp [hX]  let czA (x : X) := -- Measurable version of `czApproximation f α`    if hx : ∃ j, x ∈ czPartition hX j then ⨍ y in czPartition hX hx.choose, f y else hf.mk f x  refine ⟨czA, fun T hT ↦ ?_, hf.ae_eq_mk.mono fun x h ↦ by simp [czApproximation, czA, hX, h]⟩  let S := {x : X | ∃ j, x ∈ czPartition hX j}ᶜ ∩ (hf.mk f) ⁻¹' T  have : czA ⁻¹' T = S ∪ ⋃₀ (czPartition hX '' {i | ⨍ y in czPartition hX i, f y ∈ T}) := by    refine ext fun x ↦ ⟨fun h ↦ ?_, fun h ↦ ?_⟩    · by_cases hx : ∃ j, x ∈ czPartition hX j      · refine Or.inr ⟨czPartition hX hx.choose, ⟨mem_image_of_mem _ ?_, hx.choose_spec⟩⟩        simpa [czA, hx] using h      · exact Or.inl ⟨hx, by simpa [czA, hx, hX] using h⟩    · cases h with      | inl h => simpa [czA, mem_setOf_eq ▸ mem_setOf_eq ▸ h.1] using h.2      | inr h => obtain ⟨_, ⟨⟨i, ⟨hi, rfl⟩⟩, hxi⟩⟩ := h                 have hx : ∃ j, x ∈ czPartition hX j := ⟨i, hxi⟩                 simpa [czA, hx, czPartition_pairwiseDisjoint' hx.choose_spec hxi] using hi  rw [this]  have := Measurable.exists (MeasurableSet.czPartition hX · |>.mem)  apply MeasurableSet.union (by measurability) ∘ MeasurableSet.sUnion ((to_countable _).image _)  simp [MeasurableSet.czPartition hX]