awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
h_1 : Nontrivial β
inhabited_h : Inhabited β
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
g : α → β := piecewise (β := fun (a : α) ↦ β) (⋂ (i : ι), s i) (const α default) f
refine_1 : Measurable (α := (↑(⋂ (i : ι), s i) : Type u_2)) (Set.restrict (π := fun (a : α) ↦ β) (⋂ (i : ι), s i) g)
refine_2 : Measurable (α := (↑(⋂ (i : ι), s i)ᶜ : Type u_2)) (Set.restrict (π := fun (a : α) ↦ β) (⋂ (i : ι), s i)ᶜ g)
⊢ AEMeasurable f (sum μ)
have refine_3 : ∀ (i : ι), ∀ᵐ (x : α) ∂μ i, f x = g x
Tactic: refine ⟨g, measurable_of_restrict_of_restrict_compl hsm ?_ ?_, ae_sum_iff.mpr fun i => ?_⟩
-- 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)
h_1 : Nontrivial β
inhabited_h : Inhabited β
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
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)
have refine_1 : Measurable.{u_2, u_3} (α := (↑(⋂ (i : ι), s i) : Type u_2)) (β := β)
  (Set.restrict (π := fun (a : α) ↦ β) (⋂ (i : ι), s i) (const α default))
Tactic: rw [restrict_piecewise]
-- 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)
h_1 : Nontrivial β
inhabited_h : Inhabited β
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
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)
have refine_2 : Measurable (α := (↑(⋃ (i : ι), (s i)ᶜ) : Type u_2)) (Set.restrict (π := fun (a : α) ↦ β) (⋃ (i : ι), (s i)ᶜ) f)
Tactic: rw [restrict_piecewise_compl, compl_iInter]
-- 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)
h_1 : Nontrivial β
inhabited_h : Inhabited β
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
g : α → β := piecewise (β := fun (a : α) ↦ β) (⋂ (i : ι), s i) (const α default) f
t : Set β
ht : MeasurableSet t
⊢ MeasurableSet (α := (↑(⋃ (i : ι), (s i)ᶜ) : Type u_2))
    (Set.restrict (π := fun (a : α) ↦ β) (⋃ (i : ι), (s i)ᶜ) f ⁻¹' t)
have refine_2 : Eq (α := Set { x : α // Membership.mem (γ := Set α) (⋃ (i : ι), (s i)ᶜ) x })
  (Subtype.val (p := fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : ι), (s i)ᶜ) x) ⁻¹'
    ⋃ (i : ι), mk f sorry ⁻¹' t ∩ (s i)ᶜ)
  (Set.restrict (π := fun (a : α) ↦ β) (⋃ (i : ι), (s i)ᶜ) f ⁻¹' t)
Tactic: refine ⟨⋃ i, (h i).mk f ⁻¹' t ∩ (s i)ᶜ, MeasurableSet.iUnion fun i ↦
      (measurable_mk _ ht).inter (measurableSet_toMeasurable _ _).compl, ?_⟩
-- 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)
h_1 : Nontrivial β
inhabited_h : Inhabited β
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
g : α → β := piecewise (β := fun (a : α) ↦ β) (⋂ (i : ι), s i) (const α default) f
t : Set β
ht : MeasurableSet t
⊢ Eq (α := Set { x : α // Membership.mem (γ := Set α) (⋃ (i : ι), (s i)ᶜ) x })
    (Subtype.val (p := fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : ι), (s i)ᶜ) x) ⁻¹'
      ⋃ (i : ι), mk f ⋯ ⁻¹' t ∩ (s i)ᶜ)
    (Set.restrict (π := fun (a : α) ↦ β) (⋃ (i : ι), (s i)ᶜ) f ⁻¹' t)
have refine_2 : ∀ (x : α) (hx : Membership.mem (γ := Set α) (⋃ (i : ι), (s i)ᶜ) x),
  Membership.mem (γ := Set { x : α // Membership.mem (γ := Set α) (⋃ (i : ι), (s i)ᶜ) x })
      (Subtype.val (p := fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : ι), (s i)ᶜ) x) ⁻¹'
        ⋃ (i : ι), mk f sorry ⁻¹' t ∩ (s i)ᶜ)
      (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : ι), (s i)ᶜ) x) x hx) ↔
    Membership.mem (γ := Set { x : α // Membership.mem (γ := Set α) (⋃ (i : ι), (s i)ᶜ) x })
      (Set.restrict (π := fun (a : α) ↦ β) (⋃ (i : ι), (s i)ᶜ) f ⁻¹' t)
      (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : ι), (s i)ᶜ) x) x hx)
Tactic: ext ⟨x, hx⟩
-- 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)
h_1 : Nontrivial β
inhabited_h : Inhabited β
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
g : α → β := piecewise (β := fun (a : α) ↦ β) (⋂ (i : ι), s i) (const α default) f
t : Set β
ht : MeasurableSet t
x : α
hx : Membership.mem (γ := Set α) (⋃ (i : ι), (s i)ᶜ) x
⊢ Membership.mem (γ := Set { x : α // Membership.mem (γ := Set α) (⋃ (i : ι), (s i)ᶜ) x })
      (Subtype.val (p := fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : ι), (s i)ᶜ) x) ⁻¹'
        ⋃ (i : ι), mk f ⋯ ⁻¹' t ∩ (s i)ᶜ)
      (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : ι), (s i)ᶜ) x) x hx) ↔
    Membership.mem (γ := Set { x : α // Membership.mem (γ := Set α) (⋃ (i : ι), (s i)ᶜ) x })
      (Set.restrict (π := fun (a : α) ↦ β) (⋃ (i : ι), (s i)ᶜ) f ⁻¹' t)
      (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : ι), (s i)ᶜ) x) x hx)
