awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
δ : Type u_5
m0 : MeasurableSpace α
inst : MeasurableSpace δ
μ : Measure α
f : α → δ
hf : AEMeasurable f μ
s : Set δ
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ AEMeasurable.mk f hf ⁻¹' s) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (t ∩ f ⁻¹' s) : ℝ≥0∞)
have h : t ∩ AEMeasurable.mk f hf ⁻¹' s =ᶠ[ae μ] t ∩ f ⁻¹' s
Tactic: apply measure_congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (hypothesis)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
f : α → β
hc : MeasurableSpace.CountablyGenerated β
h : NullMeasurable f μ
⊢ AEMeasurable f μ
have a : Nontrivial β
Tactic: nontriviality β
-- 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 μ
h_1 : Nontrivial β
⊢ AEMeasurable f μ
have inhabit : ∀ (inhabited_h : Inhabited β), AEMeasurable f μ
Tactic: inhabit β
-- 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 μ
h_1 : Nontrivial β
inhabited_h : Inhabited β
⊢ AEMeasurable f μ
have rcases : ∀ (S : Set (Set β)) (hSc : S.Countable) [hc : MeasurableSpace.CountablyGenerated β] (h : NullMeasurable f μ),
  AEMeasurable f μ
Tactic: rcases hc.1 with ⟨S, hSc, rfl⟩
Cleared hypotheses: inst, hc, h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
h_1 : Nontrivial β
inhabited_h : Inhabited β
S : Set (Set β)
hSc : S.Countable
hc : MeasurableSpace.CountablyGenerated β
h : NullMeasurable f μ
⊢ AEMeasurable f μ
have choose! : ∀ (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 μ
Tactic: choose! T hTf hTm hTeq using fun s hs ↦ (h <| .basic s hs).exists_measurable_subset_ae_eq
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
h_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
⊢ AEMeasurable f μ
have choose! : ∀ (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 μ
Tactic: choose! U hUf hUm hUeq using fun s hs ↦ (h <| .basic s hs).exists_measurable_superset_ae_eq
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (hypothesis)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
h_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
v : Set α := ⋃ s ∈ S, U s \ T s
⊢ AEMeasurable f μ
have hvm : MeasurableSet v
Tactic: have hvm : MeasurableSet v := .biUnion hSc fun s hs ↦ (hUm s hs).diff (hTm s hs)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (hypothesis)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
h_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
v : Set α := ⋃ s ∈ S, U s \ T s
hvm : MeasurableSet v
⊢ AEMeasurable f μ
have hvμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
h_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
v : Set α := ⋃ s ∈ S, U s \ T s
hvm : MeasurableSet v
hvμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ AEMeasurable f μ
have refine : Measurable (v.piecewise (β := fun (a : α) ↦ β) (fun (x : α) ↦ default) f)
Tactic: refine ⟨v.piecewise (fun _ ↦ default) f, ?_, measure_mono_null (fun x ↦
    not_imp_comm.2 fun hxv ↦ (piecewise_eq_of_notMem _ _ _ hxv).symm) hvμ⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
h_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
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)
have refine_1 : Measurable (v.restrict (π := fun (a : α) ↦ β) (v.piecewise (β := fun (a : α) ↦ β) (fun (x : α) ↦ default) f))
Tactic: refine measurable_of_restrict_of_restrict_compl hvm ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
h_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
v : Set α := ⋃ s ∈ S, U s \ T s
hvm : MeasurableSet v
hvμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (0 : ℝ≥0∞)
refine_1 : Measurable (v.restrict (π := fun (a : α) ↦ β) (v.piecewise (β := fun (a : α) ↦ β) (fun (x : α) ↦ default) f))
⊢ Measurable (v.piecewise (β := fun (a : α) ↦ β) (fun (x : α) ↦ default) f)
have refine_2 : Measurable (vᶜ.restrict (π := fun (a : α) ↦ β) (v.piecewise (β := fun (a : α) ↦ β) (fun (x : α) ↦ default) f))
Tactic: refine measurable_of_restrict_of_restrict_compl hvm ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
h_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
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))
have refine_1 : Measurable.{u_2, u_3} (α := (↑v : Type u_2)) (β := β) (v.restrict (π := fun (a : α) ↦ β) fun (x : α) ↦ default)
Tactic: rw [restrict_piecewise]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
h_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
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))
have refine_2 : Measurable (α := (↑vᶜ : Type u_2)) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ vᶜ))
Tactic: rw [restrict_piecewise_compl, restrict_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
h_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
v : Set α := ⋃ s ∈ S, U s \ T s
hvm : MeasurableSet v
hvμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Measurable (α := (↑vᶜ : Type u_2)) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ vᶜ))
have refine_2 : ∀ (s : Set β) (hs : s ∈ S),
  MeasurableSet
    (image (α := { x : α // x ∈ vᶜ }) (Subtype.val (p := fun (x : α) ↦ x ∈ vᶜ))
      (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ vᶜ) ⁻¹' s))
Tactic: refine measurable_generateFrom fun s hs ↦ .of_subtype_image ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
h_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
v : Set α := ⋃ s ∈ S, U s \ T s
hvm : MeasurableSet v
hvμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (0 : ℝ≥0∞)
s : Set β
hs : s ∈ S
⊢ MeasurableSet
    (image (α := { x : α // x ∈ vᶜ }) (Subtype.val (p := fun (x : α) ↦ x ∈ vᶜ))
      (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ vᶜ) ⁻¹' s))
have refine_2 : MeasurableSet (vᶜ ∩ f ⁻¹' s)
Tactic: rw [preimage_comp, Subtype.image_preimage_coe]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
h_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
v : Set α := ⋃ s ∈ S, U s \ T s
hvm : MeasurableSet v
hvμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (0 : ℝ≥0∞)
s : Set β
hs : s ∈ S
⊢ MeasurableSet (vᶜ ∩ f ⁻¹' s)
have h₁ : vᶜ ∩ f ⁻¹' s = T s \ v
Tactic: convert! (hTm s hs).diff hvm using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
h_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
v : Set α := ⋃ s ∈ S, U s \ T s
hvm : MeasurableSet v
hvμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (0 : ℝ≥0∞)
s : Set β
hs : s ∈ S
⊢ vᶜ ∩ f ⁻¹' s = T s \ v
have h₁ : f ⁻¹' s ∩ vᶜ = T s \ v
Tactic: rw [inter_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : α → β
h_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
v : Set α := ⋃ s ∈ S, U s \ T s
hvm : MeasurableSet v
hvμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (0 : ℝ≥0∞)
s : Set β
hs : s ∈ S
⊢ f ⁻¹' s ∩ vᶜ = T s \ v
have h₁ : ∀ (x : α) (hxv : x ∈ vᶜ) (hx : x ∈ f ⁻¹' s), x ∈ T s
Tactic: refine Set.ext fun x ↦ and_congr_left fun hxv ↦ ⟨fun hx ↦ ?_, fun hx ↦ hTf s hs hx⟩
-- 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 μ
⊢ AEMeasurable f μ
have nontriviality : Subsingleton β → 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'⟩
-- 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 μ
⊢ AEMeasurable f μ
have nontriviality₁ : Nontrivial β → 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'⟩
-- 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 μ
⊢ AEMeasurable f μ
have nontriviality₃ : Nontrivial β → ∀ (inhabited_h : Inhabited β), 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'⟩
-- 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 μ
⊢ AEMeasurable f μ
have nontriviality₄ : Nontrivial β →
  ∀ (inhabited_h : Inhabited β) (S : Set (Set β)) (hSc : S.Countable) [hc : MeasurableSpace.CountablyGenerated β]
    (h : NullMeasurable 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'⟩
Cleared hypotheses: inst, hc, h
-- 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 μ
⊢ 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),
    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