-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
f : α → β
hc : MeasurableSpace.CountablyGenerated β
h : NullMeasurable f μ
nontriviality : Subsingleton β → AEMeasurable f μ
nontriviality₁ nontriviality₂ : Nontrivial β → AEMeasurable f μ
nontriviality₃ : Nontrivial β → ∀ (inhabited_h : Inhabited β), AEMeasurable f μ
nontriviality₄ :
  Nontrivial β →
    ∀ (inhabited_h : Inhabited β) (S : Set (Set β)) (hSc : S.Countable) [hc : MeasurableSpace.CountablyGenerated β]
      (h : NullMeasurable f μ), AEMeasurable f μ
nontriviality₅ :
  Nontrivial β →
    ∀ (inhabited_h : Inhabited β) (S : Set (Set β)) (hSc : S.Countable) [hc : MeasurableSpace.CountablyGenerated β]
      (h : NullMeasurable f μ) (T : (s : Set β) → Set α) (hTf : ∀ (s : Set β) (hs : s ∈ S), T s ⊆ f ⁻¹' s)
      (hTm : ∀ (s : Set β) (hs : s ∈ S), MeasurableSet (T s)) (hTeq : ∀ (s : Set β) (hs : s ∈ S), T s =ᶠ[ae μ] f ⁻¹' s),
      AEMeasurable f μ
nontriviality₆ nontriviality₇ :
  Nontrivial β →
    ∀ (inhabited_h : Inhabited β) (S : Set (Set β)) (hSc : S.Countable) [hc : MeasurableSpace.CountablyGenerated β]
      (h : NullMeasurable f μ) (T : (s : Set β) → Set α) (hTf : ∀ (s : Set β) (hs : s ∈ S), T s ⊆ f ⁻¹' s)
      (hTm : ∀ (s : Set β) (hs : s ∈ S), MeasurableSet (T s)) (hTeq : ∀ (s : Set β) (hs : s ∈ S), T s =ᶠ[ae μ] f ⁻¹' s)
      (U : (s : Set β) → Set α) (hUf : ∀ (s : Set β) (hs : s ∈ S), U s ⊇ f ⁻¹' s)
      (hUm : ∀ (s : Set β) (hs : s ∈ S), MeasurableSet (U s)) (hUeq : ∀ (s : Set β) (hs : s ∈ S), U s =ᶠ[ae μ] f ⁻¹' s),
      AEMeasurable f μ
⊢ AEMeasurable f μ
have nontriviality₈ : Nontrivial β →
  ∀ (inhabited_h : Inhabited β) (S : Set (Set β)) (hSc : S.Countable) [hc : MeasurableSpace.CountablyGenerated β]
    (h : NullMeasurable f μ) (T : (s : Set β) → Set α) (hTf : ∀ (s : Set β) (hs : s ∈ S), T s ⊆ f ⁻¹' s)
    (hTm : ∀ (s : Set β) (hs : s ∈ S), MeasurableSet (T s)) (hTeq : ∀ (s : Set β) (hs : s ∈ S), T s =ᶠ[ae μ] f ⁻¹' s)
    (U : (s : Set β) → Set α) (hUf : ∀ (s : Set β) (hs : s ∈ S), U s ⊇ f ⁻¹' s)
    (hUm : ∀ (s : Set β) (hs : s ∈ S), MeasurableSet (U s)) (hUeq : ∀ (s : Set β) (hs : s ∈ S), U s =ᶠ[ae μ] f ⁻¹' s),
    let v : Set α := ⋃ s ∈ S, U s \ T s;
    ∀ (hvm : MeasurableSet v), AEMeasurable f μ
Tactic: classical
  nontriviality β; inhabit β
  rcases hc.1 with ⟨S, hSc, rfl⟩
  choose! T hTf hTm hTeq using fun s hs ↦ (h <| .basic s hs).exists_measurable_subset_ae_eq
  choose! U hUf hUm hUeq using fun s hs ↦ (h <| .basic s hs).exists_measurable_superset_ae_eq
  set v := ⋃ s ∈ S, U s \ T s
  have hvm : MeasurableSet v := .biUnion hSc fun s hs ↦ (hUm s hs).diff (hTm s hs)
  have hvμ : μ v = 0 := (measure_biUnion_null_iff hSc).2 fun s hs ↦ ae_le_set.1 <|
    ((hUeq s hs).trans (hTeq s hs).symm).le
  refine ⟨v.piecewise (fun _ ↦ default) f, ?_, measure_mono_null (fun x ↦
    not_imp_comm.2 fun hxv ↦ (piecewise_eq_of_notMem _ _ _ hxv).symm) hvμ⟩
  refine measurable_of_restrict_of_restrict_compl hvm ?_ ?_
  · rw [restrict_piecewise]
    apply measurable_const
  · rw [restrict_piecewise_compl, restrict_eq]
    refine measurable_generateFrom fun s hs ↦ .of_subtype_image ?_
    rw [preimage_comp, Subtype.image_preimage_coe]
    convert! (hTm s hs).diff hvm using 1
    rw [inter_comm]
    refine Set.ext fun x ↦ and_congr_left fun hxv ↦ ⟨fun hx ↦ ?_, fun hx ↦ hTf s hs hx⟩
    exact by_contra fun hx' ↦ hxv <| mem_biUnion hs ⟨hUf s hs hx, hx'⟩
Cleared hypotheses: inst, hc, h