awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ∞
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ∞
h1 : ¬p = 1
hp1_lt : 1 < p
hpq : p.HolderConjugate p.conjExponent
h0 : ¬∫⁻ (a : α), (f + g) a ^ p ∂μ = 0
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)

Tactic:
lintegral_Lp_add_le_aux hpq hf hg h0
    (lintegral_rpow_add_lt_top_of_lintegral_rpow_lt_top hf hf_top hg_top hp1).ne

Premises used: _private.0.ENNReal.lintegral_Lp_add_le_aux, ENNReal.lintegral_rpow_add_lt_top_of_lintegral_rpow_lt_top, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ∞
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ∞
h1 : ¬p = 1
hp1_lt : 1 < p
hpq : p.HolderConjugate p.conjExponent
h0 : ¬∫⁻ (a : α), (f + g) a ^ p ∂μ = 0
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)

Tactic:
exact lintegral_Lp_add_le_aux hpq hf hg h0
    (lintegral_rpow_add_lt_top_of_lintegral_rpow_lt_top hf hf_top hg_top hp1).ne

Premises used: _private.0.ENNReal.lintegral_Lp_add_le_aux, ENNReal.lintegral_rpow_add_lt_top_of_lintegral_rpow_lt_top, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hp0 : 0 ≤ p
hp1 : p ≤ 1
inl :
  ∀ (hp0 : LE.le (α := ℝ) 0 0) (hp1 : LE.le (α := ℝ) 0 1),
    (∫⁻ (a : α), HPow.hPow (β := ℝ) ((f + g) a) 0 ∂μ) ^ (1 / 0) ≤
      HPow.hPow (α := ℝ≥0∞) 2 (1 / 0 - 1) *
        ((∫⁻ (a : α), HPow.hPow (β := ℝ) (f a) 0 ∂μ) ^ (1 / 0) + (∫⁻ (a : α), HPow.hPow (β := ℝ) (g a) 0 ∂μ) ^ (1 / 0))
inr :
  ∀ (hp : 0 < p),
    (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤
      HPow.hPow (α := ℝ≥0∞) 2 (1 / p - 1) * ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p))
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤
    HPow.hPow (α := ℝ≥0∞) 2 (1 / p - 1) * ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p))

Tactic:
rcases eq_or_lt_of_le hp0 with (rfl | hp)

Premises used: eq_or_lt_of_le, rfl
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hp0 : LE.le (α := ℝ) 0 0
hp1 : LE.le (α := ℝ) 0 1
inl : 1 ≤ HPow.hPow (α := ℝ≥0∞) (β := ℝ) 2 (-1) * HAdd.hAdd (α := ℝ≥0∞) 1 1
⊢ (∫⁻ (a : α), HPow.hPow (β := ℝ) ((f + g) a) 0 ∂μ) ^ (1 / 0) ≤
    HPow.hPow (α := ℝ≥0∞) 2 (1 / 0 - 1) *
      ((∫⁻ (a : α), HPow.hPow (β := ℝ) (f a) 0 ∂μ) ^ (1 / 0) + (∫⁻ (a : α), HPow.hPow (β := ℝ) (g a) 0 ∂μ) ^ (1 / 0))

Tactic:
simp only [Pi.add_apply, rpow_zero, lintegral_one, _root_.div_zero, zero_sub]

Premises used: Pi.add_apply, ENNReal.rpow_zero, div_zero, zero_sub, MeasureTheory.lintegral_one
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hp0 : LE.le (α := ℝ) 0 0
hp1 : LE.le (α := ℝ) 0 1
inl : 1 ≤ HPow.hPow (α := ℝ≥0∞) (β := ℝ) 2 (-1) * 2
⊢ 1 ≤ HPow.hPow (α := ℝ≥0∞) (β := ℝ) 2 (-1) * HAdd.hAdd (α := ℝ≥0∞) 1 1

Tactic:
norm_num
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hp0 : LE.le (α := ℝ) 0 0
hp1 : LE.le (α := ℝ) 0 1
inl : 1 ≤ (HPow.hPow (α := ℝ≥0∞) (β := ℝ) 2 1)⁻¹ * 2
inl₁ : 1 ≤ HMul.hMul (α := ℝ≥0∞) 2⁻¹ 2
inl₂ inl₃ : LE.le (α := ℝ≥0∞) 1 1
⊢ 1 ≤ HPow.hPow (α := ℝ≥0∞) (β := ℝ) 2 (-1) * 2

Tactic:
rw [rpow_neg, rpow_one, ENNReal.inv_mul_cancel two_ne_zero ofNat_ne_top]

