-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
inst_1 : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
nontriviality : Subsingleton β → AEMeasurable f (sum μ)
nontriviality₁ : Nontrivial β → AEMeasurable f (sum μ)
nontriviality₂ nontriviality₃ : Nontrivial β → ∀ (inhabited_h : Inhabited β), AEMeasurable f (sum μ)
nontriviality₄ :
  Nontrivial β →
    ∀ (inhabited_h : Inhabited β),
      let s : ι → Set α := fun (i : ι) ↦ toMeasurable (μ i) {x : α | f x ≠ mk f ⋯ x};
      ∀ (hsμ : ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)), AEMeasurable f (sum μ)
nontriviality₅ :
  Nontrivial β →
    ∀ (inhabited_h : Inhabited β),
      let s : ι → Set α := fun (i : ι) ↦ toMeasurable (μ i) {x : α | f x ≠ mk f ⋯ x};
      ∀ (hsμ : ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞))
        (hsm : MeasurableSet.{u_2} (α := α) (⋂ (i : ι), s i)), AEMeasurable f (sum μ)
nontriviality₆ nontriviality₇ :
  Nontrivial β →
    ∀ (inhabited_h : Inhabited β),
      let s : ι → Set α := fun (i : ι) ↦ toMeasurable (μ i) {x : α | f x ≠ mk f ⋯ x};
      ∀ (hsμ : ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞))
        (hsm : MeasurableSet.{u_2} (α := α) (⋂ (i : ι), s i)) (hs : ∀ (i : ι), ∀ x ∉ s i, f x = mk f ⋯ x),
        AEMeasurable f (sum μ)
refine_1 :
  Nontrivial β →
    ∀ (inhabited_h : Inhabited β),
      let s : ι → Set α := fun (i : ι) ↦ toMeasurable (μ i) {x : α | f x ≠ mk f ⋯ x};
      ∀ (hsμ : ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞))
        (hsm : MeasurableSet.{u_2} (α := α) (⋂ (i : ι), s i)) (hs : ∀ (i : ι), ∀ x ∉ s i, f x = mk f ⋯ x),
        let g := piecewise (β := fun (a : α) ↦ β) (⋂ (i : ι), s i) (const α default) f;
        Measurable (α := (↑(⋂ (i : ι), s i) : Type u_2)) (Set.restrict (π := fun (a : α) ↦ β) (⋂ (i : ι), s i) g)
⊢ AEMeasurable f (sum μ)
have refine_2 : Nontrivial β →
  ∀ (inhabited_h : Inhabited β),
    let s : ι → Set α := fun (i : ι) ↦ toMeasurable (μ i) {x : α | f x ≠ mk f sorry x};
    ∀ (hsμ : ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞))
      (hsm : MeasurableSet.{u_2} (α := α) (⋂ (i : ι), s i)) (hs : ∀ (i : ι), ∀ x ∉ s i, f x = mk f sorry x),
      let g := piecewise (β := fun (a : α) ↦ β) (⋂ (i : ι), s i) (const α default) f;
      Measurable (α := (↑(⋂ (i : ι), s i)ᶜ : Type u_2)) (Set.restrict (π := fun (a : α) ↦ β) (⋂ (i : ι), s i)ᶜ g)
Tactic: classical
  nontriviality β
  inhabit β
  set s : ι → Set α := fun i => toMeasurable (μ i) { x | f x ≠ (h i).mk f x }
  have hsμ : ∀ i, μ i (s i) = 0 := by
    intro i
    rw [measure_toMeasurable]
    exact (h i).ae_eq_mk
  have hsm : MeasurableSet (⋂ i, s i) :=
    MeasurableSet.iInter fun i => measurableSet_toMeasurable _ _
  have hs : ∀ i x, x ∉ s i → f x = (h i).mk f x := by
    intro i x hx
    contrapose! hx
    exact subset_toMeasurable _ _ hx
  set g : α → β := (⋂ i, s i).piecewise (const α default) f
  refine ⟨g, measurable_of_restrict_of_restrict_compl hsm ?_ ?_, ae_sum_iff.mpr fun i => ?_⟩
  · rw [restrict_piecewise]
    simp only [s]
    exact measurable_const
  · rw [restrict_piecewise_compl, compl_iInter]
    intro t ht
    refine ⟨⋃ i, (h i).mk f ⁻¹' t ∩ (s i)ᶜ, MeasurableSet.iUnion fun i ↦
      (measurable_mk _ ht).inter (measurableSet_toMeasurable _ _).compl, ?_⟩
    ext ⟨x, hx⟩
    simp only [mem_preimage, mem_iUnion, Set.restrict, mem_inter_iff,
      mem_compl_iff] at hx ⊢
    constructor
    · rintro ⟨i, hxt, hxs⟩
      rwa [hs _ _ hxs]
    · rcases hx with ⟨i, hi⟩
      rw [hs _ _ hi]
      exact fun h => ⟨i, h, hi⟩
  · refine measure_mono_null (fun x (hx : f x ≠ g x) => ?_) (hsμ i)
    contrapose hx
    refine (piecewise_eq_of_notMem _ _ _ ?_).symm
    exact fun h => hx (mem_iInter.1 h i)