awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
f : α → ℝ≥0∞
hf : AEMeasurable f μ
rw : (∀ᵐ (x : α) ∂μ, f x ≠ 0 → p x) ↔ ∀ᵐ (x : α) ∂μ, Membership.mem (γ := Set α) {x : α | f x ≠ 0} x → p x
⊢ (∀ᵐ (x : α) ∂μ.withDensity f, p x) ↔ ∀ᵐ (x : α) ∂μ.restrict {x : α | f x ≠ 0}, p x
have rw₁ : NullMeasurableSet {x : α | f x ≠ 0} μ
Tactic: rw [ae_withDensity_iff' hf, ae_restrict_iff'₀]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ NullMeasurableSet {x : α | f x ≠ 0} μ
have rcases : ∀ (g : α → ℝ≥0∞) (hg : Measurable g) (hfg : f =ᶠ[ae μ] g), NullMeasurableSet {x : α | f x ≠ 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 α
p : α → Prop
f g : α → ℝ≥0∞
hg : Measurable g
hfg : f =ᶠ[ae μ] g
⊢ {x : α | g x ≠ 0} =ᶠ[ae μ] {x : α | f x ≠ 0}
have h : ∀ (a : α) (ha : f a = g a), {x : α | g x ≠ 0} a = {x : α | f 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 α
p : α → Prop
f g : α → ℝ≥0∞
hg : Measurable g
hfg : f =ᶠ[ae μ] g
a : α
ha : f a = g a
⊢ {x : α | g x ≠ 0} a = {x : α | f x ≠ 0} a
have h : {x : α | g x ≠ 0} a ↔ {x : α | f x ≠ 0} a
Tactic: simp only [eq_iff_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
f g : α → ℝ≥0∞
hg : Measurable g
hfg : f =ᶠ[ae μ] g
a : α
ha : f a = g a
h : g a ≠ 0
⊢ {x : α | f x ≠ 0} a
have rwa : ∀ (h : f a ≠ 0), {x : α | f x ≠ 0} a
Tactic: rwa [← ha] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
f g : α → ℝ≥0∞
hg : Measurable g
hfg : f =ᶠ[ae μ] g
a : α
ha : f a = g a
h : f a ≠ 0
⊢ {x : α | g x ≠ 0} a
have rwa : ∀ (h : g a ≠ 0), {x : α | g x ≠ 0} a
Tactic: rwa [ha] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
f g : α → ℝ≥0∞
hg : Measurable g
hfg : f =ᶠ[ae μ] g
⊢ NullMeasurableSet {x : α | f x ≠ 0} μ
have nonneg_eq_ae : {x : α | g x ≠ 0} =ᶠ[ae μ] {x : α | f x ≠ 0}
Tactic: have nonneg_eq_ae : {x | g x ≠ 0} =ᵐ[μ] {x | f x ≠ 0} := by
      filter_upwards [hfg] with a ha
      simp only [eq_iff_iff]
      exact ⟨fun (h : g a ≠ 0) ↦ by rwa [← ha] at h,
             fun (h : f a ≠ 0) ↦ by rwa [ha] at h⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
⊢ AEMeasurable g (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) ↔
    AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ (↑(f x) : ℝ≥0∞) * g x) μ
have t : ∃ (f' : α → ℝ≥0), Measurable f' ∧ f =ᶠ[ae μ] f'
Tactic: have t : ∃ f', Measurable f' ∧ f =ᵐ[μ] f' := hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
t : ∃ (f' : α → ℝ≥0), Measurable f' ∧ f =ᶠ[ae μ] f'
⊢ AEMeasurable g (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) ↔
    AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ (↑(f x) : ℝ≥0∞) * g x) μ
have rcases : ∀ (f' : α → ℝ≥0) (hf'_m : Measurable f') (hf'_ae : f =ᶠ[ae μ] f'),
  AEMeasurable g (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) ↔
    AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ (↑(f x) : ℝ≥0∞) * g x) μ
Tactic: rcases t with ⟨f', hf'_m, hf'_ae⟩
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᶠ[ae μ] f'
⊢ AEMeasurable g (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) ↔
    AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ (↑(f x) : ℝ≥0∞) * g x) μ
have mp : AEMeasurable g (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) →
  AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ (↑(f x) : ℝ≥0∞) * g x) μ
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᶠ[ae μ] f'
mp :
  AEMeasurable g (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) →
    AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ (↑(f x) : ℝ≥0∞) * g x) μ
