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)
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 μ)
⊢ 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)) (hs : ∀ (i : ι), ∀ x ∉ s i, f x = mk f sorry x),
      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_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ ν : Measure α
⊢ AEMeasurable f (μ + ν) ↔ AEMeasurable f μ ∧ AEMeasurable f ν
have rw : AEMeasurable f (bif true then μ else ν) ∧ AEMeasurable f (bif false then μ else ν) ↔ AEMeasurable f μ ∧ AEMeasurable f ν
Tactic: rw [← sum_cond, aemeasurable_sum_measure_iff, Bool.forall_bool, and_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ ν : Measure α
f : α → β
hμ : AEMeasurable f μ
hν : AEMeasurable f ν
⊢ Measure.map f (μ + ν) = HAdd.hAdd (α := Measure β) (Measure.map f μ) (Measure.map f ν)
have h : ∀ (s : Set β),
  MeasurableSet s →
    Eq (α := ℝ≥0∞) (((Measure.map f (μ + ν) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      ((HAdd.hAdd (α := Measure β) (Measure.map f μ) (Measure.map f ν) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
μ : Measure α
g : β → γ
f : α → β
hg : AEMeasurable (_m := inst) g (Measure.map f μ)
hf : AEMeasurable f μ
⊢ Eq (α := Measure γ) (Measure.map g (Measure.map f μ)) (Measure.map (g ∘ f) μ)
have h : ∀ (s : Set γ) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) (((Measure.map g (Measure.map f μ) : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    (((Measure.map (g ∘ f) μ : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext1 s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
μ : Measure α
g : β → γ
f : α → β
hg : AEMeasurable (_m := inst) g (Measure.map f μ)
hf : AEMeasurable f μ
s : Set γ
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((Measure.map g (Measure.map f μ) : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    (((Measure.map (g ∘ f) μ : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) (g ⁻¹' s) : ℝ≥0∞)
  (((Measure.map (g ∘ f) μ : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [map_apply_of_aemeasurable hg hs, map_apply₀ hf (hg.nullMeasurable hs),
    map_apply_of_aemeasurable (hg.comp_aemeasurable hf) hs, preimage_comp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
μ : Measure α
g : β → γ
f : α → β
hg : AEMeasurable (_m := inst) g (Measure.map f μ)
hf : AEMeasurable f μ
s : Set γ
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) (g ⁻¹' s) : ℝ≥0∞)
    (((Measure.map (g ∘ f) μ : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((Measure.map g (Measure.map f μ) : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    (((Measure.map (g ∘ f) μ : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' g ⁻¹' s) : ℝ≥0∞)
  (((Measure.map (g ∘ f) μ : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [map_apply_of_aemeasurable hg hs, map_apply₀ hf (hg.nullMeasurable hs),
    map_apply_of_aemeasurable (hg.comp_aemeasurable hf) hs, preimage_comp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
μ : Measure α
g : β → γ
f : α → β
hg : AEMeasurable (_m := inst) g (Measure.map f μ)
hf : AEMeasurable f μ
s : Set γ
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) (g ⁻¹' s) : ℝ≥0∞)
    (((Measure.map (g ∘ f) μ : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' g ⁻¹' s) : ℝ≥0∞)
    (((Measure.map (g ∘ f) μ : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((Measure.map g (Measure.map f μ) : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    (((Measure.map (g ∘ f) μ : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
have h₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' g ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (g ∘ f ⁻¹' s) : ℝ≥0∞)
Tactic: rw [map_apply_of_aemeasurable hg hs, map_apply₀ hf (hg.nullMeasurable hs),
    map_apply_of_aemeasurable (hg.comp_aemeasurable hf) hs, preimage_comp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
μ : Measure α
g : β → γ
f : α → β
hg : AEMeasurable (_m := inst) g (Measure.map f μ)
hf : AEMeasurable f μ
s : Set γ
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) (g ⁻¹' s) : ℝ≥0∞)
    (((Measure.map (g ∘ f) μ : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' g ⁻¹' s) : ℝ≥0∞)
    (((Measure.map (g ∘ f) μ : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
h₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' g ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (g ∘ f ⁻¹' s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((Measure.map g (Measure.map f μ) : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    (((Measure.map (g ∘ f) μ : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
have h₃ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' g ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' g ⁻¹' s) : ℝ≥0∞)
Tactic: rw [map_apply_of_aemeasurable hg hs, map_apply₀ hf (hg.nullMeasurable hs),
    map_apply_of_aemeasurable (hg.comp_aemeasurable hf) hs, preimage_comp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
s : Set α := toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := s.piecewise (β := fun (a : α) ↦ β) (fun (x : α) ↦ h₀.some (s := t)) (mk f H)
⊢ ∃ (g : α → β), Measurable g ∧ range g ⊆ t ∧ f =ᶠ[ae μ] g
have refine_1 : Measurable g
Tactic: refine ⟨g, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
s : Set α := toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := s.piecewise (β := fun (a : α) ↦ β) (fun (x : α) ↦ h₀.some (s := t)) (mk f H)
refine_1 : Measurable g
⊢ ∃ (g : α → β), Measurable g ∧ range g ⊆ t ∧ f =ᶠ[ae μ] g
have refine_2 : range g ⊆ t
Tactic: refine ⟨g, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
s : Set α := toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := s.piecewise (β := fun (a : α) ↦ β) (fun (x : α) ↦ h₀.some (s := t)) (mk f H)
refine_1 : Measurable g
refine_2 : range g ⊆ t
⊢ ∃ (g : α → β), Measurable g ∧ range g ⊆ t ∧ f =ᶠ[ae μ] g
have refine_3 : f =ᶠ[ae μ] g
Tactic: refine ⟨g, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
s : Set α := toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := s.piecewise (β := fun (a : α) ↦ β) (fun (x : α) ↦ h₀.some (s := t)) (mk f H)
x : α
⊢ g x ∈ t
have pos : ∀ (hx : x ∈ s), g x ∈ t
Tactic: by_cases hx : x ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
s : Set α := toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := s.piecewise (β := fun (a : α) ↦ β) (fun (x : α) ↦ h₀.some (s := t)) (mk f H)
x : α
pos : ∀ (hx : x ∈ s), g x ∈ t
⊢ g x ∈ t
have neg : ∀ (hx : x ∉ s), g x ∈ t
Tactic: by_cases hx : x ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
s : Set α := toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := s.piecewise (β := fun (a : α) ↦ β) (fun (x : α) ↦ h₀.some (s := t)) (mk f H)
x : α
hx : x ∉ s
⊢ g x ∈ t
have neg : mk f H x ∈ t
Tactic: simp only [g, hx, piecewise_eq_of_notMem, not_false_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
s : Set α := toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := s.piecewise (β := fun (a : α) ↦ β) (fun (x : α) ↦ h₀.some (s := t)) (mk f H)
x : α
hx : x ∉ s
⊢ mk f H x ∈ t
have neg : ∀ (hx : mk f H x ∉ t), x ∈ s
Tactic: contrapose hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
s : Set α := toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := s.piecewise (β := fun (a : α) ↦ β) (fun (x : α) ↦ h₀.some (s := t)) (mk f H)
x : α
hx : mk f H x ∉ t
⊢ x ∈ s
have neg : Membership.mem (γ := Set α) {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ x
Tactic: apply subset_toMeasurable
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
s : Set α := toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := s.piecewise (β := fun (a : α) ↦ β) (fun (x : α) ↦ h₀.some (s := t)) (mk f H)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : {x : α | f x = mk f H x ∧ f x ∈ t} ∈ ae μ
Tactic: rw [measure_toMeasurable, ← compl_mem_ae_iff, compl_compl]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (hypothesis)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
s : Set α := toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := s.piecewise (β := fun (a : α) ↦ β) (fun (x : α) ↦ h₀.some (s := t)) (mk f H)
⊢ f =ᶠ[ae μ] g
have A : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: have A : μ (toMeasurable μ { x | f x = H.mk f x ∧ f x ∈ t }ᶜ) = 0 := by
      rw [measure_toMeasurable, ← compl_mem_ae_iff, compl_compl]
      exact H.ae_eq_mk.and ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
s : Set α := toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := s.piecewise (β := fun (a : α) ↦ β) (fun (x : α) ↦ h₀.some (s := t)) (mk f H)
A : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ f =ᶠ[ae μ] g
have h : ∀ (x : α) (hx : x ∈ (toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ)ᶜ), f x = g x
Tactic: filter_upwards [compl_mem_ae_iff.2 A] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (hypothesis)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
s : Set α := toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := s.piecewise (β := fun (a : α) ↦ β) (fun (x : α) ↦ h₀.some (s := t)) (mk f H)
A : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
x : α
hx : x ∈ (toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ)ᶜ
⊢ f x = g x
have hx₁ : x ∉ toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ
Tactic: rw [mem_compl_iff] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
s : Set α := toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := s.piecewise (β := fun (a : α) ↦ β) (fun (x : α) ↦ h₀.some (s := t)) (mk f H)
A : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
x : α
hx : x ∉ toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ
⊢ f x = g x
have h : f x = mk f H x
Tactic: simp only [s, g, hx, piecewise_eq_of_notMem, not_false_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
s : Set α := toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := s.piecewise (β := fun (a : α) ↦ β) (fun (x : α) ↦ h₀.some (s := t)) (mk f H)
A : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
x : α
hx : x ∉ toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ
⊢ f x = mk f H x
have h : ∀ (hx : f x ≠ mk f H x), x ∈ toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ
Tactic: contrapose! hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
s : Set α := toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ
g : α → β := s.piecewise (β := fun (a : α) ↦ β) (fun (x : α) ↦ h₀.some (s := t)) (mk f H)
A : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
x : α
hx : f x ≠ mk f H x
⊢ x ∈ toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ
have h : Membership.mem (γ := Set α) {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ x
Tactic: apply subset_toMeasurable
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
let let₁ let₂ let₃ : ∃ (g : α → β), Measurable g ∧ range g ⊆ t ∧ f =ᶠ[ae μ] g
⊢ ∃ (g : α → β), Measurable g ∧ range g ⊆ t ∧ f =ᶠ[ae μ] g
have refine_1 : let s := toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ;
let g := s.piecewise (β := fun (a : α) ↦ β) (fun (x : α) ↦ h₀.some (s := t)) (mk f H);
Measurable g
Tactic: classical
  let s : Set α := toMeasurable μ { x | f x = H.mk f x ∧ f x ∈ t }ᶜ
  let g : α → β := piecewise s (fun _ => h₀.some) (H.mk f)
  refine ⟨g, ?_, ?_, ?_⟩
  · exact Measurable.piecewise (measurableSet_toMeasurable _ _) measurable_const H.measurable_mk
  · rintro _ ⟨x, rfl⟩
    by_cases hx : x ∈ s
    · simpa [g, hx] using h₀.some_mem
    · simp only [g, hx, piecewise_eq_of_notMem, not_false_iff]
      contrapose hx
      apply subset_toMeasurable
      simp +contextual only [hx, mem_compl_iff, mem_setOf_eq, not_and,
        not_false_iff, imp_true_iff]
  · have A : μ (toMeasurable μ { x | f x = H.mk f x ∧ f x ∈ t }ᶜ) = 0 := by
      rw [measure_toMeasurable, ← compl_mem_ae_iff, compl_compl]
      exact H.ae_eq_mk.and ht
    filter_upwards [compl_mem_ae_iff.2 A] with x hx
    rw [mem_compl_iff] at hx
    simp only [s, g, hx, piecewise_eq_of_notMem, not_false_iff]
    contrapose! hx
    apply subset_toMeasurable
    simp only [hx, mem_compl_iff, mem_setOf_eq, false_and, not_false_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
let let₁ let₂ let₃ : ∃ (g : α → β), Measurable g ∧ range g ⊆ t ∧ f =ᶠ[ae μ] g
refine_1 :
  let s := toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ;
  let g := s.piecewise (β := fun (a : α) ↦ β) (fun (x : α) ↦ h₀.some (s := t)) (mk f H);
  Measurable g
⊢ ∃ (g : α → β), Measurable g ∧ range g ⊆ t ∧ f =ᶠ[ae μ] g
have refine_2 : let s := toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ;
let g := s.piecewise (β := fun (a : α) ↦ β) (fun (x : α) ↦ h₀.some (s := t)) (mk f H);
range g ⊆ t
Tactic: classical
  let s : Set α := toMeasurable μ { x | f x = H.mk f x ∧ f x ∈ t }ᶜ
  let g : α → β := piecewise s (fun _ => h₀.some) (H.mk f)
  refine ⟨g, ?_, ?_, ?_⟩
  · exact Measurable.piecewise (measurableSet_toMeasurable _ _) measurable_const H.measurable_mk
  · rintro _ ⟨x, rfl⟩
    by_cases hx : x ∈ s
    · simpa [g, hx] using h₀.some_mem
    · simp only [g, hx, piecewise_eq_of_notMem, not_false_iff]
      contrapose hx
      apply subset_toMeasurable
      simp +contextual only [hx, mem_compl_iff, mem_setOf_eq, not_and,
        not_false_iff, imp_true_iff]
  · have A : μ (toMeasurable μ { x | f x = H.mk f x ∧ f x ∈ t }ᶜ) = 0 := by
      rw [measure_toMeasurable, ← compl_mem_ae_iff, compl_compl]
      exact H.ae_eq_mk.and ht
    filter_upwards [compl_mem_ae_iff.2 A] with x hx
    rw [mem_compl_iff] at hx
    simp only [s, g, hx, piecewise_eq_of_notMem, not_false_iff]
    contrapose! hx
    apply subset_toMeasurable
    simp only [hx, mem_compl_iff, mem_setOf_eq, false_and, not_false_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
let let₁ let₂ let₃ : ∃ (g : α → β), Measurable g ∧ range g ⊆ t ∧ f =ᶠ[ae μ] g
refine_1 :
  let s := toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ;
  let g := s.piecewise (β := fun (a : α) ↦ β) (fun (x : α) ↦ h₀.some (s := t)) (mk f H);
  Measurable g
refine_2 :
  let s := toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ;
  let g := s.piecewise (β := fun (a : α) ↦ β) (fun (x : α) ↦ h₀.some (s := t)) (mk f H);
  range g ⊆ t
⊢ ∃ (g : α → β), Measurable g ∧ range g ⊆ t ∧ f =ᶠ[ae μ] g
have refine_3 : let s := toMeasurable μ {x : α | f x = mk f H x ∧ f x ∈ t}ᶜ;
let g := s.piecewise (β := fun (a : α) ↦ β) (fun (x : α) ↦ h₀.some (s := t)) (mk f H);
f =ᶠ[ae μ] g
Tactic: classical
  let s : Set α := toMeasurable μ { x | f x = H.mk f x ∧ f x ∈ t }ᶜ
  let g : α → β := piecewise s (fun _ => h₀.some) (H.mk f)
  refine ⟨g, ?_, ?_, ?_⟩
  · exact Measurable.piecewise (measurableSet_toMeasurable _ _) measurable_const H.measurable_mk
  · rintro _ ⟨x, rfl⟩
    by_cases hx : x ∈ s
    · simpa [g, hx] using h₀.some_mem
    · simp only [g, hx, piecewise_eq_of_notMem, not_false_iff]
      contrapose hx
      apply subset_toMeasurable
      simp +contextual only [hx, mem_compl_iff, mem_setOf_eq, not_and,
        not_false_iff, imp_true_iff]
  · have A : μ (toMeasurable μ { x | f x = H.mk f x ∧ f x ∈ t }ᶜ) = 0 := by
      rw [measure_toMeasurable, ← compl_mem_ae_iff, compl_compl]
      exact H.ae_eq_mk.and ht
    filter_upwards [compl_mem_ae_iff.2 A] with x hx
    rw [mem_compl_iff] at hx
    simp only [s, g, hx, piecewise_eq_of_notMem, not_false_iff]
    contrapose! hx
    apply subset_toMeasurable
    simp only [hx, mem_compl_iff, mem_setOf_eq, false_and, not_false_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : Preorder β
inst_1 : Zero β
mβ : MeasurableSpace β
f : α → β
hf : AEMeasurable f μ
f_nn : ∀ᵐ (t : α) ∂μ, 0 ≤ f t
⊢ ∃ (g : α → β), Measurable g ∧ 0 ≤ g ∧ f =ᶠ[ae μ] g
have obtain : ∀ (G : α → β) (hG_meas : Measurable G) (hG_mem : range G ⊆ (Preorder.toLE : LE β).1 0) (hG_ae_eq : f =ᶠ[ae μ] G),
  ∃ (g : α → β), Measurable g ∧ 0 ≤ g ∧ f =ᶠ[ae μ] g
Tactic: obtain ⟨G, hG_meas, hG_mem, hG_ae_eq⟩ := hf.exists_ae_eq_range_subset f_nn ⟨0, le_rfl⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AEMeasurable (hypothesis)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
h : AEMeasurable f μ
s : Set β
hfs : ∀ (x : α), f x ∈ s
⊢ AEMeasurable (codRestrict f s hfs) μ
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 β
f : α → β
μ : Measure α
h : AEMeasurable f μ
s : Set β
hfs : ∀ (x : α), f x ∈ s
h_1 : Nontrivial α
⊢ AEMeasurable (codRestrict f s hfs) μ
have inhabit : ∀ (inhabited_h : Inhabited α), AEMeasurable (codRestrict f s hfs) μ
Tactic: inhabit α