awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
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
rw rw₁ : ∫⁻ (a : α), g a ∂μ.withDensity (AEMeasurable.mk f hf) = ∫⁻ (a : α), g a ∂μ.withDensity f'
⊢ ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), g a ∂μ.withDensity f'

Tactic:
rw [withDensity_congr_ae hf.ae_eq_mk]

Premises used: MeasureTheory.withDensity_congr_ae, AEMeasurable.ae_eq_mk
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
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
hf₁ : ∀ᵐ (x : α) ∂μ, AEMeasurable.mk f hf x < ∞
⊢ ∫⁻ (a : α), g a ∂μ.withDensity f' = ∫⁻ (a : α), (f' * g) a ∂μ

Tactic:
apply lintegral_withDensity_eq_lintegral_mul_non_measurable _ hf.measurable_mk

Premises used: MeasureTheory.lintegral_withDensity_eq_lintegral_mul_non_measurable, AEMeasurable.measurable_mk
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
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
h : ∀ (a : α), f a < ∞ → f a = AEMeasurable.mk f hf a → AEMeasurable.mk f hf a < ∞
⊢ ∀ᵐ (x : α) ∂μ, AEMeasurable.mk f hf x < ∞

Tactic:
filter_upwards [h'f, hf.ae_eq_mk]

Premises used: AEMeasurable.ae_eq_mk
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
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 : α
hx : f x < ∞
h'x : f x = AEMeasurable.mk f hf x
h h₁ h₂ h₃ : f x < ∞
⊢ AEMeasurable.mk f hf x < ∞

Tactic:
rwa [← h'x]
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
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
h : f' * g =ᶠ[ae μ] f * g
⊢ ∫⁻ (a : α), (f' * g) a ∂μ = ∫⁻ (a : α), (f * g) a ∂μ

Tactic:
apply lintegral_congr_ae

Premises used: MeasureTheory.lintegral_congr_ae
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
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
h : ∀ (a : α), f a = AEMeasurable.mk f hf a → (f' * g) a = (f * g) a
⊢ f' * g =ᶠ[ae μ] f * g

Tactic:
filter_upwards [hf.ae_eq_mk]

Premises used: AEMeasurable.ae_eq_mk
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
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 : α
hx : f x = AEMeasurable.mk f hf x
⊢ (f' * g) x = (f * g) x

Tactic:
simp only [f', hx, Pi.mul_apply]

Premises used: Pi.mul_apply
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
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 ∂μ
g₃ : ∫⁻ (a : α), (f' * g) a ∂μ = ∫⁻ (a : α), (f * g) a ∂μ
⊢ ∫⁻ (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]

Premises used: MeasureTheory.Measure.withDensity
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
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 ∂μ
rw₁ rw₂ : ∫⁻ (a : α) in s, (f * g) a ∂μ = ∫⁻ (a : α) in s, (f * g) a ∂μ
⊢ ∫⁻ (a : α) in s, g a ∂μ.withDensity f = ∫⁻ (a : α) in s, (f * g) a ∂μ

Tactic:
rw [restrict_withDensity hs, lintegral_withDensity_eq_lintegral_mul_non_measurable₀ _ hf h'f]

Premises used: MeasureTheory.lintegral_withDensity_eq_lintegral_mul_non_measurable₀, MeasureTheory.restrict_withDensity
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
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 ∂μ
rw₁ rw₂ : ∫⁻ (a : α) in s, (f * g) a ∂μ = ∫⁻ (a : α) in s, (f * g) a ∂μ
⊢ ∫⁻ (a : α) in s, g a ∂μ.withDensity f = ∫⁻ (a : α) in s, (f * g) a ∂μ

Tactic:
rw [restrict_withDensity' s, lintegral_withDensity_eq_lintegral_mul_non_measurable₀ _ hf h'f]

Premises used: MeasureTheory.lintegral_withDensity_eq_lintegral_mul_non_measurable₀, MeasureTheory.restrict_withDensity'
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
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∞)
⊢ μ.withDensity (f * g) = (μ.withDensity f).withDensity g

Tactic:
ext1 s hs
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
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
h₃ h₄ : ∫⁻ (a : α) in s, (f * g) a ∂μ = ∫⁻ (a : α) in s, (f * g) a ∂μ
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity (f * g) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((μ.withDensity f).withDensity g : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [withDensity_apply _ hs, withDensity_apply _ hs, restrict_withDensity hs,
    lintegral_withDensity_eq_lintegral_mul₀ hf.restrict hg.restrict]

Premises used: MeasureTheory.restrict_withDensity, AEMeasurable.restrict, MeasureTheory.lintegral_withDensity_eq_lintegral_mul₀, MeasureTheory.withDensity_apply
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
⊢ μ.withDensity (f * g) = (μ.withDensity f).withDensity g

Tactic:
withDensity_mul₀ hf.aemeasurable hg.aemeasurable

Premises used: Measurable.aemeasurable, MeasureTheory.withDensity_mul₀
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
rw : μ.withDensity (f * fun (x : α) ↦ (f x)⁻¹) ≤ μ
⊢ ((μ.withDensity f).withDensity fun (x : α) ↦ (f x)⁻¹) ≤ μ

Tactic:
rw [← withDensity_mul₀ hf hf.inv]

Premises used: MeasureTheory.withDensity_mul₀, AEMeasurable.inv
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
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)⁻¹) ≤ μ

Tactic:
(withDensity_mono this).trans ?_

Premises used: LE.le.trans, MeasureTheory.withDensity_mono
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
this : (f * fun (x : α) ↦ (f x)⁻¹) ≤ᶠ[ae μ] 1
refine : μ.withDensity 1 ≤ μ
⊢ μ.withDensity (f * fun (x : α) ↦ (f x)⁻¹) ≤ μ

Tactic:
refine (withDensity_mono this).trans ?_

Premises used: LE.le.trans, MeasureTheory.withDensity_mono
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
this : (f * fun (x : α) ↦ (f x)⁻¹) ≤ᶠ[ae μ] 1
rw rw₁ : μ ≤ μ
⊢ μ.withDensity 1 ≤ μ

Tactic:
rw [withDensity_one]

Premises used: MeasureTheory.withDensity_one
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
suffices : (f * fun (x : α) ↦ (f x)⁻¹) ≤ᶠ[ae μ] 1
⊢ μ.withDensity (f * fun (x : α) ↦ (f x)⁻¹) ≤ μ

Tactic:
suffices (f * fun x ↦ (f x)⁻¹) ≤ᵐ[μ] 1 by
    refine (withDensity_mono this).trans ?_
    rw [withDensity_one]
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∀ (x : α), HMul.hMul (β := (x : α) → ℝ≥0∞) f (fun (x : α) ↦ (f x)⁻¹) x ≤ 1 x
⊢ (f * fun (x : α) ↦ (f x)⁻¹) ≤ᶠ[ae μ] 1

Tactic:
filter_upwards with x
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
x : α
⊢ HMul.hMul (β := (x : α) → ℝ≥0∞) f (fun (x : α) ↦ (f x)⁻¹) x ≤ 1 x

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
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 ≠ ∞
rw : μ.withDensity (f * fun (x : α) ↦ (f x)⁻¹) = μ
⊢ ((μ.withDensity f).withDensity fun (x : α) ↦ (f x)⁻¹) = μ

Tactic:
rw [← withDensity_mul₀ hf hf.inv]

Premises used: MeasureTheory.withDensity_mul₀, AEMeasurable.inv
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
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 = μ
rw₁ rw₂ : μ = μ
⊢ μ.withDensity (f * fun (x : α) ↦ (f x)⁻¹) = μ

Tactic:
rw [withDensity_congr_ae this, withDensity_one]

Premises used: MeasureTheory.withDensity_one, MeasureTheory.withDensity_congr_ae
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
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 ≠ ∞
suffices : (f * fun (x : α) ↦ (f x)⁻¹) =ᶠ[ae μ] 1
⊢ μ.withDensity (f * fun (x : α) ↦ (f x)⁻¹) = μ

Tactic:
suffices (f * fun x ↦ (f x)⁻¹) =ᵐ[μ] 1 by
    rw [withDensity_congr_ae this, withDensity_one]
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
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 ≠ ∞
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
⊢ (f * fun (x : α) ↦ (f x)⁻¹) =ᶠ[ae μ] 1

Tactic:
filter_upwards [hf_ne_zero, hf_ne_top] with x hf_ne_zero hf_ne_top
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
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)
h₁ h₂ : Eq (α := ℝ≥0∞) 1 1
⊢ f x * (f x)⁻¹ = 1 x

Tactic:
rw [ENNReal.mul_inv_cancel hf_ne_zero hf_ne_top, Pi.one_apply]

Premises used: Pi.one_apply, ENNReal.mul_inv_cancel
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hf_ne_zero : ∀ᵐ (x : α) ∂μ, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
⊢ ((μ.withDensity f).withDensity fun (x : α) ↦ (f x)⁻¹) = μ

Tactic:
withDensity_inv_same₀ hf.aemeasurable hf_ne_zero hf_ne_top

Premises used: Measurable.aemeasurable, MeasureTheory.withDensity_inv_same₀
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_zero : ∀ᵐ (x : α) ∂μ, f x ≠ 0
⊢ μ ≪ μ.withDensity f

Tactic:
Measure.AbsolutelyContinuous.mk (fun s hs hμs ↦ ?_)

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.mk
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_zero : ∀ᵐ (x : α) ∂μ, f x ≠ 0
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∞)
⊢ μ ≪ μ.withDensity f

Tactic:
refine Measure.AbsolutelyContinuous.mk (fun s hs hμs ↦ ?_)

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.mk
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
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∞) {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

Premises used: MeasureTheory.lintegral_eq_zero_iff', Filter.EventuallyEq, Set.indicator_zero', AEMeasurable.restrict, MeasureTheory.ae_iff, ae_eq_restrict_iff_indicator_ae_eq, MeasureTheory.withDensity_apply
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
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∞) {a : α | f a = 0} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp only [ae_iff, ne_eq, not_not] at hf_ne_zero

Premises used: Classical.not_not, ne_eq, MeasureTheory.ae_iff
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
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∞) {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

Premises used: Pi.zero_apply, exists_prop, Set.indicator_apply_eq_zero, Classical.not_forall
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
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∞)
⊢ 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⟩
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
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∞)
hle : s ⊆ {a : α | a ∈ s ∧ ¬f a = 0} ∪ {a : α | f a = 0}
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
measure_mono_null hle <| nonpos_iff_eq_zero.1 <| le_trans (measure_union_le _ _)
    <| hμs.symm ▸ zero_add _ |>.symm ▸ hf_ne_zero.le

Premises used: Eq.rec, Eq.le, MeasureTheory.measure_mono_null, Iff.mp, MeasureTheory.measure_union_le, nonpos_iff_eq_zero, le_trans
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
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∞)
hle : s ⊆ {a : α | a ∈ s ∧ ¬f a = 0} ∪ {a : α | f a = 0}
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact measure_mono_null hle <| nonpos_iff_eq_zero.1 <| le_trans (measure_union_le _ _)
    <| hμs.symm ▸ zero_add _ |>.symm ▸ hf_ne_zero.le