⊢ AEMeasurable g (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) ↔
    AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ (↑(f x) : ℝ≥0∞) * g x) μ
have mpr : AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ (↑(f x) : ℝ≥0∞) * g x) μ →
  AEMeasurable g (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᶠ[ae μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] g'
⊢ AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ (↑(f x) : ℝ≥0∞) * g x) μ
have A : MeasurableSet.{u_1} (α := α) {x : α | f' x ≠ 0}
Tactic: have A : MeasurableSet {x | f' x ≠ 0} := hf'_m (measurableSet_singleton _).compl
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᶠ[ae μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] g'
A : MeasurableSet.{u_1} (α := α) {x : α | f' x ≠ 0}
⊢ AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ (↑(f x) : ℝ≥0∞) * g x) μ
have mp : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (↑(f x) : ℝ≥0∞) * g x) fun (x : α) ↦ (↑(f' x) : ℝ≥0∞) * g' x
Tactic: refine ⟨fun x => f' x * g' x, hf'_m.coe_nnreal_ennreal.smul g'meas, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᶠ[ae μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] g'
A : MeasurableSet.{u_1} (α := α) {x : α | f' x ≠ 0}
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (↑(f x) : ℝ≥0∞) * g x) fun (x : α) ↦ (↑(f' x) : ℝ≥0∞) * g' x
have mp : ∀ᵐ (x : α) ∂μ.restrict {x : α | f' x ≠ 0},
  Eq (α := ℝ≥0∞) ((fun (x : α) ↦ (↑(f x) : ℝ≥0∞) * g x) x) ((fun (x : α) ↦ (↑(f' x) : ℝ≥0∞) * g' x) x)
Tactic: apply ae_of_ae_restrict_of_ae_restrict_compl { x | f' x ≠ 0 }
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᶠ[ae μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] g'
A : MeasurableSet.{u_1} (α := α) {x : α | f' x ≠ 0}
mp :
  ∀ᵐ (x : α) ∂μ.restrict {x : α | f' x ≠ 0},
    Eq (α := ℝ≥0∞) ((fun (x : α) ↦ (↑(f x) : ℝ≥0∞) * g x) x) ((fun (x : α) ↦ (↑(f' x) : ℝ≥0∞) * g' x) x)
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (↑(f x) : ℝ≥0∞) * g x) fun (x : α) ↦ (↑(f' x) : ℝ≥0∞) * g' x
have mp₁ : ∀ᵐ (x : α) ∂μ.restrict {x : α | f' x ≠ 0}ᶜ,
  Eq (α := ℝ≥0∞) ((fun (x : α) ↦ (↑(f x) : ℝ≥0∞) * g x) x) ((fun (x : α) ↦ (↑(f' x) : ℝ≥0∞) * g' x) x)
Tactic: apply ae_of_ae_restrict_of_ae_restrict_compl { x | f' x ≠ 0 }
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᶠ[ae μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] g'
A : MeasurableSet.{u_1} (α := α) {x : α | f' x ≠ 0}
⊢ ∀ᵐ (x : α) ∂μ.restrict {x : α | f' x ≠ 0},
    Eq (α := ℝ≥0∞) ((fun (x : α) ↦ (↑(f x) : ℝ≥0∞) * g x) x) ((fun (x : α) ↦ (↑(f' x) : ℝ≥0∞) * g' x) x)
have hg'₁ : ∀ᵐ (x : α) ∂μ, (↑(f x) : ℝ≥0∞) ≠ 0 → g x = g' x
Tactic: rw [EventuallyEq, ae_withDensity_iff' hf.coe_nnreal_ennreal] at hg'
Cleared hypotheses: hg', A
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᶠ[ae μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : ∀ᵐ (x : α) ∂μ, (↑(f x) : ℝ≥0∞) ≠ 0 → g x = g' x
A : MeasurableSet.{u_1} (α := α) {x : α | f' x ≠ 0}
⊢ ∀ᵐ (x : α) ∂μ.restrict {x : α | f' x ≠ 0},
    Eq (α := ℝ≥0∞) ((fun (x : α) ↦ (↑(f x) : ℝ≥0∞) * g x) x) ((fun (x : α) ↦ (↑(f' x) : ℝ≥0∞) * g' x) x)
have mp : ∀ᵐ (x : α) ∂μ,
  Membership.mem (γ := Set α) {x : α | f' x ≠ 0} x →
    Eq (α := ℝ≥0∞) ((fun (x : α) ↦ (↑(f x) : ℝ≥0∞) * g x) x) ((fun (x : α) ↦ (↑(f' x) : ℝ≥0∞) * g' x) x)
Tactic: rw [ae_restrict_iff' A]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᶠ[ae μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : ∀ᵐ (x : α) ∂μ, (↑(f x) : ℝ≥0∞) ≠ 0 → g x = g' x
A : MeasurableSet.{u_1} (α := α) {x : α | f' x ≠ 0}
⊢ ∀ᵐ (x : α) ∂μ,
    Membership.mem (γ := Set α) {x : α | f' x ≠ 0} x →
      Eq (α := ℝ≥0∞) ((fun (x : α) ↦ (↑(f x) : ℝ≥0∞) * g x) x) ((fun (x : α) ↦ (↑(f' x) : ℝ≥0∞) * g' x) x)
have h : ∀ (a : α) (ha : (↑(f a) : ℝ≥0∞) ≠ 0 → g a = g' a) (h'a : f a = f' a) (h_a_nonneg : f' a ≠ 0),
  (↑(f a) : ℝ≥0∞) * g a = (↑(f' a) : ℝ≥0∞) * g' a
Tactic: filter_upwards [hg', hf'_ae] with a ha h'a h_a_nonneg
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᶠ[ae μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : ∀ᵐ (x : α) ∂μ, (↑(f x) : ℝ≥0∞) ≠ 0 → g x = g' x
A : MeasurableSet.{u_1} (α := α) {x : α | f' x ≠ 0}
a : α
ha : (↑(f a) : ℝ≥0∞) ≠ 0 → g a = g' a
h'a : f a = f' a
h_a_nonneg : f' a ≠ 0
⊢ (↑(f a) : ℝ≥0∞) * g a = (↑(f' a) : ℝ≥0∞) * g' a
have this : (↑(f' a) : ℝ≥0∞) ≠ 0
Tactic: have : (f' a : ℝ≥0∞) ≠ 0 := by simpa only [Ne, ENNReal.coe_eq_zero] using h_a_nonneg
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᶠ[ae μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : ∀ᵐ (x : α) ∂μ, (↑(f x) : ℝ≥0∞) ≠ 0 → g x = g' x
A : MeasurableSet.{u_1} (α := α) {x : α | f' x ≠ 0}
a : α
ha : (↑(f a) : ℝ≥0∞) ≠ 0 → g a = g' a
h'a : f a = f' a
h_a_nonneg : f' a ≠ 0
this : (↑(f' a) : ℝ≥0∞) ≠ 0
⊢ (↑(f a) : ℝ≥0∞) * g a = (↑(f' a) : ℝ≥0∞) * g' a
have h : ∀ (this : (↑(f a) : ℝ≥0∞) ≠ 0), (↑(f a) : ℝ≥0∞) * g a = (↑(f a) : ℝ≥0∞) * g' a
Tactic: rw [← h'a] at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᶠ[ae μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : ∀ᵐ (x : α) ∂μ, (↑(f x) : ℝ≥0∞) ≠ 0 → g x = g' x
A : MeasurableSet.{u_1} (α := α) {x : α | f' x ≠ 0}
a : α
ha : (↑(f a) : ℝ≥0∞) ≠ 0 → g a = g' a
h'a : f a = f' a
h_a_nonneg : f' a ≠ 0
this : (↑(f a) : ℝ≥0∞) ≠ 0
⊢ (↑(f a) : ℝ≥0∞) * g a = (↑(f a) : ℝ≥0∞) * g' a
have h : (↑(f a) : ℝ≥0∞) * g' a = (↑(f a) : ℝ≥0∞) * g' a
Tactic: rw [ha this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᶠ[ae μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] g'
A : MeasurableSet.{u_1} (α := α) {x : α | f' x ≠ 0}
⊢ ∀ᵐ (x : α) ∂μ.restrict {x : α | f' x ≠ 0}ᶜ,
    Eq (α := ℝ≥0∞) ((fun (x : α) ↦ (↑(f x) : ℝ≥0∞) * g x) x) ((fun (x : α) ↦ (↑(f' x) : ℝ≥0∞) * g' x) x)
have mp : ∀ᵐ (x : α) ∂μ,
  Membership.mem (γ := Set α) {x : α | f' x ≠ 0}ᶜ x →
    Eq (α := ℝ≥0∞) ((fun (x : α) ↦ (↑(f x) : ℝ≥0∞) * g x) x) ((fun (x : α) ↦ (↑(f' x) : ℝ≥0∞) * g' x) x)
Tactic: rw [ae_restrict_iff' A.compl]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᶠ[ae μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] g'
A : MeasurableSet.{u_1} (α := α) {x : α | f' x ≠ 0}
⊢ ∀ᵐ (x : α) ∂μ,
    Membership.mem (γ := Set α) {x : α | f' x ≠ 0}ᶜ x →
      Eq (α := ℝ≥0∞) ((fun (x : α) ↦ (↑(f x) : ℝ≥0∞) * g x) x) ((fun (x : α) ↦ (↑(f' x) : ℝ≥0∞) * g' x) x)
have h : ∀ (a : α) (ha : f a = f' a) (ha_null : Membership.mem (γ := Set α) {x : α | f' x ≠ 0}ᶜ a),
  (↑(f a) : ℝ≥0∞) * g a = (↑(f' a) : ℝ≥0∞) * g' a
Tactic: filter_upwards [hf'_ae] with a ha ha_null
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᶠ[ae μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] g'
A : MeasurableSet.{u_1} (α := α) {x : α | f' x ≠ 0}
a : α
ha : f a = f' a
ha_null : Membership.mem (γ := Set α) {x : α | f' x ≠ 0}ᶜ a
⊢ (↑(f a) : ℝ≥0∞) * g a = (↑(f' a) : ℝ≥0∞) * g' a
have ha_null₁ : f' a = 0
Tactic: have ha_null : f' a = 0 := Function.notMem_support.mp ha_null
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᶠ[ae μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] g'
A : MeasurableSet.{u_1} (α := α) {x : α | f' x ≠ 0}
a : α
ha : f a = f' a
ha_null_1 : Membership.mem (γ := Set α) {x : α | f' x ≠ 0}ᶜ a
ha_null : f' a = 0
⊢ (↑(f a) : ℝ≥0∞) * g a = (↑(f' a) : ℝ≥0∞) * g' a
have h : ∀ (ha : f a = 0) (ha_null : Membership.mem (γ := Set α) {x : α | f' x ≠ 0}ᶜ a) (ha_null : f' a = 0),
  (↑(f a) : ℝ≥0∞) * g a = (↑0 : ℝ≥0∞) * g' a
Tactic: rw [ha_null] at ha ⊢
Cleared hypotheses: ha, ha_null_1, ha_null
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᶠ[ae μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] g'
A : MeasurableSet.{u_1} (α := α) {x : α | f' x ≠ 0}
a : α
ha : f a = 0
ha_null_1 : Membership.mem (γ := Set α) {x : α | f' x ≠ 0}ᶜ a
ha_null : f' a = 0
⊢ (↑(f a) : ℝ≥0∞) * g a = (↑0 : ℝ≥0∞) * g' a
have h : (↑0 : ℝ≥0∞) * g a = (↑0 : ℝ≥0∞) * g' a
Tactic: rw [ha]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᶠ[ae μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : (fun (x : α) ↦ (↑(f x) : ℝ≥0∞) * g x) =ᶠ[ae μ] g'
⊢ AEMeasurable g (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))
have mpr : g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] fun (x : α) ↦ (↑(f' x) : ℝ≥0∞)⁻¹ * g' x
Tactic: refine ⟨fun x => ((f' x)⁻¹ : ℝ≥0∞) * g' x, hf'_m.coe_nnreal_ennreal.inv.smul g'meas, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᶠ[ae μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : (fun (x : α) ↦ (↑(f x) : ℝ≥0∞) * g x) =ᶠ[ae μ] g'
⊢ g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] fun (x : α) ↦ (↑(f' x) : ℝ≥0∞)⁻¹ * g' x
have mpr : ∀ᵐ (x : α) ∂μ, (↑(f x) : ℝ≥0∞) ≠ 0 → g x = (↑(f' x) : ℝ≥0∞)⁻¹ * g' x
Tactic: rw [EventuallyEq, ae_withDensity_iff' hf.coe_nnreal_ennreal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᶠ[ae μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : (fun (x : α) ↦ (↑(f x) : ℝ≥0∞) * g x) =ᶠ[ae μ] g'
⊢ ∀ᵐ (x : α) ∂μ, (↑(f x) : ℝ≥0∞) ≠ 0 → g x = (↑(f' x) : ℝ≥0∞)⁻¹ * g' x
have h : ∀ (a : α) (hfga : (↑(f a) : ℝ≥0∞) * g a = g' a) (hff'a : f a = f' a) (h'a : (↑(f a) : ℝ≥0∞) ≠ 0),
  g a = (↑(f' a) : ℝ≥0∞)⁻¹ * g' a
Tactic: filter_upwards [hg', hf'_ae] with a hfga hff'a h'a
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᶠ[ae μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : (fun (x : α) ↦ (↑(f x) : ℝ≥0∞) * g x) =ᶠ[ae μ] g'
a : α
hfga : (↑(f a) : ℝ≥0∞) * g a = g' a
hff'a : f a = f' a
h'a : (↑(f a) : ℝ≥0∞) ≠ 0
⊢ g a = (↑(f' a) : ℝ≥0∞)⁻¹ * g' a
have hfga₁ : (↑(f' a) : ℝ≥0∞) * g a = g' a
Tactic: rw [hff'a] at hfga h'a
Cleared hypotheses: hfga, hff'a, h'a
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᶠ[ae μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : (fun (x : α) ↦ (↑(f x) : ℝ≥0∞) * g x) =ᶠ[ae μ] g'
a : α
hfga : (↑(f a) : ℝ≥0∞) * g a = g' a
hff'a : f a = f' a
h'a : (↑(f a) : ℝ≥0∞) ≠ 0
hfga₁ : (↑(f' a) : ℝ≥0∞) * g a = g' a
hff'a₁ : f a = f' a
⊢ g a = (↑(f' a) : ℝ≥0∞)⁻¹ * g' a
have h'a₁ : (↑(f' a) : ℝ≥0∞) ≠ 0
Tactic: rw [hff'a] at hfga h'a
Cleared hypotheses: hfga, hff'a, h'a
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᶠ[ae μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : (fun (x : α) ↦ (↑(f x) : ℝ≥0∞) * g x) =ᶠ[ae μ] g'
a : α
hfga : (↑(f' a) : ℝ≥0∞) * g a = g' a
hff'a : f a = f' a
h'a : (↑(f' a) : ℝ≥0∞) ≠ 0
⊢ g a = (↑(f' a) : ℝ≥0∞)⁻¹ * g' a
have h : g a = (↑(f' a) : ℝ≥0∞)⁻¹ * ((↑(f' a) : ℝ≥0∞) * g a)
Tactic: rw [← hfga, ← mul_assoc, ENNReal.inv_mul_cancel h'a ENNReal.coe_ne_top, one_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᶠ[ae μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : (fun (x : α) ↦ (↑(f x) : ℝ≥0∞) * g x) =ᶠ[ae μ] g'
a : α
hfga : (↑(f' a) : ℝ≥0∞) * g a = g' a
hff'a : f a = f' a
h'a : (↑(f' a) : ℝ≥0∞) ≠ 0
h : g a = (↑(f' a) : ℝ≥0∞)⁻¹ * ((↑(f' a) : ℝ≥0∞) * g a)
⊢ g a = (↑(f' a) : ℝ≥0∞)⁻¹ * g' a
have h₁ : g a = (↑(f' a) : ℝ≥0∞)⁻¹ * (↑(f' a) : ℝ≥0∞) * g a
Tactic: rw [← hfga, ← mul_assoc, ENNReal.inv_mul_cancel h'a ENNReal.coe_ne_top, one_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᶠ[ae μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : (fun (x : α) ↦ (↑(f x) : ℝ≥0∞) * g x) =ᶠ[ae μ] g'
a : α
hfga : (↑(f' a) : ℝ≥0∞) * g a = g' a
hff'a : f a = f' a
h'a : (↑(f' a) : ℝ≥0∞) ≠ 0
h : g a = (↑(f' a) : ℝ≥0∞)⁻¹ * ((↑(f' a) : ℝ≥0∞) * g a)
h₁ : g a = (↑(f' a) : ℝ≥0∞)⁻¹ * (↑(f' a) : ℝ≥0∞) * g a
⊢ g a = (↑(f' a) : ℝ≥0∞)⁻¹ * g' a
have h₂ : g a = 1 * g a
Tactic: rw [← hfga, ← mul_assoc, ENNReal.inv_mul_cancel h'a ENNReal.coe_ne_top, one_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᶠ[ae μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : (fun (x : α) ↦ (↑(f x) : ℝ≥0∞) * g x) =ᶠ[ae μ] g'
a : α
hfga : (↑(f' a) : ℝ≥0∞) * g a = g' a
hff'a : f a = f' a
h'a : (↑(f' a) : ℝ≥0∞) ≠ 0
h : g a = (↑(f' a) : ℝ≥0∞)⁻¹ * ((↑(f' a) : ℝ≥0∞) * g a)
h₁ : g a = (↑(f' a) : ℝ≥0∞)⁻¹ * (↑(f' a) : ℝ≥0∞) * g a
h₂ : g a = 1 * g a
⊢ g a = (↑(f' a) : ℝ≥0∞)⁻¹ * g' a
have h₃ : g a = g a
Tactic: rw [← hfga, ← mul_assoc, ENNReal.inv_mul_cancel h'a ENNReal.coe_ne_top, one_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
a : α
⊢ withDensity (dirac a) f = HSMul.hSMul (β := Measure α) (f a) (dirac a)
have h : ∀ (s : Set α) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) (((withDensity (dirac a) f : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((HSMul.hSMul (β := Measure α) (f a) (dirac a) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
inst : MeasurableSingletonClass α
f : α → ℝ≥0∞
a : α
⊢ withDensity (dirac a) f = HSMul.hSMul (β := Measure α) (f a) (dirac a)
have h : ∀ (s : Set α) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) (((withDensity (dirac a) f : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((HSMul.hSMul (β := Measure α) (f a) (dirac a) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
⊢ ∀ {g : α → ℝ≥0∞}, Measurable g → ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ
have indicator : ∀ (c : ℝ≥0∞) ⦃s : Set α⦄,
  MeasurableSet s →
    ∫⁻ (a : α), s.indicator (fun (x : α) ↦ c) a ∂μ.withDensity f =
      ∫⁻ (a : α), HMul.hMul (β := α → ℝ≥0∞) f (s.indicator fun (x : α) ↦ c) a ∂μ
Tactic: apply Measurable.ennreal_induction
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
indicator :
  ∀ (c : ℝ≥0∞) ⦃s : Set α⦄,
    MeasurableSet s →
      ∫⁻ (a : α), s.indicator (fun (x : α) ↦ c) a ∂μ.withDensity f =
        ∫⁻ (a : α), HMul.hMul (β := α → ℝ≥0∞) f (s.indicator fun (x : α) ↦ c) a ∂μ
⊢ ∀ {g : α → ℝ≥0∞}, Measurable g → ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ
have add : ∀ ⦃f_1 g : α → ℝ≥0∞⦄,
  Disjoint (Function.support f_1) (Function.support g) →
    Measurable f_1 →
      Measurable g →
        ∫⁻ (a : α), f_1 a ∂μ.withDensity f = ∫⁻ (a : α), (f * f_1) a ∂μ →
          ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ →
            ∫⁻ (a : α), (f_1 + g) a ∂μ.withDensity f = ∫⁻ (a : α), (f * (f_1 + g)) a ∂μ
Tactic: apply Measurable.ennreal_induction