-- Module: Mathlib.MeasureTheory.Measure.AEMeasurable
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 μ
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 μ
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) (hvμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (0 : ℝ≥0∞)), 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)
      (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) (hvμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (0 : ℝ≥0∞)),
        Measurable (v.piecewise (β := fun (a : α) ↦ β) (fun (x : α) ↦ default) f)
refine_1 :
  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) (hvμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (0 : ℝ≥0∞)),
        Measurable (v.restrict (π := fun (a : α) ↦ β) (v.piecewise (β := fun (a : α) ↦ β) (fun (x : α) ↦ default) f))
refine_2 refine_2₁ :
  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) (hvμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (0 : ℝ≥0∞)),
        Measurable (vᶜ.restrict (π := fun (a : α) ↦ β) (v.piecewise (β := fun (a : α) ↦ β) (fun (x : α) ↦ default) f))
⊢ 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'⟩

Premises used: Subtype.image_preimage_coe, Set.restrict_piecewise, Set.preimage_comp, measurable_generateFrom, Set.inter_comm, MeasurableSpace.CountablyGenerated.isCountablyGenerated, Set.restrict_eq, measurable_const, MeasurableSet.of_subtype_image, rfl, Set.restrict_piecewise_compl