awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
rw : ((μ.withDensity f).trim hm : (a : Set α) → ℝ≥0∞) s = ∫⁻ (a : α) in s, f a ∂μ.trim hm
⊢ Eq (α := ℝ≥0∞) (((μ.withDensity f).trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((μ.trim hm).withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw₁ : ((μ.withDensity f).trim hm : (a : Set α) → ℝ≥0∞) s = ∫⁻ (a : α), f a ∂(μ.restrict s).trim hm
Tactic: rw [withDensity_apply _ hs, restrict_trim _ _ hs, lintegral_trim _ hf, trim_measurableSet_eq _ hs,
    withDensity_apply _ (hm s hs)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
rw : ((μ.withDensity f).trim hm : (a : Set α) → ℝ≥0∞) s = ∫⁻ (a : α) in s, f a ∂μ.trim hm
rw₁ : ((μ.withDensity f).trim hm : (a : Set α) → ℝ≥0∞) s = ∫⁻ (a : α), f a ∂(μ.restrict s).trim hm
⊢ Eq (α := ℝ≥0∞) (((μ.withDensity f).trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((μ.trim hm).withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw₂ : ((μ.withDensity f).trim hm : (a : Set α) → ℝ≥0∞) s = ∫⁻ (a : α) in s, f a ∂μ
Tactic: rw [withDensity_apply _ hs, restrict_trim _ _ hs, lintegral_trim _ hf, trim_measurableSet_eq _ hs,
    withDensity_apply _ (hm s hs)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
rw : ((μ.withDensity f).trim hm : (a : Set α) → ℝ≥0∞) s = ∫⁻ (a : α) in s, f a ∂μ.trim hm
rw₁ : ((μ.withDensity f).trim hm : (a : Set α) → ℝ≥0∞) s = ∫⁻ (a : α), f a ∂(μ.restrict s).trim hm
rw₂ : ((μ.withDensity f).trim hm : (a : Set α) → ℝ≥0∞) s = ∫⁻ (a : α) in s, f a ∂μ
⊢ Eq (α := ℝ≥0∞) (((μ.withDensity f).trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((μ.trim hm).withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw₃ : (μ.withDensity f : (a : Set α) → ℝ≥0∞) s = ∫⁻ (a : α) in s, f a ∂μ
Tactic: rw [withDensity_apply _ hs, restrict_trim _ _ hs, lintegral_trim _ hf, trim_measurableSet_eq _ hs,
    withDensity_apply _ (hm s hs)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
rw : ((μ.withDensity f).trim hm : (a : Set α) → ℝ≥0∞) s = ∫⁻ (a : α) in s, f a ∂μ.trim hm
rw₁ : ((μ.withDensity f).trim hm : (a : Set α) → ℝ≥0∞) s = ∫⁻ (a : α), f a ∂(μ.restrict s).trim hm
rw₂ : ((μ.withDensity f).trim hm : (a : Set α) → ℝ≥0∞) s = ∫⁻ (a : α) in s, f a ∂μ
rw₃ : (μ.withDensity f : (a : Set α) → ℝ≥0∞) s = ∫⁻ (a : α) in s, f a ∂μ
⊢ Eq (α := ℝ≥0∞) (((μ.withDensity f).trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((μ.trim hm).withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw₄ : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, f a ∂μ
Tactic: rw [withDensity_apply _ hs, restrict_trim _ _ hs, lintegral_trim _ hf, trim_measurableSet_eq _ hs,
    withDensity_apply _ (hm s hs)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ μ.withDensity f = 0 ↔ f =ᶠ[ae μ] 0
have rw : Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞) ↔ f =ᶠ[ae μ] 0
Tactic: rw [← measure_univ_eq_zero, withDensity_apply _ .univ, restrict_univ, lintegral_eq_zero_iff' hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
rw : Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞) ↔ f =ᶠ[ae μ] 0
⊢ μ.withDensity f = 0 ↔ f =ᶠ[ae μ] 0
have rw₁ : ∫⁻ (a : α) in univ, f a ∂μ = 0 ↔ f =ᶠ[ae μ] 0
Tactic: rw [← measure_univ_eq_zero, withDensity_apply _ .univ, restrict_univ, lintegral_eq_zero_iff' hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
rw : Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞) ↔ f =ᶠ[ae μ] 0
rw₁ : ∫⁻ (a : α) in univ, f a ∂μ = 0 ↔ f =ᶠ[ae μ] 0
⊢ μ.withDensity f = 0 ↔ f =ᶠ[ae μ] 0
have rw₂ : ∫⁻ (a : α), f a ∂μ = 0 ↔ f =ᶠ[ae μ] 0
Tactic: rw [← measure_univ_eq_zero, withDensity_apply _ .univ, restrict_univ, lintegral_eq_zero_iff' hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
rw : Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞) ↔ f =ᶠ[ae μ] 0
rw₁ : ∫⁻ (a : α) in univ, f a ∂μ = 0 ↔ f =ᶠ[ae μ] 0
rw₂ : ∫⁻ (a : α), f a ∂μ = 0 ↔ f =ᶠ[ae μ] 0
⊢ μ.withDensity f = 0 ↔ f =ᶠ[ae μ] 0
have rw₃ : f =ᶠ[ae μ] 0 ↔ f =ᶠ[ae μ] 0
Tactic: rw [← measure_univ_eq_zero, withDensity_apply _ .univ, restrict_univ, lintegral_eq_zero_iff' hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
have mp : Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) →
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
mp :
  Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
have mpr : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞) →
  Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α := toMeasurable (μ.withDensity f) s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
have mp : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ toMeasurable (μ.withDensity f) s) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: apply measure_mono_null (inter_subset_inter_right _ (subset_toMeasurable (μ.withDensity f) s))
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α := toMeasurable (μ.withDensity f) s
rw : Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [measure_toMeasurable, hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α := toMeasurable (μ.withDensity f) s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ toMeasurable (μ.withDensity f) s) : ℝ≥0∞) (0 : ℝ≥0∞)
have A : Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: have A : μ.withDensity f t = 0 := by rw [measure_toMeasurable, hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α := toMeasurable (μ.withDensity f) s
A : Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ toMeasurable (μ.withDensity f) s) : ℝ≥0∞) (0 : ℝ≥0∞)
have mp : ∀
  (A :
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬(a ∈ toMeasurable (μ.withDensity f) s → f a = 0 a)} : ℝ≥0∞)
      (0 : ℝ≥0∞)),
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ toMeasurable (μ.withDensity f) s) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [withDensity_apply f (measurableSet_toMeasurable _ s),
      lintegral_eq_zero_iff' (AEMeasurable.restrict hf),
      EventuallyEq, ae_restrict_iff'₀, ae_iff] at A
Cleared hypotheses: A
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α := toMeasurable (μ.withDensity f) s
A : Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
mp :
  ∀
    (A :
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬(a ∈ toMeasurable (μ.withDensity f) s → f a = 0 a)} : ℝ≥0∞)
        (0 : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ toMeasurable (μ.withDensity f) s) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ toMeasurable (μ.withDensity f) s) : ℝ≥0∞) (0 : ℝ≥0∞)
have mp₁ : ∀ (A : ∀ᵐ (x : α) ∂μ.restrict (toMeasurable (μ.withDensity f) s), f x = 0 x),
  NullMeasurableSet (toMeasurable (μ.withDensity f) s) μ
Tactic: rw [withDensity_apply f (measurableSet_toMeasurable _ s),
      lintegral_eq_zero_iff' (AEMeasurable.restrict hf),
      EventuallyEq, ae_restrict_iff'₀, ae_iff] at A
Cleared hypotheses: A
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α := toMeasurable (μ.withDensity f) s
A :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬(a ∈ toMeasurable (μ.withDensity f) s → f a = 0)} : ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ toMeasurable (μ.withDensity f) s) : ℝ≥0∞) (0 : ℝ≥0∞)
have h : {x : α | f x ≠ 0} ∩ toMeasurable (μ.withDensity f) s = {a : α | ¬(a ∈ toMeasurable (μ.withDensity f) s → f a = 0)}
Tactic: convert! A using 2
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α := toMeasurable (μ.withDensity f) s
A :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬(a ∈ toMeasurable (μ.withDensity f) s → f a = 0)} : ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ {x : α | f x ≠ 0} ∩ toMeasurable (μ.withDensity f) s = {a : α | ¬(a ∈ toMeasurable (μ.withDensity f) s → f a = 0)}
have h : ∀ (x : α),
  x ∈ {x : α | f x ≠ 0} ∩ toMeasurable (μ.withDensity f) s ↔
    Membership.mem (γ := Set α) {a : α | ¬(a ∈ toMeasurable (μ.withDensity f) s → f a = 0)} x
Tactic: ext x
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α := toMeasurable μ ({x : α | f x ≠ 0} ∩ s)
x : α
hx : x ∈ s
⊢ x ∈ t ∪ {x : α | f x = 0}
have inl : ∀ (fx : f x = 0), x ∈ t ∪ {x : α | f x = 0}
Tactic: rcases eq_or_ne (f x) 0 with (fx | fx)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α := toMeasurable μ ({x : α | f x ≠ 0} ∩ s)
x : α
hx : x ∈ s
inl : ∀ (fx : f x = 0), x ∈ t ∪ {x : α | f x = 0}
⊢ x ∈ t ∪ {x : α | f x = 0}
have inr : ∀ (fx : f x ≠ 0), x ∈ t ∪ {x : α | f x = 0}
Tactic: rcases eq_or_ne (f x) 0 with (fx | fx)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α := toMeasurable μ ({x : α | f x ≠ 0} ∩ s)
x : α
hx : x ∈ s
fx : f x ≠ 0
⊢ x ∈ t ∪ {x : α | f x = 0}
have inr : x ∈ t
Tactic: left
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α := toMeasurable μ ({x : α | f x ≠ 0} ∩ s)
x : α
hx : x ∈ s
fx : f x ≠ 0
⊢ x ∈ t
have inr : x ∈ {x : α | f x ≠ 0} ∩ s
Tactic: apply subset_toMeasurable _ _
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α := toMeasurable μ ({x : α | f x ≠ 0} ∩ s)
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have A : s ⊆ t ∪ {x : α | f x = 0}
Tactic: have A : s ⊆ t ∪ { x | f x = 0 } := by
      intro x hx
      rcases eq_or_ne (f x) 0 with (fx | fx)
      · simp only [fx, mem_union, mem_setOf_eq, or_true]
      · left
        apply subset_toMeasurable _ _
        exact ⟨fx, hx⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α := toMeasurable μ ({x : α | f x ≠ 0} ∩ s)
A : s ⊆ t ∪ {x : α | f x = 0}
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have apply : Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: apply measure_mono_null A (measure_union_null _ _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α := toMeasurable μ ({x : α | f x ≠ 0} ∩ s)
A : s ⊆ t ∪ {x : α | f x = 0}
apply : Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have apply₁ : Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) {x : α | f x = 0} : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: apply measure_mono_null A (measure_union_null _ _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α := toMeasurable μ ({x : α | f x ≠ 0} ∩ s)
A : s ⊆ t ∪ {x : α | f x = 0}
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
have a : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: apply withDensity_absolutelyContinuous
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α := toMeasurable μ ({x : α | f x ≠ 0} ∩ s)
A : s ⊆ t ∪ {x : α | f x = 0}
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) {x : α | f x = 0} : ℝ≥0∞) (0 : ℝ≥0∞)
have rcases : ∀ (g : α → ℝ≥0∞) (hg : Measurable g) (hfg : f =ᶠ[ae μ] g),
  Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) {x : α | f x = 0} : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rcases hf with ⟨g, hg, hfg⟩
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α := toMeasurable μ ({x : α | f x ≠ 0} ∩ s)
A : s ⊆ t ∪ {x : α | f x = 0}
g : α → ℝ≥0∞
hg : Measurable g
hfg : f =ᶠ[ae μ] g
⊢ Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) {x : α | (fun (x : α) ↦ {x : α | f x = 0} x = {x : α | g x = 0} x) x}ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
have h : ∀ (a : α) (ha : f a = g a), {x : α | f x = 0} a = {x : α | g x = 0} a
Tactic: filter_upwards [hfg] with a ha
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α := toMeasurable μ ({x : α | f x ≠ 0} ∩ s)
A : s ⊆ t ∪ {x : α | f x = 0}
g : α → ℝ≥0∞
hg : Measurable g
hfg : f =ᶠ[ae μ] g
a : α
ha : f a = g a
⊢ {x : α | f x = 0} a = {x : α | g x = 0} a
have h : {x : α | f x = 0} a ↔ {x : α | g x = 0} a
Tactic: rw [eq_iff_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α := toMeasurable μ ({x : α | f x ≠ 0} ∩ s)
A : s ⊆ t ∪ {x : α | f x = 0}
g : α → ℝ≥0∞
hg : Measurable g
hfg : f =ᶠ[ae μ] g
a : α
ha : f a = g a
h : {x : α | f x = 0} a
⊢ {x : α | g x = 0} a
have ha₁ : 0 = g a
Tactic: rw [h] at ha
Cleared hypotheses: ha, h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α := toMeasurable μ ({x : α | f x ≠ 0} ∩ s)
A : s ⊆ t ∪ {x : α | f x = 0}
g : α → ℝ≥0∞
hg : Measurable g
hfg : f =ᶠ[ae μ] g
a : α
ha : f a = g a
h : {x : α | g x = 0} a
⊢ {x : α | f x = 0} a
have ha₁ : f a = 0
Tactic: rw [h] at ha
Cleared hypotheses: ha, h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α := toMeasurable μ ({x : α | f x ≠ 0} ∩ s)
A : s ⊆ t ∪ {x : α | f x = 0}
g : α → ℝ≥0∞
hg : Measurable g
hfg : f =ᶠ[ae μ] g
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) {x : α | f x = 0} : ℝ≥0∞) (0 : ℝ≥0∞)
have t₁ : {x : α | f x = 0} =ᶠ[ae (μ.withDensity f)] {x : α | g x = 0}
Tactic: have t : {x | f x = 0} =ᵐ[μ.withDensity f] {x | g x = 0} := by
      apply withDensity_absolutelyContinuous
      filter_upwards [hfg] with a ha
      rw [eq_iff_iff]
      exact ⟨fun h ↦ by rw [h] at ha; exact ha.symm,
             fun h ↦ by rw [h] at ha; exact ha⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