Premises used: ENNReal.ofNat_ne_top, ENNReal.rpow_one, two_ne_zero, ENNReal.inv_mul_cancel, ENNReal.rpow_neg
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hp0 : 0 ≤ p
hp1 : p ≤ 1
hp : 0 < p
rw : (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p + g a ^ p ∂μ) ^ (1 / p)
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ + ∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)

Tactic:
rw [← lintegral_add_left' (hf.pow_const p)]

Premises used: MeasureTheory.lintegral_add_left', AEMeasurable.pow_const
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hp0 : 0 ≤ p
hp1 : p ≤ 1
hp : 0 < p
h₁ : ∀ (a : α), (f + g) a ^ p ≤ f a ^ p + g a ^ p
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p + g a ^ p ∂μ) ^ (1 / p)

Tactic:
gcongr with a
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hp0 : 0 ≤ p
hp1 : p ≤ 1
hp : 0 < p
a : α
⊢ (f + g) a ^ p ≤ f a ^ p + g a ^ p

Tactic:
rpow_add_le_add_rpow _ _ hp0 hp1

Premises used: ENNReal.rpow_add_le_add_rpow
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hp0 : 0 ≤ p
hp1 : p ≤ 1
hp : 0 < p
a : α
⊢ (f + g) a ^ p ≤ f a ^ p + g a ^ p

Tactic:
exact rpow_add_le_add_rpow _ _ hp0 hp1

Premises used: ENNReal.rpow_add_le_add_rpow
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hp0 : 0 ≤ p
hp1 : p ≤ 1
hp : 0 < p
⊢ (∫⁻ (a : α), f a ^ p ∂μ + ∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p) ≤
    HPow.hPow (α := ℝ≥0∞) 2 (1 / p - 1) * ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p))

Tactic:
rpow_add_le_mul_rpow_add_rpow _ _ ((one_le_div hp).2 hp1)

Premises used: Iff.mpr, ENNReal.rpow_add_le_mul_rpow_add_rpow, one_le_div
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hp0 : 0 ≤ p
hp1 : p ≤ 1
hp : 0 < p
a : (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ + ∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤
    HPow.hPow (α := ℝ≥0∞) 2 (1 / p - 1) * ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p))

Tactic:
calc
    (∫⁻ a, (f + g) a ^ p ∂μ) ^ (1 / p) ≤ ((∫⁻ a, f a ^ p ∂μ) + ∫⁻ a, g a ^ p ∂μ) ^ (1 / p) := by
      rw [← lintegral_add_left' (hf.pow_const p)]
      gcongr with a
      exact rpow_add_le_add_rpow _ _ hp0 hp1
    _ ≤ (2 : ℝ≥0∞) ^ (1 / p - 1) * ((∫⁻ a, f a ^ p ∂μ) ^ (1 / p) + (∫⁻ a, g a ^ p ∂μ) ^ (1 / p)) :=
      rpow_add_le_mul_rpow_add_rpow _ _ ((one_le_div hp).2 hp1)

Premises used: Iff.mpr, HSub.hSub, HDiv.hDiv, ENNReal.rpow_add_le_mul_rpow_add_rpow, HPow.hPow, HAdd.hAdd, one_le_div, OfNat.ofNat, MeasureTheory.lintegral
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ ∫⁻ (a : α), (↑(f a) : ℝ≥0∞) * (↑(g a) : ℝ≥0∞) ∂μ ≤
    (∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), (↑(g a) : ℝ≥0∞) ^ q ∂μ) ^ (1 / q)

Tactic:
ENNReal.lintegral_mul_le_Lp_mul_Lq μ hpq hf.coe_nnreal_ennreal hg.coe_nnreal_ennreal

Premises used: AEMeasurable.coe_nnreal_ennreal, ENNReal.lintegral_mul_le_Lp_mul_Lq
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ ∫⁻ (a : α), (↑(f a) : ℝ≥0∞) * (↑(g a) : ℝ≥0∞) ∂μ ≤
    (∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), (↑(g a) : ℝ≥0∞) ^ q ∂μ) ^ (1 / q)

Tactic:
exact ENNReal.lintegral_mul_le_Lp_mul_Lq μ hpq hf.coe_nnreal_ennreal hg.coe_nnreal_ennreal

