awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
A : (fun (x : α) ↦ (f x)⁻¹ * i x) ≤ g
x : α
h'x : f x < ∞
hx : f x ≠ 0
⊢ i x = f x * ((f x)⁻¹ * i x)
have rw : i x = f x * (f x)⁻¹ * i x
Tactic: rw [← mul_assoc, ENNReal.mul_inv_cancel hx h'x.ne, one_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
A : (fun (x : α) ↦ (f x)⁻¹ * i x) ≤ g
x : α
h'x : f x < ∞
hx : f x ≠ 0
rw : i x = f x * (f x)⁻¹ * i x
⊢ i x = f x * ((f x)⁻¹ * i x)
have rw₁ : i x = 1 * i x
Tactic: rw [← mul_assoc, ENNReal.mul_inv_cancel hx h'x.ne, one_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
A : (fun (x : α) ↦ (f x)⁻¹ * i x) ≤ g
x : α
h'x : f x < ∞
hx : f x ≠ 0
rw : i x = f x * (f x)⁻¹ * i x
rw₁ : i x = 1 * i x
⊢ i x = f x * ((f x)⁻¹ * i x)
have rw₂ : i x = i x
Tactic: rw [← mul_assoc, ENNReal.mul_inv_cancel hx h'x.ne, one_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ.restrict s, f x < ∞
⊢ ∫⁻ (a : α) in s, g a ∂μ.withDensity f = ∫⁻ (a : α) in s, (f * g) a ∂μ
have rw : ∫⁻ (a : α), g a ∂(μ.restrict s).withDensity f = ∫⁻ (a : α) in s, (f * g) a ∂μ
Tactic: rw [restrict_withDensity hs, lintegral_withDensity_eq_lintegral_mul_non_measurable _ f_meas hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ.restrict s, f x < ∞
rw : ∫⁻ (a : α), g a ∂(μ.restrict s).withDensity f = ∫⁻ (a : α) in s, (f * g) a ∂μ
⊢ ∫⁻ (a : α) in s, g a ∂μ.withDensity f = ∫⁻ (a : α) in s, (f * g) a ∂μ
have rw₁ : ∫⁻ (a : α) in s, (f * g) a ∂μ = ∫⁻ (a : α) in s, (f * g) a ∂μ
Tactic: rw [restrict_withDensity hs, lintegral_withDensity_eq_lintegral_mul_non_measurable _ f_meas hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
⊢ ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), g a ∂μ.withDensity f'
have rw : ∫⁻ (a : α), g a ∂μ.withDensity (AEMeasurable.mk f hf) = ∫⁻ (a : α), g a ∂μ.withDensity f'
Tactic: rw [withDensity_congr_ae hf.ae_eq_mk]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
⊢ ∫⁻ (a : α), g a ∂μ.withDensity f' = ∫⁻ (a : α), (f' * g) a ∂μ
have hf₁ : ∀ᵐ (x : α) ∂μ, AEMeasurable.mk f hf x < ∞
Tactic: apply lintegral_withDensity_eq_lintegral_mul_non_measurable _ hf.measurable_mk
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
⊢ ∀ᵐ (x : α) ∂μ, AEMeasurable.mk f hf x < ∞
have h : ∀ (a : α), f a < ∞ → f a = AEMeasurable.mk f hf a → AEMeasurable.mk f hf a < ∞
Tactic: filter_upwards [h'f, hf.ae_eq_mk]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
⊢ ∫⁻ (a : α), (f' * g) a ∂μ = ∫⁻ (a : α), (f * g) a ∂μ
have h : f' * g =ᶠ[ae μ] f * g
Tactic: apply lintegral_congr_ae
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
⊢ f' * g =ᶠ[ae μ] f * g
have h : ∀ (a : α), f a = AEMeasurable.mk f hf a → (f' * g) a = (f * g) a
Tactic: filter_upwards [hf.ae_eq_mk]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
⊢ ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ
have g₁ : ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), g a ∂μ.withDensity f'
Tactic: calc
    ∫⁻ a, g a ∂μ.withDensity f = ∫⁻ a, g a ∂μ.withDensity f' := by
      rw [withDensity_congr_ae hf.ae_eq_mk]
    _ = ∫⁻ a, (f' * g) a ∂μ := by
      apply lintegral_withDensity_eq_lintegral_mul_non_measurable _ hf.measurable_mk
      filter_upwards [h'f, hf.ae_eq_mk]
      intro x hx h'x
      rwa [← h'x]
    _ = ∫⁻ a, (f * g) a ∂μ := by
      apply lintegral_congr_ae
      filter_upwards [hf.ae_eq_mk]
      intro x hx
      simp only [f', hx, Pi.mul_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
g₁ : ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), g a ∂μ.withDensity f'
⊢ ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ
have g₂ : ∫⁻ (a : α), g a ∂μ.withDensity f' = ∫⁻ (a : α), (f' * g) a ∂μ
Tactic: calc
    ∫⁻ a, g a ∂μ.withDensity f = ∫⁻ a, g a ∂μ.withDensity f' := by
      rw [withDensity_congr_ae hf.ae_eq_mk]
    _ = ∫⁻ a, (f' * g) a ∂μ := by
      apply lintegral_withDensity_eq_lintegral_mul_non_measurable _ hf.measurable_mk
      filter_upwards [h'f, hf.ae_eq_mk]
      intro x hx h'x
      rwa [← h'x]
    _ = ∫⁻ a, (f * g) a ∂μ := by
      apply lintegral_congr_ae
      filter_upwards [hf.ae_eq_mk]
      intro x hx
      simp only [f', hx, Pi.mul_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
g₁ : ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), g a ∂μ.withDensity f'
g₂ : ∫⁻ (a : α), g a ∂μ.withDensity f' = ∫⁻ (a : α), (f' * g) a ∂μ
⊢ ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ
have g₃ : ∫⁻ (a : α), (f' * g) a ∂μ = ∫⁻ (a : α), (f * g) a ∂μ
Tactic: calc
    ∫⁻ a, g a ∂μ.withDensity f = ∫⁻ a, g a ∂μ.withDensity f' := by
      rw [withDensity_congr_ae hf.ae_eq_mk]
    _ = ∫⁻ a, (f' * g) a ∂μ := by
      apply lintegral_withDensity_eq_lintegral_mul_non_measurable _ hf.measurable_mk
      filter_upwards [h'f, hf.ae_eq_mk]
      intro x hx h'x
      rwa [← h'x]
    _ = ∫⁻ a, (f * g) a ∂μ := by
      apply lintegral_congr_ae
      filter_upwards [hf.ae_eq_mk]
      intro x hx
      simp only [f', hx, Pi.mul_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f (μ.restrict s)
g : α → ℝ≥0∞
hs : MeasurableSet s
h'f : ∀ᵐ (x : α) ∂μ.restrict s, f x < ∞
⊢ ∫⁻ (a : α) in s, g a ∂μ.withDensity f = ∫⁻ (a : α) in s, (f * g) a ∂μ
have rw : ∫⁻ (a : α), g a ∂(μ.restrict s).withDensity f = ∫⁻ (a : α) in s, (f * g) a ∂μ
Tactic: rw [restrict_withDensity hs, lintegral_withDensity_eq_lintegral_mul_non_measurable₀ _ hf h'f]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f (μ.restrict s)
g : α → ℝ≥0∞
hs : MeasurableSet s
h'f : ∀ᵐ (x : α) ∂μ.restrict s, f x < ∞
rw : ∫⁻ (a : α), g a ∂(μ.restrict s).withDensity f = ∫⁻ (a : α) in s, (f * g) a ∂μ
⊢ ∫⁻ (a : α) in s, g a ∂μ.withDensity f = ∫⁻ (a : α) in s, (f * g) a ∂μ
have rw₁ : ∫⁻ (a : α) in s, (f * g) a ∂μ = ∫⁻ (a : α) in s, (f * g) a ∂μ
Tactic: rw [restrict_withDensity hs, lintegral_withDensity_eq_lintegral_mul_non_measurable₀ _ hf h'f]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f (μ.restrict s)
g : α → ℝ≥0∞
h'f : ∀ᵐ (x : α) ∂μ.restrict s, f x < ∞
⊢ ∫⁻ (a : α) in s, g a ∂μ.withDensity f = ∫⁻ (a : α) in s, (f * g) a ∂μ
have rw : ∫⁻ (a : α), g a ∂(μ.restrict s).withDensity f = ∫⁻ (a : α) in s, (f * g) a ∂μ
Tactic: rw [restrict_withDensity' s, lintegral_withDensity_eq_lintegral_mul_non_measurable₀ _ hf h'f]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f (μ.restrict s)
g : α → ℝ≥0∞
h'f : ∀ᵐ (x : α) ∂μ.restrict s, f x < ∞
rw : ∫⁻ (a : α), g a ∂(μ.restrict s).withDensity f = ∫⁻ (a : α) in s, (f * g) a ∂μ
⊢ ∫⁻ (a : α) in s, g a ∂μ.withDensity f = ∫⁻ (a : α) in s, (f * g) a ∂μ
have rw₁ : ∫⁻ (a : α) in s, (f * g) a ∂μ = ∫⁻ (a : α) in s, (f * g) a ∂μ
Tactic: rw [restrict_withDensity' s, lintegral_withDensity_eq_lintegral_mul_non_measurable₀ _ hf h'f]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ μ.withDensity (f * g) = (μ.withDensity f).withDensity g
have h : ∀ (s : Set α) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((μ.withDensity (f * g) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((μ.withDensity f).withDensity g : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext1 s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity (f * g) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((μ.withDensity f).withDensity g : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have h : ∫⁻ (a : α) in s, (f * g) a ∂μ = ((μ.withDensity f).withDensity g : (a : Set α) → ℝ≥0∞) s
Tactic: rw [withDensity_apply _ hs, withDensity_apply _ hs, restrict_withDensity hs,
    lintegral_withDensity_eq_lintegral_mul₀ hf.restrict hg.restrict]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
s : Set α
hs : MeasurableSet s
h : ∫⁻ (a : α) in s, (f * g) a ∂μ = ((μ.withDensity f).withDensity g : (a : Set α) → ℝ≥0∞) s
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity (f * g) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((μ.withDensity f).withDensity g : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : ∫⁻ (a : α) in s, (f * g) a ∂μ = ∫⁻ (a : α) in s, g a ∂μ.withDensity f
Tactic: rw [withDensity_apply _ hs, withDensity_apply _ hs, restrict_withDensity hs,
    lintegral_withDensity_eq_lintegral_mul₀ hf.restrict hg.restrict]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
s : Set α
hs : MeasurableSet s
h : ∫⁻ (a : α) in s, (f * g) a ∂μ = ((μ.withDensity f).withDensity g : (a : Set α) → ℝ≥0∞) s
h₁ : ∫⁻ (a : α) in s, (f * g) a ∂μ = ∫⁻ (a : α) in s, g a ∂μ.withDensity f
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity (f * g) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((μ.withDensity f).withDensity g : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have h₂ : ∫⁻ (a : α) in s, (f * g) a ∂μ = ∫⁻ (a : α), g a ∂(μ.restrict s).withDensity f
Tactic: rw [withDensity_apply _ hs, withDensity_apply _ hs, restrict_withDensity hs,
    lintegral_withDensity_eq_lintegral_mul₀ hf.restrict hg.restrict]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
s : Set α
hs : MeasurableSet s
h : ∫⁻ (a : α) in s, (f * g) a ∂μ = ((μ.withDensity f).withDensity g : (a : Set α) → ℝ≥0∞) s
h₁ : ∫⁻ (a : α) in s, (f * g) a ∂μ = ∫⁻ (a : α) in s, g a ∂μ.withDensity f
h₂ : ∫⁻ (a : α) in s, (f * g) a ∂μ = ∫⁻ (a : α), g a ∂(μ.restrict s).withDensity f
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity (f * g) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((μ.withDensity f).withDensity g : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have h₃ : ∫⁻ (a : α) in s, (f * g) a ∂μ = ∫⁻ (a : α) in s, (f * g) a ∂μ
Tactic: rw [withDensity_apply _ hs, withDensity_apply _ hs, restrict_withDensity hs,
    lintegral_withDensity_eq_lintegral_mul₀ hf.restrict hg.restrict]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ ((μ.withDensity f).withDensity fun (x : α) ↦ (f x)⁻¹) ≤ μ
have rw : μ.withDensity (f * fun (x : α) ↦ (f x)⁻¹) ≤ μ
Tactic: rw [← withDensity_mul₀ hf hf.inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
this : (f * fun (x : α) ↦ (f x)⁻¹) ≤ᶠ[ae μ] 1
⊢ μ.withDensity (f * fun (x : α) ↦ (f x)⁻¹) ≤ μ
have refine : μ.withDensity 1 ≤ μ
Tactic: refine (withDensity_mono this).trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
this : (f * fun (x : α) ↦ (f x)⁻¹) ≤ᶠ[ae μ] 1
⊢ μ.withDensity 1 ≤ μ
have rw : μ ≤ μ
Tactic: rw [withDensity_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ μ.withDensity (f * fun (x : α) ↦ (f x)⁻¹) ≤ μ
have suffices : (f * fun (x : α) ↦ (f x)⁻¹) ≤ᶠ[ae μ] 1
Tactic: suffices (f * fun x ↦ (f x)⁻¹) ≤ᵐ[μ] 1 by
    refine (withDensity_mono this).trans ?_
    rw [withDensity_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ (f * fun (x : α) ↦ (f x)⁻¹) ≤ᶠ[ae μ] 1
have h : ∀ (x : α), HMul.hMul (β := (x : α) → ℝ≥0∞) f (fun (x : α) ↦ (f x)⁻¹) x ≤ 1 x
Tactic: filter_upwards with x
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_zero : ∀ᵐ (x : α) ∂μ, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
⊢ ((μ.withDensity f).withDensity fun (x : α) ↦ (f x)⁻¹) = μ
have rw : μ.withDensity (f * fun (x : α) ↦ (f x)⁻¹) = μ
Tactic: rw [← withDensity_mul₀ hf hf.inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_zero : ∀ᵐ (x : α) ∂μ, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
this : (f * fun (x : α) ↦ (f x)⁻¹) =ᶠ[ae μ] 1
⊢ μ.withDensity (f * fun (x : α) ↦ (f x)⁻¹) = μ
have rw : μ.withDensity 1 = μ
Tactic: rw [withDensity_congr_ae this, withDensity_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_zero : ∀ᵐ (x : α) ∂μ, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
this : (f * fun (x : α) ↦ (f x)⁻¹) =ᶠ[ae μ] 1
rw : μ.withDensity 1 = μ
⊢ μ.withDensity (f * fun (x : α) ↦ (f x)⁻¹) = μ
have rw₁ : μ = μ
Tactic: rw [withDensity_congr_ae this, withDensity_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_zero : ∀ᵐ (x : α) ∂μ, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
⊢ μ.withDensity (f * fun (x : α) ↦ (f x)⁻¹) = μ
have suffices : (f * fun (x : α) ↦ (f x)⁻¹) =ᶠ[ae μ] 1
Tactic: suffices (f * fun x ↦ (f x)⁻¹) =ᵐ[μ] 1 by
    rw [withDensity_congr_ae this, withDensity_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_zero : ∀ᵐ (x : α) ∂μ, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
⊢ (f * fun (x : α) ↦ (f x)⁻¹) =ᶠ[ae μ] 1
have h : ∀ (x : α) (hf_ne_zero : f x ≠ 0) (hf_ne_top : f x ≠ ∞),
  HMul.hMul (β := (x : α) → ℝ≥0∞) f (fun (x : α) ↦ (f x)⁻¹) x = 1 x
Tactic: filter_upwards [hf_ne_zero, hf_ne_top] with x hf_ne_zero hf_ne_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_zero_1 : ∀ᵐ (x : α) ∂μ, f x ≠ 0
hf_ne_top_1 : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
x : α
hf_ne_zero : f x ≠ 0
hf_ne_top : f x ≠ ∞
⊢ f x * (f x)⁻¹ = 1 x
have h : Eq (α := ℝ≥0∞) 1 (1 x)
Tactic: rw [ENNReal.mul_inv_cancel hf_ne_zero hf_ne_top, Pi.one_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_zero_1 : ∀ᵐ (x : α) ∂μ, f x ≠ 0
hf_ne_top_1 : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
x : α
hf_ne_zero : f x ≠ 0
hf_ne_top : f x ≠ ∞
h : Eq (α := ℝ≥0∞) 1 (1 x)
⊢ f x * (f x)⁻¹ = 1 x
have h₁ : Eq (α := ℝ≥0∞) 1 1
Tactic: rw [ENNReal.mul_inv_cancel hf_ne_zero hf_ne_top, Pi.one_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_zero : ∀ᵐ (x : α) ∂μ, f x ≠ 0
⊢ μ ≪ μ.withDensity f
have refine : ∀ (s : Set α) (hs : MeasurableSet s)
  (hμs : Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine Measure.AbsolutelyContinuous.mk (fun s hs hμs ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_zero : ∀ᵐ (x : α) ∂μ, f x ≠ 0
s : Set α
hs : MeasurableSet s
hμs : Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have hμs₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬s.indicator f a = 0 a} : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [withDensity_apply _ hs, lintegral_eq_zero_iff' hf.restrict,
    ae_eq_restrict_iff_indicator_ae_eq hs, Set.indicator_zero', Filter.EventuallyEq, ae_iff] at hμs
Cleared hypotheses: hμs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_zero : ∀ᵐ (x : α) ∂μ, f x ≠ 0
s : Set α
hs : MeasurableSet s
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬s.indicator f a = 0 a} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have hf_ne_zero₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | f a = 0} : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp only [ae_iff, ne_eq, not_not] at hf_ne_zero
Cleared hypotheses: hf_ne_zero
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
s : Set α
hs : MeasurableSet s
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬s.indicator f a = 0 a} : ℝ≥0∞) (0 : ℝ≥0∞)
hf_ne_zero : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | f a = 0} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have hμs₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | a ∈ s ∧ ¬f a = 0} : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp only [Pi.zero_apply, Set.indicator_apply_eq_zero, not_forall, exists_prop] at hμs
Cleared hypotheses: hμs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
s : Set α
hs : MeasurableSet s
hf_ne_zero : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | f a = 0} : ℝ≥0∞) (0 : ℝ≥0∞)
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | a ∈ s ∧ ¬f a = 0} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have hle : s ⊆ {a : α | a ∈ s ∧ ¬f a = 0} ∪ {a : α | f a = 0}
Tactic: have hle : s ⊆ {a | a ∈ s ∧ ¬f a = 0} ∪ {a | f a = 0} :=
    fun x hx ↦ or_iff_not_imp_right.mpr <| fun hnx ↦ ⟨hx, hnx⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f : α → ℝ≥0
⊢ SigmaFinite (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))
have refine_1 : ∀ (n : ℕ),
  LT.lt (α := ℝ≥0∞)
    ((μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞) : (a : Set α) → ℝ≥0∞)
        ((fun (n : ℕ) ↦ spanningSets μ n ∩ f ⁻¹' Iic (↑n : ℝ≥0)) n) :
      ℝ≥0∞)
    (∞ : ℝ≥0∞)
Tactic: refine ⟨⟨⟨fun n ↦ spanningSets μ n ∩ f ⁻¹' (Iic n), fun _ ↦ trivial, fun n ↦ ?_, ?_⟩⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f : α → ℝ≥0
refine_1 :
  ∀ (n : ℕ),
    LT.lt (α := ℝ≥0∞)
      ((μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞) : (a : Set α) → ℝ≥0∞)
          ((fun (n : ℕ) ↦ spanningSets μ n ∩ f ⁻¹' Iic (↑n : ℝ≥0)) n) :
        ℝ≥0∞)
      (∞ : ℝ≥0∞)
⊢ SigmaFinite (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))
have refine_2 : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), (fun (n : ℕ) ↦ spanningSets μ n ∩ f ⁻¹' Iic (↑n : ℝ≥0)) i) univ
Tactic: refine ⟨⟨⟨fun n ↦ spanningSets μ n ∩ f ⁻¹' (Iic n), fun _ ↦ trivial, fun n ↦ ?_, ?_⟩⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f : α → ℝ≥0
n : ℕ
⊢ LT.lt (α := ℝ≥0∞)
    ((μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞) : (a : Set α) → ℝ≥0∞)
        ((fun (n : ℕ) ↦ spanningSets μ n ∩ f ⁻¹' Iic (↑n : ℝ≥0)) n) :
      ℝ≥0∞)
    (∞ : ℝ≥0∞)
have refine_1 : ∫⁻ (a : α) in (fun (n : ℕ) ↦ spanningSets μ n ∩ f ⁻¹' Iic (↑n : ℝ≥0)) n, (↑(f a) : ℝ≥0∞) ∂μ < ∞
Tactic: rw [withDensity_apply']
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f : α → ℝ≥0
n : ℕ
⊢ ∫⁻ (a : α) in (fun (n : ℕ) ↦ spanningSets μ n ∩ f ⁻¹' Iic (↑n : ℝ≥0)) n, (↑(f a) : ℝ≥0∞) ∂μ < ∞
have refine_1 : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (n : ℕ) ↦ spanningSets μ n ∩ f ⁻¹' Iic (↑n : ℝ≥0)) n) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: apply setLIntegral_lt_top_of_bddAbove
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f : α → ℝ≥0
n : ℕ
refine_1 :
  Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (n : ℕ) ↦ spanningSets μ n ∩ f ⁻¹' Iic (↑n : ℝ≥0)) n) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
⊢ ∫⁻ (a : α) in (fun (n : ℕ) ↦ spanningSets μ n ∩ f ⁻¹' Iic (↑n : ℝ≥0)) n, (↑(f a) : ℝ≥0∞) ∂μ < ∞
have refine_1₁ : BddAbove (f '' (fun (n : ℕ) ↦ spanningSets μ n ∩ f ⁻¹' Iic (↑n : ℝ≥0)) n)
Tactic: apply setLIntegral_lt_top_of_bddAbove
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f : α → ℝ≥0
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), (fun (n : ℕ) ↦ spanningSets μ n ∩ f ⁻¹' Iic (↑n : ℝ≥0)) i) univ
have refine_2 : ∀ (x : α), ∃ (i : ℕ), x ∈ spanningSets μ i ∩ f ⁻¹' Iic (↑i : ℝ≥0)
Tactic: rw [iUnion_eq_univ_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f : α → ℝ≥0
⊢ ∀ (x : α), ∃ (i : ℕ), x ∈ spanningSets μ i ∩ f ⁻¹' Iic (↑i : ℝ≥0)
have refine_2 : ∀ (x : α), x ∈ spanningSets μ (max (spanningSetsIndex μ x) ⌈f x⌉₊)
Tactic: refine fun x ↦ ⟨max (spanningSetsIndex μ x) ⌈f x⌉₊, ?_, ?_⟩