Premises used: MeasureTheory.measure_mono_null, Iff.mp, MeasureTheory.measure_union_le, nonpos_iff_eq_zero, le_trans
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
f g : α → β
d : α → ℝ≥0∞
hd : AEMeasurable d μ
h_ae_nonneg : ∀ᵐ (x : α) ∂μ, d x ≠ 0
⊢ f =ᶠ[ae (μ.withDensity d)] g ↔ f =ᶠ[ae μ] g

Tactic:
Iff.intro
  (fun h ↦ Measure.AbsolutelyContinuous.ae_eq
    (withDensity_absolutelyContinuous' hd h_ae_nonneg) h)
  (fun h ↦ Measure.AbsolutelyContinuous.ae_eq
    (withDensity_absolutelyContinuous μ d) h)

Premises used: MeasureTheory.withDensity_absolutelyContinuous', Iff.intro, MeasureTheory.withDensity_absolutelyContinuous, MeasureTheory.Measure.AbsolutelyContinuous.ae_eq
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f : α → ℝ≥0
⊢ SigmaFinite (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))

Tactic:
⟨⟨⟨fun n ↦ spanningSets μ n ∩ f ⁻¹' (Iic n), fun _ ↦ trivial, fun n ↦ ?_, ?_⟩⟩⟩

Premises used: trivial, MeasureTheory.Measure.FiniteSpanningSetsIn.mk, Nonempty.intro, Nat.cast, Inter.inter, Set.preimage, Set.Iic, MeasureTheory.spanningSets, MeasureTheory.SigmaFinite.mk
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
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∞)
refine_2 : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), (fun (n : ℕ) ↦ spanningSets μ n ∩ f ⁻¹' Iic (↑n : ℝ≥0)) i) univ
⊢ SigmaFinite (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))