Premises used: AEMeasurable.coe_nnreal_ennreal, ENNReal.lintegral_mul_le_Lp_mul_Lq
-- Module: Mathlib.MeasureTheory.Integral.MeanValue
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (ε := ℝ) (fun (x : α) ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : (x : α) → ENNReal := fun (x : α) ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
hf₁ : AEMeasurable g (μ.restrict s)
⊢ AEMeasurable ρ (μ.restrict s)

Tactic:
apply AEMeasurable.ennreal_ofReal

Premises used: AEMeasurable.ennreal_ofReal
-- Module: Mathlib.MeasureTheory.Integral.MeanValue
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (ε := ℝ) (fun (x : α) ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : (x : α) → ENNReal := fun (x : α) ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
⊢ AEMeasurable g (μ.restrict s)

Tactic:
hg.aestronglyMeasurable.aemeasurable

Premises used: MeasureTheory.Integrable.aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.aemeasurable
-- Module: Mathlib.MeasureTheory.Integral.MeanValue
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (ε := ℝ) (fun (x : α) ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : (x : α) → ENNReal := fun (x : α) ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
⊢ AEMeasurable g (μ.restrict s)

Tactic:
exact hg.aestronglyMeasurable.aemeasurable

Premises used: MeasureTheory.Integrable.aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.aemeasurable
-- Module: Mathlib.MeasureTheory.Integral.MeanValue
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (ε := ℝ) (fun (x : α) ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : (x : α) → ENNReal := fun (x : α) ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
⊢ AEMeasurable ρ (μ.restrict s)

Tactic:
have hρ_ae : AEMeasurable ρ (μ.restrict s) := by
    apply AEMeasurable.ennreal_ofReal
    exact hg.aestronglyMeasurable.aemeasurable
-- Module: Mathlib.MeasureTheory.Integral.MeanValue
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (ε := ℝ) (fun (x : α) ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : (x : α) → ENNReal := fun (x : α) ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
hρ_ae : AEMeasurable ρ (μ.restrict s)
⊢ ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤

Tactic:
simp [ρ]
-- Module: Mathlib.MeasureTheory.Integral.MeanValue
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (ε := ℝ) (fun (x : α) ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : (x : α) → ENNReal := fun (x : α) ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
hρ_ae : AEMeasurable ρ (μ.restrict s)
⊢ ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤

Tactic:
have hρ_top : ∀ᵐ x ∂μ.restrict s, ρ x < ⊤ := by simp [ρ]
-- Module: Mathlib.MeasureTheory.Integral.MeanValue
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (ε := ℝ) (fun (x : α) ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : (x : α) → ENNReal := fun (x : α) ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
apply : ∀ (x : α), 0 ≤ g x → (fun (x : α) ↦ (ρ x).toReal) x = g x
⊢ (fun (x : α) ↦ (ρ x).toReal) =ᶠ[ae (μ.restrict s)] g

Tactic:
apply hg0.mono

Premises used: Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Integral.MeanValue
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (ε := ℝ) (fun (x : α) ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : (x : α) → ENNReal := fun (x : α) ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
x : α
hx : 0 ≤ g x
⊢ (fun (x : α) ↦ (ρ x).toReal) x = g x

Tactic:
simpa [ρ]
-- Module: Mathlib.MeasureTheory.Integral.MeanValue
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (ε := ℝ) (fun (x : α) ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : (x : α) → ENNReal := fun (x : α) ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
⊢ (fun (x : α) ↦ (ρ x).toReal) =ᶠ[ae (μ.restrict s)] g

Tactic:
have h_toReal_ae : (fun x ↦ (ρ x).toReal) =ᵐ[μ.restrict s] g := by
    apply hg0.mono
    intro x hx
    simpa [ρ]
-- Module: Mathlib.MeasureTheory.Integral.MeanValue
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (ε := ℝ) (fun (x : α) ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : (x : α) → ENNReal := fun (x : α) ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
h_toReal_ae : (fun (x : α) ↦ (ρ x).toReal) =ᶠ[ae (μ.restrict s)] g
h : (ae (μ.restrict s)).EventuallyEq (β := ℝ) (fun (a : α) ↦ f a * g a) fun (a : α) ↦ (ρ a).toReal * f a
⊢ Eq (α := ℝ) (∫ (x : α) in s, f x * g x ∂μ) (∫ (x : α) in s, (ρ x).toReal * f x ∂μ)

Tactic:
apply MeasureTheory.integral_congr_ae

Premises used: MeasureTheory.integral_congr_ae
-- Module: Mathlib.MeasureTheory.Integral.MeanValue
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (ε := ℝ) (fun (x : α) ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : (x : α) → ENNReal := fun (x : α) ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
h_toReal_ae : (fun (x : α) ↦ (ρ x).toReal) =ᶠ[ae (μ.restrict s)] g
h :
  ∀ (x : α),
    (fun (x : α) ↦ (ρ x).toReal) x = g x →
      Eq (α := ℝ) ((fun (a : α) ↦ f a * g a) x) ((fun (a : α) ↦ (ρ a).toReal * f a) x)
⊢ (ae (μ.restrict s)).EventuallyEq (β := ℝ) (fun (a : α) ↦ f a * g a) fun (a : α) ↦ (ρ a).toReal * f a

Tactic:
apply h_toReal_ae.mono

Premises used: Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Integral.MeanValue
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (ε := ℝ) (fun (x : α) ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : (x : α) → ENNReal := fun (x : α) ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
h_toReal_ae : (fun (x : α) ↦ (ρ x).toReal) =ᶠ[ae (μ.restrict s)] g
x : α
hx : (fun (x : α) ↦ (ρ x).toReal) x = g x
⊢ Eq (α := ℝ) ((fun (a : α) ↦ f a * g a) x) ((fun (a : α) ↦ (ρ a).toReal * f a) x)

Tactic:
simp [hx, mul_comm]

Premises used: mul_comm
-- Module: Mathlib.MeasureTheory.Integral.MeanValue
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (ε := ℝ) (fun (x : α) ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : (x : α) → ENNReal := fun (x : α) ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
h_toReal_ae : (fun (x : α) ↦ (ρ x).toReal) =ᶠ[ae (μ.restrict s)] g
⊢ Eq (α := ℝ) (∫ (x : α) in s, f x ∂μ.withDensity fun (x : α) ↦ ρ x) (∫ (x : α) in s, (ρ x).toReal • f x ∂μ)

Tactic:
have h := setIntegral_withDensity_eq_setIntegral_toReal_smul₀ hρ_ae hρ_top f hs_meas
-- Module: Mathlib.MeasureTheory.Integral.MeanValue
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (ε := ℝ) (fun (x : α) ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : (x : α) → ENNReal := fun (x : α) ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
h_toReal_ae : (fun (x : α) ↦ (ρ x).toReal) =ᶠ[ae (μ.restrict s)] g
h : Eq (α := ℝ) (∫ (x : α) in s, f x ∂μ.withDensity fun (x : α) ↦ ρ x) (∫ (x : α) in s, (ρ x).toReal • f x ∂μ)
⊢ Eq (α := ℝ) (∫ (x : α) in s, (ρ x).toReal * f x ∂μ) (∫ (x : α) in s, f x ∂ν)

Tactic:
simp [ν, h]
-- Module: Mathlib.MeasureTheory.Integral.MeanValue
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (ε := ℝ) (fun (x : α) ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : (x : α) → ENNReal := fun (x : α) ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
h_toReal_ae : (fun (x : α) ↦ (ρ x).toReal) =ᶠ[ae (μ.restrict s)] g
_ : Eq (α := ℝ) (∫ (x : α) in s, f x * g x ∂μ) (∫ (x : α) in s, (ρ x).toReal * f x ∂μ)
_₁ : Eq (α := ℝ) (∫ (x : α) in s, (ρ x).toReal * f x ∂μ) (∫ (x : α) in s, f x ∂ν)
⊢ Eq (α := ℝ) (∫ (x : α) in s, f x * g x ∂μ) (∫ (x : α) in s, f x ∂ν)

Tactic:
calc
      _ = ∫ x in s, (ρ x).toReal * f x ∂μ := by
        apply MeasureTheory.integral_congr_ae
        apply h_toReal_ae.mono
        intro x hx
        simp [hx, mul_comm]
      _ = _ := by
        have h := setIntegral_withDensity_eq_setIntegral_toReal_smul₀ hρ_ae hρ_top f hs_meas
        simp [ν, h]
-- Module: Mathlib.MeasureTheory.Integral.MeanValue
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (ε := ℝ) (fun (x : α) ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : (x : α) → ENNReal := fun (x : α) ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
h_toReal_ae : (fun (x : α) ↦ (ρ x).toReal) =ᶠ[ae (μ.restrict s)] g
⊢ Eq (α := ℝ) (∫ (x : α) in s, f x * g x ∂μ) (∫ (x : α) in s, f x ∂ν)

Tactic:
have heq : ∫ x in s, f x * g x ∂μ = ∫ x in s, f x ∂ν := by
    calc
      _ = ∫ x in s, (ρ x).toReal * f x ∂μ := by
        apply MeasureTheory.integral_congr_ae
        apply h_toReal_ae.mono
        intro x hx
        simp [hx, mul_comm]
      _ = _ := by
        have h := setIntegral_withDensity_eq_setIntegral_toReal_smul₀ hρ_ae hρ_top f hs_meas
        simp [ν, h]
-- Module: Mathlib.MeasureTheory.Integral.MeanValue
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (ε := ℝ) (fun (x : α) ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : (x : α) → ENNReal := fun (x : α) ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
h_toReal_ae : (fun (x : α) ↦ (ρ x).toReal) =ᶠ[ae (μ.restrict s)] g
heq : Eq (α := ℝ) (∫ (x : α) in s, f x * g x ∂μ) (∫ (x : α) in s, f x ∂ν)
⊢ Eq (α := ℝ) (∫ (x : α) in s, (fun (x : α) ↦ (1 : ℝ)) x ∂μ.withDensity fun (x : α) ↦ ρ x)
    (∫ (x : α) in s, HSMul.hSMul (β := ℝ) (ρ x).toReal ((fun (x : α) ↦ (1 : ℝ)) x) ∂μ)

Tactic:
have h := setIntegral_withDensity_eq_setIntegral_toReal_smul₀
      hρ_ae hρ_top (fun _ ↦ (1 : ℝ)) hs_meas
-- Module: Mathlib.MeasureTheory.Integral.MeanValue
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (ε := ℝ) (fun (x : α) ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : (x : α) → ENNReal := fun (x : α) ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
h_toReal_ae : (fun (x : α) ↦ (ρ x).toReal) =ᶠ[ae (μ.restrict s)] g
heq : Eq (α := ℝ) (∫ (x : α) in s, f x * g x ∂μ) (∫ (x : α) in s, f x ∂ν)
h :
  Eq (α := ℝ) (∫ (x : α) in s, (fun (x : α) ↦ (1 : ℝ)) x ∂μ.withDensity fun (x : α) ↦ ρ x)
    (∫ (x : α) in s, HSMul.hSMul (β := ℝ) (ρ x).toReal ((fun (x : α) ↦ (1 : ℝ)) x) ∂μ)
rw rw₁ : Eq (α := ℝ) (∫ (x : α) in s, g x ∂μ) (∫ (a : α) in s, g a ∂μ)
⊢ Eq (α := ℝ) (∫ (x : α) in s, g x ∂μ) (∫ (x : α) in s, (ρ x).toReal ∂μ)

Tactic:
rw [integral_congr_ae h_toReal_ae]

Premises used: MeasureTheory.integral_congr_ae
-- Module: Mathlib.MeasureTheory.Integral.MeanValue
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (ε := ℝ) (fun (x : α) ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : (x : α) → ENNReal := fun (x : α) ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
h_toReal_ae : (fun (x : α) ↦ (ρ x).toReal) =ᶠ[ae (μ.restrict s)] g
heq : Eq (α := ℝ) (∫ (x : α) in s, f x * g x ∂μ) (∫ (x : α) in s, f x ∂ν)
h :
  Eq (α := ℝ) (∫ (x : α) in s, (fun (x : α) ↦ (1 : ℝ)) x ∂μ.withDensity fun (x : α) ↦ ρ x)
    (∫ (x : α) in s, HSMul.hSMul (β := ℝ) (ρ x).toReal ((fun (x : α) ↦ (1 : ℝ)) x) ∂μ)
⊢ Eq (α := ℝ) (∫ (x : α) in s, (ρ x).toReal ∂μ) (∫ (x : α) in s, 1 ∂ν)

Tactic:
simp [ν, h]
-- Module: Mathlib.MeasureTheory.Integral.MeanValue
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (ε := ℝ) (fun (x : α) ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : (x : α) → ENNReal := fun (x : α) ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
h_toReal_ae : (fun (x : α) ↦ (ρ x).toReal) =ᶠ[ae (μ.restrict s)] g
heq : Eq (α := ℝ) (∫ (x : α) in s, f x * g x ∂μ) (∫ (x : α) in s, f x ∂ν)
h :
  Eq (α := ℝ) (∫ (x : α) in s, (fun (x : α) ↦ (1 : ℝ)) x ∂μ.withDensity fun (x : α) ↦ ρ x)
    (∫ (x : α) in s, HSMul.hSMul (β := ℝ) (ρ x).toReal ((fun (x : α) ↦ (1 : ℝ)) x) ∂μ)
_ : Eq (α := ℝ) (∫ (x : α) in s, g x ∂μ) (∫ (x : α) in s, (ρ x).toReal ∂μ)
_₁ : Eq (α := ℝ) (∫ (x : α) in s, (ρ x).toReal ∂μ) (∫ (x : α) in s, 1 ∂ν)
⊢ Eq (α := ℝ) (∫ (x : α) in s, g x ∂μ) (∫ (x : α) in s, 1 ∂ν)

Tactic:
calc
      _ = ∫ x in s, (ρ x).toReal ∂μ := by rw [integral_congr_ae h_toReal_ae]
      _ = _ := by simp [ν, h]