have refine_2 : ∀ (hx : ∃ (i : ι), x ∉ s i), (∃ (i : ι), mk f sorry x ∈ t ∧ x ∉ s i) ↔ f x ∈ t
Tactic: simp only [mem_preimage, mem_iUnion, Set.restrict, mem_inter_iff,
      mem_compl_iff] at hx ⊢
Cleared hypotheses: hx
-- 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)
h_1 : Nontrivial β
inhabited_h : Inhabited β
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
g : α → β := piecewise (β := fun (a : α) ↦ β) (⋂ (i : ι), s i) (const α default) f
t : Set β
ht : MeasurableSet t
x : α
hx : ∃ (i : ι), x ∉ s i
⊢ (∃ (i : ι), mk f ⋯ x ∈ t ∧ x ∉ s i) ↔ f x ∈ t
have refine_2 : (∃ (i : ι), mk f sorry x ∈ t ∧ x ∉ s i) → f x ∈ t
Tactic: constructor
-- 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)
h_1 : Nontrivial β
inhabited_h : Inhabited β
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
g : α → β := piecewise (β := fun (a : α) ↦ β) (⋂ (i : ι), s i) (const α default) f
t : Set β
ht : MeasurableSet t
x : α
hx : ∃ (i : ι), x ∉ s i
refine_2 : (∃ (i : ι), mk f ⋯ x ∈ t ∧ x ∉ s i) → f x ∈ t
⊢ (∃ (i : ι), mk f ⋯ x ∈ t ∧ x ∉ s i) ↔ f x ∈ t
have refine_2₁ : f x ∈ t → ∃ (i : ι), mk f sorry x ∈ t ∧ x ∉ s i
Tactic: constructor
-- 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)
h_1 : Nontrivial β
inhabited_h : Inhabited β
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
g : α → β := piecewise (β := fun (a : α) ↦ β) (⋂ (i : ι), s i) (const α default) f
t : Set β
ht : MeasurableSet t
x : α
hx : ∃ (i : ι), x ∉ s i
⊢ f x ∈ t → ∃ (i : ι), mk f ⋯ x ∈ t ∧ x ∉ s i
have refine_2 : ∀ (i : ι) (hi : x ∉ s i), f x ∈ t → ∃ (i : ι), mk f sorry x ∈ t ∧ x ∉ s i
Tactic: rcases hx with ⟨i, hi⟩
Cleared hypotheses: hx
-- 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)
h_1 : Nontrivial β
inhabited_h : Inhabited β
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
g : α → β := piecewise (β := fun (a : α) ↦ β) (⋂ (i : ι), s i) (const α default) f
t : Set β
ht : MeasurableSet t
x : α
i : ι
hi : x ∉ s i
⊢ f x ∈ t → ∃ (i : ι), mk f ⋯ x ∈ t ∧ x ∉ s i
have refine_2 : mk f sorry x ∈ t → ∃ (i : ι), mk f sorry x ∈ t ∧ x ∉ s i
Tactic: rw [hs _ _ hi]
-- 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)
h_1 : Nontrivial β
inhabited_h : Inhabited β
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
g : α → β := piecewise (β := fun (a : α) ↦ β) (⋂ (i : ι), s i) (const α default) f
i : ι
⊢ ∀ᵐ (x : α) ∂μ i, f x = g x
have refine_3 : ∀ (x : α) (hx : f x ≠ g x), x ∈ s i
Tactic: refine measure_mono_null (fun x (hx : f x ≠ g x) => ?_) (hsμ i)
-- 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)
h_1 : Nontrivial β
inhabited_h : Inhabited β
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
g : α → β := piecewise (β := fun (a : α) ↦ β) (⋂ (i : ι), s i) (const α default) f
i : ι
x : α
hx : f x ≠ g x
⊢ x ∈ s i
have refine_3 : ∀ (hx : x ∉ s i), f x = g x
Tactic: contrapose hx
Cleared hypotheses: hx
-- 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)
h_1 : Nontrivial β
inhabited_h : Inhabited β
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
g : α → β := piecewise (β := fun (a : α) ↦ β) (⋂ (i : ι), s i) (const α default) f
i : ι
x : α
hx : x ∉ s i
⊢ f x = g x
have refine_3 : x ∉ ⋂ (i : ι), s i
Tactic: refine (piecewise_eq_of_notMem _ _ _ ?_).symm
-- 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)
⊢ AEMeasurable f (sum μ)
have nontriviality : Subsingleton β → AEMeasurable f (sum μ)
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)
-- 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 μ)
⊢ AEMeasurable f (sum μ)
have nontriviality₁ : Nontrivial β → AEMeasurable f (sum μ)
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)
-- 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 μ)
⊢ AEMeasurable f (sum μ)
have nontriviality₂ : Nontrivial β → ∀ (inhabited_h : Inhabited β), AEMeasurable f (sum μ)
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)
-- 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 μ)
⊢ AEMeasurable f (sum μ)
have nontriviality₄ : 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∞)), AEMeasurable f (sum μ)
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)
-- 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 μ)
⊢ AEMeasurable f (sum μ)
have nontriviality₅ : 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)), AEMeasurable f (sum μ)
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)