awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
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∞) ≠ 0

Tactic:
simpa only [Ne, ENNReal.coe_eq_zero] using h_a_nonneg

Premises used: Ne, ENNReal.coe_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
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∞) ≠ 0

Tactic:
have : (f' a : ℝ≥0∞) ≠ 0 := by simpa only [Ne, ENNReal.coe_eq_zero] using h_a_nonneg
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
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
h : ∀ (this : (↑(f a) : ℝ≥0∞) ≠ 0), (↑(f a) : ℝ≥0∞) * g a = (↑(f a) : ℝ≥0∞) * g' a
⊢ (↑(f a) : ℝ≥0∞) * g a = (↑(f' a) : ℝ≥0∞) * g' a

Tactic:
rw [← h'a] at this ⊢
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
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
h h₁ : (↑(f a) : ℝ≥0∞) * g' a = (↑(f a) : ℝ≥0∞) * g' a
⊢ (↑(f a) : ℝ≥0∞) * g a = (↑(f a) : ℝ≥0∞) * g' a

Tactic:
rw [ha this]
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
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 : α) ∂μ,
    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)
⊢ ∀ᵐ (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:
rw [ae_restrict_iff' A.compl]

Premises used: MeasurableSet.compl, MeasureTheory.ae_restrict_iff'
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
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}
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
⊢ ∀ᵐ (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:
filter_upwards [hf'_ae] with a ha ha_null
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
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

Tactic:
have ha_null : f' a = 0 := Function.notMem_support.mp ha_null
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
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
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
⊢ (↑(f a) : ℝ≥0∞) * g a = (↑(f' a) : ℝ≥0∞) * g' a

Tactic:
rw [ha_null] at ha ⊢
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
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
h : (↑0 : ℝ≥0∞) * g a = (↑0 : ℝ≥0∞) * g' a
⊢ (↑(f a) : ℝ≥0∞) * g a = (↑0 : ℝ≥0∞) * g' a

Tactic:
rw [ha]
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
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
⊢ (↑0 : ℝ≥0∞) * g a = (↑0 : ℝ≥0∞) * g' a

Tactic:
simp only [ENNReal.coe_zero, zero_mul]

Premises used: MulZeroClass.zero_mul, ENNReal.coe_zero
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
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'
mpr : g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] fun (x : α) ↦ (↑(f' x) : ℝ≥0∞)⁻¹ * g' x
⊢ AEMeasurable g (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))

Tactic:
refine ⟨fun x => ((f' x)⁻¹ : ℝ≥0∞) * g' x, hf'_m.coe_nnreal_ennreal.inv.smul g'meas, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
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'
mpr : ∀ᵐ (x : α) ∂μ, (↑(f x) : ℝ≥0∞) ≠ 0 → g x = (↑(f' x) : ℝ≥0∞)⁻¹ * g' x
⊢ g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] fun (x : α) ↦ (↑(f' x) : ℝ≥0∞)⁻¹ * g' x

Tactic:
rw [EventuallyEq, ae_withDensity_iff' hf.coe_nnreal_ennreal]

Premises used: Filter.EventuallyEq, AEMeasurable.coe_nnreal_ennreal, MeasureTheory.ae_withDensity_iff'
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
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'
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
⊢ ∀ᵐ (x : α) ∂μ, (↑(f x) : ℝ≥0∞) ≠ 0 → g x = (↑(f' x) : ℝ≥0∞)⁻¹ * g' x

Tactic:
filter_upwards [hg', hf'_ae] with a hfga hff'a h'a
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
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
⊢ (↑(f' a) : ℝ≥0∞) * g a = g' a

Tactic:
rw [hff'a] at hfga h'a
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
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
⊢ f a = f' a

Tactic:
rw [hff'a] at hfga h'a
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
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
⊢ (↑(f' a) : ℝ≥0∞) ≠ 0

Tactic:
rw [hff'a] at hfga h'a
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
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
h₃ h₄ : g a = g a
⊢ g a = (↑(f' a) : ℝ≥0∞)⁻¹ * g' a

Tactic:
rw [← hfga, ← mul_assoc, ENNReal.inv_mul_cancel h'a ENNReal.coe_ne_top, one_mul]

Premises used: mul_assoc, ENNReal.inv_mul_cancel, one_mul, ENNReal.coe_ne_top
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : Measurable f
g : α → ℝ≥0∞
⊢ AEMeasurable g (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) ↔
    AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ (↑(f x) : ℝ≥0∞) * g x) μ

Tactic:
aemeasurable_withDensity_ennreal_iff' <| hf.aemeasurable

Premises used: MeasureTheory.aemeasurable_withDensity_ennreal_iff', Measurable.aemeasurable
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
a : α
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∞)
⊢ withDensity (dirac a) f = HSMul.hSMul (β := Measure α) (f a) (dirac a)

Tactic:
ext s hs
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
a : α
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:
simp [withDensity_apply f hs, setLIntegral_dirac' hf hs, dirac_apply' _ hs,
    Set.indicator]

Premises used: Set.indicator, MeasureTheory.Measure.dirac_apply', MeasureTheory.setLIntegral_dirac', MeasureTheory.withDensity_apply
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
a : α
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:
classical
  simp [withDensity_apply f hs, setLIntegral_dirac' hf hs, dirac_apply' _ hs,
    Set.indicator]

Premises used: Set.indicator, MeasureTheory.Measure.dirac_apply', MeasureTheory.withDensity_apply
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
inst : MeasurableSingletonClass α
f : α → ℝ≥0∞
a : α
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∞)
⊢ withDensity (dirac a) f = HSMul.hSMul (β := Measure α) (f a) (dirac a)

Tactic:
ext s hs
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
inst : MeasurableSingletonClass α
f : α → ℝ≥0∞
a : α
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:
simp [withDensity_apply f hs, setLIntegral_dirac, Set.indicator]

Premises used: Set.indicator, MeasureTheory.setLIntegral_dirac, MeasureTheory.withDensity_apply
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
inst : MeasurableSingletonClass α
f : α → ℝ≥0∞
a : α
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:
classical
  simp [withDensity_apply f hs, setLIntegral_dirac, Set.indicator]

Premises used: Set.indicator, MeasureTheory.setLIntegral_dirac, MeasureTheory.withDensity_apply
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
⊢ Eq (α := Measure α) (withDensity count f) (sum fun (a : α) ↦ HSMul.hSMul (β := Measure α) (f a) (dirac a))

Tactic:
simp [count, withDensity_sum, dirac_withDensity' hf _]

Premises used: MeasureTheory.withDensity_sum, MeasureTheory.dirac_withDensity', MeasureTheory.Measure.count
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
inst : MeasurableSingletonClass α
f : α → ℝ≥0∞
⊢ Eq (α := Measure α) (withDensity count f) (sum fun (a : α) ↦ HSMul.hSMul (β := Measure α) (f a) (dirac a))

Tactic:
simp [count, withDensity_sum, dirac_withDensity]

Premises used: MeasureTheory.withDensity_sum, MeasureTheory.Measure.count, MeasureTheory.dirac_withDensity
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
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 ∂μ
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 ∂μ
iSup :
  ∀ ⦃f_1 : ℕ → α → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f_1 n)) →
      Monotone f_1 →
        (∀ (n : ℕ), ∫⁻ (a : α), f_1 n a ∂μ.withDensity f = ∫⁻ (a : α), (f * f_1 n) a ∂μ) →
          ∫⁻ (a : α), (fun (x : α) ↦ (⨆ (n : ℕ), f_1 n x : ℝ≥0∞)) a ∂μ.withDensity f =
            ∫⁻ (a : α), HMul.hMul (β := α → ℝ≥0∞) f (fun (x : α) ↦ ⨆ (n : ℕ), f_1 n x) a ∂μ
⊢ ∀ {g : α → ℝ≥0∞}, Measurable g → ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ

Tactic:
apply Measurable.ennreal_induction
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
c : ℝ≥0∞
s : Set α
h_ms : MeasurableSet s
⊢ ∫⁻ (a : α), s.indicator (fun (x : α) ↦ c) a ∂μ.withDensity f =
    ∫⁻ (a : α), HMul.hMul (β := α → ℝ≥0∞) f (s.indicator fun (x : α) ↦ c) a ∂μ

Tactic:
simp [*, mul_comm _ c, ← indicator_mul_right]

Premises used: mul_comm, Set.indicator_mul_right
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
g h : α → ℝ≥0∞
add :
  Disjoint (Function.support g) (Function.support h) →
    Measurable g →
      Measurable h →
        ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ →
          ∫⁻ (a : α), h a ∂μ.withDensity f = ∫⁻ (a : α), (f * h) a ∂μ →
            ∫⁻ (a : α), (g + h) a ∂μ.withDensity f = ∫⁻ (a : α), (f * (g + h)) a ∂μ
⊢ Disjoint (Function.support g) (Function.support h) →
    Measurable g →
      Measurable h →
        ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ →
          ∫⁻ (a : α), h a ∂μ.withDensity f = ∫⁻ (a : α), (f * h) a ∂μ →
            ∫⁻ (a : α), (g + h) a ∂μ.withDensity f = ∫⁻ (a : α), (f * (g + h)) a ∂μ

Tactic:
_
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
g h : α → ℝ≥0∞
h_1 : Disjoint (Function.support g) (Function.support h)
h_mea_g : Measurable g
add :
  Measurable h →
    ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ →
      ∫⁻ (a : α), h a ∂μ.withDensity f = ∫⁻ (a : α), (f * h) a ∂μ →
        ∫⁻ (a : α), (g + h) a ∂μ.withDensity f = ∫⁻ (a : α), (f * (g + h)) a ∂μ
⊢ Measurable h →
    ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ →
      ∫⁻ (a : α), h a ∂μ.withDensity f = ∫⁻ (a : α), (f * h) a ∂μ →
        ∫⁻ (a : α), (g + h) a ∂μ.withDensity f = ∫⁻ (a : α), (f * (g + h)) a ∂μ

Tactic:
_
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
g h : α → ℝ≥0∞
h_1 : Disjoint (Function.support g) (Function.support h)
h_mea_g : Measurable g
h_2 : Measurable h
h_ind_g : ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ
h_ind_h : ∫⁻ (a : α), h a ∂μ.withDensity f = ∫⁻ (a : α), (f * h) a ∂μ
⊢ ∫⁻ (a : α), (g + h) a ∂μ.withDensity f = ∫⁻ (a : α), (f * (g + h)) a ∂μ

Tactic:
simp [mul_add, *, Measurable.mul]

Premises used: Measurable.mul, mul_add
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
g : ℕ → α → ℝ≥0∞
h_mea_g : ∀ (n : ℕ), Measurable (g n)
h_mono_g : Monotone g
h_ind : ∀ (n : ℕ), ∫⁻ (a : α), g n a ∂μ.withDensity f = ∫⁻ (a : α), (f * g n) a ∂μ
m n : ℕ
hmn : m ≤ n
x : α
grw grw₁ : f x * g n x ≤ f x * g n x
⊢ f x * g m x ≤ f x * g n x

Tactic:
grw [h_mono_g hmn x]
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
g : ℕ → α → ℝ≥0∞
h_mea_g : ∀ (n : ℕ), Measurable (g n)
h_mono_g : Monotone g
h_ind : ∀ (n : ℕ), ∫⁻ (a : α), g n a ∂μ.withDensity f = ∫⁻ (a : α), (f * g n) a ∂μ
⊢ Monotone.{0, u_1} (β := (a : α) → ℝ≥0∞) fun (n : ℕ) (a : α) ↦ f a * g n a

Tactic:
have : Monotone fun n a => f a * g n a := fun m n hmn x => by dsimp; grw [h_mono_g hmn x]
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
g : ℕ → α → ℝ≥0∞
h_mea_g : ∀ (n : ℕ), Measurable (g n)
h_mono_g : Monotone g
h_ind : ∀ (n : ℕ), ∫⁻ (a : α), g n a ∂μ.withDensity f = ∫⁻ (a : α), (f * g n) a ∂μ
this : Monotone.{0, u_1} (β := (a : α) → ℝ≥0∞) fun (n : ℕ) (a : α) ↦ f a * g n a
⊢ ∫⁻ (a : α), (fun (x : α) ↦ (⨆ (n : ℕ), g n x : ℝ≥0∞)) a ∂μ.withDensity f =
    ∫⁻ (a : α), HMul.hMul (β := α → ℝ≥0∞) f (fun (x : α) ↦ ⨆ (n : ℕ), g n x) a ∂μ

Tactic:
simp [lintegral_iSup, ENNReal.mul_iSup, h_mf.mul (h_mea_g _), *]

Premises used: Measurable.mul, MeasureTheory.lintegral_iSup, ENNReal.mul_iSup
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
s : Set α
hs : MeasurableSet s
rw : ∫⁻ (x : α), g x ∂(μ.restrict s).withDensity f = ∫⁻ (x : α) in s, (f * g) x ∂μ
rw₁ rw₂ : ∫⁻ (a : α) in s, (f * g) a ∂μ = ∫⁻ (x : α) in s, (f * g) x ∂μ
⊢ ∫⁻ (x : α) in s, g x ∂μ.withDensity f = ∫⁻ (x : α) in s, (f * g) x ∂μ

Tactic:
rw [restrict_withDensity hs, lintegral_withDensity_eq_lintegral_mul _ hf hg]

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

Tactic:
have : μ.withDensity f = μ.withDensity f' := withDensity_congr_ae hf.ae_eq_mk
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
hg : AEMeasurable g (μ.withDensity f)
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
this : μ.withDensity f = μ.withDensity f'
rw :
  ∀ (hg : AEMeasurable g (μ.withDensity f')) (this : μ.withDensity f = μ.withDensity f'),
    ∫⁻ (a : α), g a ∂μ.withDensity f' = ∫⁻ (a : α), (f * g) a ∂μ
⊢ ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ

Tactic:
rw [this] at hg ⊢
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
⊢ ∫⁻ (a : α), g a ∂μ.withDensity f' = ∫⁻ (a : α), g' a ∂μ.withDensity f'

Tactic:
lintegral_congr_ae hg.ae_eq_mk

Premises used: MeasureTheory.lintegral_congr_ae, AEMeasurable.ae_eq_mk
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
⊢ ∫⁻ (a : α), g' a ∂μ.withDensity f' = ∫⁻ (a : α), (f' * g') a ∂μ

Tactic:
(lintegral_withDensity_eq_lintegral_mul _ hf.measurable_mk hg.measurable_mk)

Premises used: MeasureTheory.lintegral_withDensity_eq_lintegral_mul, AEMeasurable.measurable_mk
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
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 μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
h : ∀ᵐ (x : α) ∂μ.restrict {x : α | f' x ≠ 0}, (f' * g') x = (f' * g) x
h₁ : ∀ᵐ (x : α) ∂μ.restrict {x : α | f' x ≠ 0}ᶜ, (f' * g') x = (f' * g) x
⊢ f' * g' =ᶠ[ae μ] f' * g

Tactic:
apply ae_of_ae_restrict_of_ae_restrict_compl { x | f' x ≠ 0 }

Premises used: MeasureTheory.ae_of_ae_restrict_of_ae_restrict_compl, setOf, Ne, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
⊢ g =ᶠ[ae (μ.withDensity f')] AEMeasurable.mk g hg

Tactic:
have Z := hg.ae_eq_mk