Tactic:
refine ⟨⟨⟨fun n ↦ spanningSets μ n ∩ f ⁻¹' (Iic n), fun _ ↦ trivial, fun n ↦ ?_, ?_⟩⟩⟩
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f : α → ℝ≥0
n : ℕ
refine_1 : ∫⁻ (a : α) in (fun (n : ℕ) ↦ spanningSets μ n ∩ f ⁻¹' Iic (↑n : ℝ≥0)) n, (↑(f a) : ℝ≥0∞) ∂μ < ∞
⊢ LT.lt (α := ℝ≥0∞)
    ((μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞) : (a : Set α) → ℝ≥0∞)
        ((fun (n : ℕ) ↦ spanningSets μ n ∩ f ⁻¹' Iic (↑n : ℝ≥0)) n) :
      ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
rw [withDensity_apply']

Premises used: MeasureTheory.withDensity_apply'
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
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∞)
refine_1₁ : BddAbove (f '' (fun (n : ℕ) ↦ spanningSets μ n ∩ f ⁻¹' Iic (↑n : ℝ≥0)) n)
⊢ ∫⁻ (a : α) in (fun (n : ℕ) ↦ spanningSets μ n ∩ f ⁻¹' Iic (↑n : ℝ≥0)) n, (↑(f a) : ℝ≥0∞) ∂μ < ∞

Tactic:
apply setLIntegral_lt_top_of_bddAbove

Premises used: MeasureTheory.setLIntegral_lt_top_of_bddAbove
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f : α → ℝ≥0
n : ℕ
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (n : ℕ) ↦ spanningSets μ n ∩ f ⁻¹' Iic (↑n : ℝ≥0)) n) : ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
((measure_mono inter_subset_left).trans_lt (measure_spanningSets_lt_top μ n)).ne

Premises used: MeasureTheory.measure_spanningSets_lt_top, Set.inter_subset_left, MeasureTheory.measure_mono, LE.le.trans_lt, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f : α → ℝ≥0
n : ℕ
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (n : ℕ) ↦ spanningSets μ n ∩ f ⁻¹' Iic (↑n : ℝ≥0)) n) : ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
exact ((measure_mono inter_subset_left).trans_lt (measure_spanningSets_lt_top μ n)).ne

Premises used: MeasureTheory.measure_spanningSets_lt_top, Set.inter_subset_left, MeasureTheory.measure_mono, LE.le.trans_lt, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f : α → ℝ≥0
n : ℕ
⊢ BddAbove (f '' (fun (n : ℕ) ↦ spanningSets μ n ∩ f ⁻¹' Iic (↑n : ℝ≥0)) n)

Tactic:
⟨n, forall_mem_image.2 fun x hx ↦ hx.2⟩

Premises used: Iff.mpr, Nat.cast, BddAbove, Set.Nonempty, And.right, Exists.intro, Set.forall_mem_image
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f : α → ℝ≥0
n : ℕ
⊢ BddAbove (f '' (fun (n : ℕ) ↦ spanningSets μ n ∩ f ⁻¹' Iic (↑n : ℝ≥0)) n)

Tactic:
exact ⟨n, forall_mem_image.2 fun x hx ↦ hx.2⟩
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f : α → ℝ≥0
refine_2 : ∀ (x : α), ∃ (i : ℕ), x ∈ spanningSets μ i ∩ f ⁻¹' Iic (↑i : ℝ≥0)
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), (fun (n : ℕ) ↦ spanningSets μ n ∩ f ⁻¹' Iic (↑n : ℝ≥0)) i) univ

Tactic:
rw [iUnion_eq_univ_iff]

Premises used: Set.iUnion_eq_univ_iff
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f : α → ℝ≥0
⊢ ∀ (x : α), ∃ (i : ℕ), x ∈ spanningSets μ i ∩ f ⁻¹' Iic (↑i : ℝ≥0)

Tactic:
fun x ↦ ⟨max (spanningSetsIndex μ x) ⌈f x⌉₊, ?_, ?_⟩

Premises used: MeasureTheory.spanningSetsIndex, Max.max, Nat.ceil, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f : α → ℝ≥0
refine_2 : ∀ (x : α), x ∈ spanningSets μ (max (spanningSetsIndex μ x) ⌈f x⌉₊)
refine_2₁ : ∀ (x : α), x ∈ f ⁻¹' Iic (↑(max (spanningSetsIndex μ x) ⌈f x⌉₊) : ℝ≥0)
⊢ ∀ (x : α), ∃ (i : ℕ), x ∈ spanningSets μ i ∩ f ⁻¹' Iic (↑i : ℝ≥0)

Tactic:
refine fun x ↦ ⟨max (spanningSetsIndex μ x) ⌈f x⌉₊, ?_, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f : α → ℝ≥0
x : α
⊢ x ∈ spanningSets μ (max (spanningSetsIndex μ x) ⌈f x⌉₊)

Tactic:
mem_spanningSets_of_index_le _ _ (le_max_left ..)

Premises used: MeasureTheory.mem_spanningSets_of_index_le, le_max_left
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f : α → ℝ≥0
x : α
⊢ x ∈ spanningSets μ (max (spanningSetsIndex μ x) ⌈f x⌉₊)

Tactic:
exact mem_spanningSets_of_index_le _ _ (le_max_left ..)

Premises used: MeasureTheory.mem_spanningSets_of_index_le, le_max_left
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f : α → ℝ≥0
x : α
⊢ x ∈ f ⁻¹' Iic (↑(max (spanningSetsIndex μ x) ⌈f x⌉₊) : ℝ≥0)

Tactic:
simp [Nat.le_ceil]

Premises used: Nat.le_ceil
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f : α → ℝ≥0∞
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
⊢ f =ᶠ[ae μ] fun (x : α) ↦ (↑(f x).toNNReal : ℝ≥0∞)

Tactic:
have : f =ᵐ[μ] fun x ↦ (f x).toNNReal := hf_ne_top.mono fun x hx ↦ (ENNReal.coe_toNNReal hx).symm
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f : α → ℝ≥0∞
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
this : f =ᶠ[ae μ] fun (x : α) ↦ (↑(f x).toNNReal : ℝ≥0∞)
rw : SigmaFinite (μ.withDensity fun (x : α) ↦ (↑(f x).toNNReal : ℝ≥0∞))
⊢ SigmaFinite (μ.withDensity f)

Tactic:
rw [withDensity_congr_ae this]

Premises used: MeasureTheory.withDensity_congr_ae