t_1 : Set α := toMeasurable μ ({x : α | f x ≠ 0} ∩ s)
A : s ⊆ t_1 ∪ {x : α | f x = 0}
g : α → ℝ≥0∞
hg : Measurable g
hfg : f =ᶠ[ae μ] g
t : {x : α | f x = 0} =ᶠ[ae (μ.withDensity f)] {x : α | g x = 0}
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) {x : α | f x = 0} : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ.withDensity g : (a : Set α) → ℝ≥0∞) {x : α | g x = 0} : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [measure_congr t, withDensity_congr_ae hfg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
t_1 : Set α := toMeasurable μ ({x : α | f x ≠ 0} ∩ s)
A : s ⊆ t_1 ∪ {x : α | f x = 0}
g : α → ℝ≥0∞
hg : Measurable g
hfg : f =ᶠ[ae μ] g
t : {x : α | f x = 0} =ᶠ[ae (μ.withDensity f)] {x : α | g x = 0}
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity g : (a : Set α) → ℝ≥0∞) {x : α | g x = 0} : ℝ≥0∞) (0 : ℝ≥0∞)
have M : MeasurableSet.{u_1} (α := α) {x : α | g x = 0}
Tactic: have M : MeasurableSet { x : α | g x = 0 } := hg (measurableSet_singleton _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
t_1 : Set α := toMeasurable μ ({x : α | f x ≠ 0} ∩ s)
A : s ⊆ t_1 ∪ {x : α | f x = 0}
g : α → ℝ≥0∞
hg : Measurable g
hfg : f =ᶠ[ae μ] g
t : {x : α | f x = 0} =ᶠ[ae (μ.withDensity f)] {x : α | g x = 0}
M : MeasurableSet.{u_1} (α := α) {x : α | g x = 0}
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity g : (a : Set α) → ℝ≥0∞) {x : α | g x = 0} : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : g =ᶠ[ae (μ.restrict {x : α | g x = 0})] 0
Tactic: rw [withDensity_apply _ M, lintegral_eq_zero_iff hg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
t_1 : Set α := toMeasurable μ ({x : α | f x ≠ 0} ∩ s)
A : s ⊆ t_1 ∪ {x : α | f x = 0}
g : α → ℝ≥0∞
hg : Measurable g
hfg : f =ᶠ[ae μ] g
t : {x : α | f x = 0} =ᶠ[ae (μ.withDensity f)] {x : α | g x = 0}
M : MeasurableSet.{u_1} (α := α) {x : α | g x = 0}
⊢ g =ᶠ[ae (μ.restrict {x : α | g x = 0})] 0
have h : ∀ (a : α), g a = 0 → g a = 0 a
Tactic: filter_upwards [ae_restrict_mem M]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ (∀ᵐ (x : α) ∂μ.withDensity f, p x) ↔ ∀ᵐ (x : α) ∂μ, f x ≠ 0 → p x
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ {a : α | ¬p a}) : ℝ≥0∞) (0 : ℝ≥0∞) =
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬(f a ≠ 0 → p a)} : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [ae_iff, ae_iff, withDensity_apply_eq_zero' hf, iff_iff_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≠ 0} ∩ {a : α | ¬p a}) : ℝ≥0∞) (0 : ℝ≥0∞) =
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬(f a ≠ 0 → p a)} : ℝ≥0∞) (0 : ℝ≥0∞)
have e_a : Eq.{u_1 + 1} (α := Set α) ({x : α | f x ≠ 0} ∩ {a : α | ¬p a}) {a : α | ¬(f a ≠ 0 → p a)}
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ Eq.{u_1 + 1} (α := Set α) ({x : α | f x ≠ 0} ∩ {a : α | ¬p a}) {a : α | ¬(f a ≠ 0 → p a)}
have e_a : ∀ (x : α),
  Membership.mem (γ := Set α) ({x : α | f x ≠ 0} ∩ {a : α | ¬p a}) x ↔
    Membership.mem (γ := Set α) {a : α | ¬(f a ≠ 0 → p a)} x
Tactic: ext x
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ (∀ᵐ (x : α) ∂μ.withDensity f, p x) ↔ ∀ᵐ (x : α) ∂μ.restrict {x : α | f x ≠ 0}, p x
have rw : (∀ᵐ (x : α) ∂μ, f x ≠ 0 → p x) ↔ ∀ᵐ (x : α) ∂μ, Membership.mem (γ := Set α) {x : α | f x ≠ 0} x → p x
Tactic: rw [ae_withDensity_iff' hf, ae_restrict_iff'₀]