awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ∂ν)
hg1 : Eq (α := ℝ) (∫ (x : α) in s, g x ∂μ) (∫ (x : α) in s, 1 ∂ν)
hν0 : ¬Eq (α := ℝ) (∫ (x : α) in s, 1 ∂ν) 0
hν0' : ENNReal.toReal ((ν : (a : Set α) → ENNReal) s) ≠ 0
hνfin : Ne (α := ENNReal) ((ν : (a : Set α) → ENNReal) s : ENNReal) (⊤ : ENNReal)
hν0'' : Ne (α := ENNReal) ((ν : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
x : α
hx : (fun (x : α) ↦ (ρ x).toReal) x = g x
⊢ Eq (α := ℝ) ((fun (x : α) ↦ (ρ x).toReal * f x) x) ((fun (x : α) ↦ f x * g x) 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
heq : Eq (α := ℝ) (∫ (x : α) in s, f x * g x ∂μ) (∫ (x : α) in s, f x ∂ν)
hg1 : Eq (α := ℝ) (∫ (x : α) in s, g x ∂μ) (∫ (x : α) in s, 1 ∂ν)
hν0 : ¬Eq (α := ℝ) (∫ (x : α) in s, 1 ∂ν) 0
hν0' : ENNReal.toReal ((ν : (a : Set α) → ENNReal) s) ≠ 0
hνfin : Ne (α := ENNReal) ((ν : (a : Set α) → ENNReal) s : ENNReal) (⊤ : ENNReal)
hν0'' : Ne (α := ENNReal) ((ν : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
⊢ (ae (μ.restrict s)).EventuallyEq (β := ℝ) (fun (x : α) ↦ (ρ x).toReal * f x) fun (x : α) ↦ f x * g x

Tactic:
have hmul_ae : (fun x ↦ (ρ x).toReal * f x) =ᵐ[μ.restrict s] (fun x ↦ f x * g x) := by
        apply h_toReal_ae.mono
        intro x hx
        simp [hx, 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
heq : Eq (α := ℝ) (∫ (x : α) in s, f x * g x ∂μ) (∫ (x : α) in s, f x ∂ν)
hg1 : Eq (α := ℝ) (∫ (x : α) in s, g x ∂μ) (∫ (x : α) in s, 1 ∂ν)
hν0 : ¬Eq (α := ℝ) (∫ (x : α) in s, 1 ∂ν) 0
hν0' : ENNReal.toReal ((ν : (a : Set α) → ENNReal) s) ≠ 0
hνfin : Ne (α := ENNReal) ((ν : (a : Set α) → ENNReal) s : ENNReal) (⊤ : ENNReal)
hν0'' : Ne (α := ENNReal) ((ν : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
hmul_ae : (ae (μ.restrict s)).EventuallyEq (β := ℝ) (fun (x : α) ↦ (ρ x).toReal * f x) fun (x : α) ↦ f x * g x
rwa rwa₁ rwa₂ rwa₃ : IntegrableOn (ε := ℝ) (fun (x : α) ↦ f x * g x) s μ
⊢ IntegrableOn (ε := ℝ) (fun (x : α) ↦ (ρ x).toReal * f x) s μ

Tactic:
rwa [integrableOn_congr_fun_ae hmul_ae]

Premises used: MeasureTheory.integrableOn_congr_fun_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 ∂ν)
hg1 : Eq (α := ℝ) (∫ (x : α) in s, g x ∂μ) (∫ (x : α) in s, 1 ∂ν)
hν0 : ¬Eq (α := ℝ) (∫ (x : α) in s, 1 ∂ν) 0
hν0' : ENNReal.toReal ((ν : (a : Set α) → ENNReal) s) ≠ 0
hνfin : Ne (α := ENNReal) ((ν : (a : Set α) → ENNReal) s : ENNReal) (⊤ : ENNReal)
hν0'' : Ne (α := ENNReal) ((ν : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
hmul_ae : (ae (μ.restrict s)).EventuallyEq (β := ℝ) (fun (x : α) ↦ (ρ x).toReal * f x) fun (x : α) ↦ f x * g x
⊢ IntegrableOn (ε := ℝ) (fun (x : α) ↦ (ρ x).toReal * f x) s μ

Tactic:
have h_IntOn : IntegrableOn (fun x ↦ (ρ x).toReal * f x) s μ := by
        rwa [integrableOn_congr_fun_ae hmul_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 ∂ν)
hg1 : Eq (α := ℝ) (∫ (x : α) in s, g x ∂μ) (∫ (x : α) in s, 1 ∂ν)
hν0 : ¬Eq (α := ℝ) (∫ (x : α) in s, 1 ∂ν) 0
hν0' : ENNReal.toReal ((ν : (a : Set α) → ENNReal) s) ≠ 0
hνfin : Ne (α := ENNReal) ((ν : (a : Set α) → ENNReal) s : ENNReal) (⊤ : ENNReal)
hν0'' : Ne (α := ENNReal) ((ν : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
hmul_ae : (ae (μ.restrict s)).EventuallyEq (β := ℝ) (fun (x : α) ↦ (ρ x).toReal * f x) fun (x : α) ↦ f x * g x
h_IntOn : IntegrableOn (ε := ℝ) (fun (x : α) ↦ (ρ x).toReal * f x) s μ
rwa : Integrable (ε := ℝ) (fun (x : α) ↦ (ρ x).toReal • f x) (μ.restrict s)
rwa₁ rwa₂ rwa₃ rwa₄ : IntegrableOn (ε := ℝ) (fun (x : α) ↦ (ρ x).toReal • f x) s μ
⊢ Integrable f ((μ.restrict s).withDensity ρ)

Tactic:
rwa [integrable_withDensity_iff_integrable_smul₀' hρ_ae hρ_top, ← IntegrableOn]

Premises used: MeasureTheory.integrable_withDensity_iff_integrable_smul₀', MeasureTheory.IntegrableOn
-- 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 ∂ν)
hg1 : Eq (α := ℝ) (∫ (x : α) in s, g x ∂μ) (∫ (x : α) in s, 1 ∂ν)
hν0 : ¬Eq (α := ℝ) (∫ (x : α) in s, 1 ∂ν) 0
hν0' : ENNReal.toReal ((ν : (a : Set α) → ENNReal) s) ≠ 0
hνfin : Ne (α := ENNReal) ((ν : (a : Set α) → ENNReal) s : ENNReal) (⊤ : ENNReal)
hν0'' : Ne (α := ENNReal) ((ν : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
hmul_ae : (ae (μ.restrict s)).EventuallyEq (β := ℝ) (fun (x : α) ↦ (ρ x).toReal * f x) fun (x : α) ↦ f x * g x
h_IntOn : IntegrableOn (ε := ℝ) (fun (x : α) ↦ (ρ x).toReal * f x) s μ
⊢ Integrable f ((μ.restrict s).withDensity ρ)

Tactic:
have h_Int : Integrable f ((μ.restrict s).withDensity ρ) := by
        rwa [integrable_withDensity_iff_integrable_smul₀' hρ_ae hρ_top, ← IntegrableOn]
-- 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 ∂ν)
hg1 : Eq (α := ℝ) (∫ (x : α) in s, g x ∂μ) (∫ (x : α) in s, 1 ∂ν)
hν0 : ¬Eq (α := ℝ) (∫ (x : α) in s, 1 ∂ν) 0
hν0' : ENNReal.toReal ((ν : (a : Set α) → ENNReal) s) ≠ 0
hνfin : Ne (α := ENNReal) ((ν : (a : Set α) → ENNReal) s : ENNReal) (⊤ : ENNReal)
hν0'' : Ne (α := ENNReal) ((ν : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
hmul_ae : (ae (μ.restrict s)).EventuallyEq (β := ℝ) (fun (x : α) ↦ (ρ x).toReal * f x) fun (x : α) ↦ f x * g x
h_IntOn : IntegrableOn (ε := ℝ) (fun (x : α) ↦ (ρ x).toReal * f x) s μ
h_Int : Integrable f ((μ.restrict s).withDensity ρ)
h :
  ∀ (t : Set α) (ht : MeasurableSet t),
    Eq (α := ENNReal) ((ν.restrict s : (a : Set α) → ENNReal) t : ENNReal)
      (((μ.restrict s).withDensity ρ : (a : Set α) → ENNReal) t : ENNReal)
⊢ ν.restrict s = (μ.restrict s).withDensity ρ

Tactic:
ext t ht
-- 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 ∂ν)
hg1 : Eq (α := ℝ) (∫ (x : α) in s, g x ∂μ) (∫ (x : α) in s, 1 ∂ν)
hν0 : ¬Eq (α := ℝ) (∫ (x : α) in s, 1 ∂ν) 0
hν0' : ENNReal.toReal ((ν : (a : Set α) → ENNReal) s) ≠ 0
hνfin : Ne (α := ENNReal) ((ν : (a : Set α) → ENNReal) s : ENNReal) (⊤ : ENNReal)
hν0'' : Ne (α := ENNReal) ((ν : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
hmul_ae : (ae (μ.restrict s)).EventuallyEq (β := ℝ) (fun (x : α) ↦ (ρ x).toReal * f x) fun (x : α) ↦ f x * g x
h_IntOn : IntegrableOn (ε := ℝ) (fun (x : α) ↦ (ρ x).toReal * f x) s μ
h_Int : Integrable f ((μ.restrict s).withDensity ρ)
t : Set α
ht : MeasurableSet t
⊢ Eq (α := ENNReal) ((ν.restrict s : (a : Set α) → ENNReal) t : ENNReal)
    (((μ.restrict s).withDensity ρ : (a : Set α) → ENNReal) t : ENNReal)

Tactic:
simp [ht, ν, 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 ∂ν)
hg1 : Eq (α := ℝ) (∫ (x : α) in s, g x ∂μ) (∫ (x : α) in s, 1 ∂ν)
hν0 : ¬Eq (α := ℝ) (∫ (x : α) in s, 1 ∂ν) 0
hν0' : ENNReal.toReal ((ν : (a : Set α) → ENNReal) s) ≠ 0
hνfin : Ne (α := ENNReal) ((ν : (a : Set α) → ENNReal) s : ENNReal) (⊤ : ENNReal)
hν0'' : Ne (α := ENNReal) ((ν : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
hmul_ae : (ae (μ.restrict s)).EventuallyEq (β := ℝ) (fun (x : α) ↦ (ρ x).toReal * f x) fun (x : α) ↦ f x * g x
h_IntOn : IntegrableOn (ε := ℝ) (fun (x : α) ↦ (ρ x).toReal * f x) s μ
h_Int : Integrable f ((μ.restrict s).withDensity ρ)
⊢ ν.restrict s = (μ.restrict s).withDensity ρ

Tactic:
have hνrs : ν.restrict s = (μ.restrict s).withDensity ρ := by
        ext t ht
        simp [ht, ν, 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 ∂ν)
hg1 : Eq (α := ℝ) (∫ (x : α) in s, g x ∂μ) (∫ (x : α) in s, 1 ∂ν)
hν0 : ¬Eq (α := ℝ) (∫ (x : α) in s, 1 ∂ν) 0
hν0' : ENNReal.toReal ((ν : (a : Set α) → ENNReal) s) ≠ 0
hνfin : Ne (α := ENNReal) ((ν : (a : Set α) → ENNReal) s : ENNReal) (⊤ : ENNReal)
hν0'' : Ne (α := ENNReal) ((ν : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
hmul_ae : (ae (μ.restrict s)).EventuallyEq (β := ℝ) (fun (x : α) ↦ (ρ x).toReal * f x) fun (x : α) ↦ f x * g x
h_IntOn : IntegrableOn (ε := ℝ) (fun (x : α) ↦ (ρ x).toReal * f x) s μ
h_Int : Integrable f ((μ.restrict s).withDensity ρ)
hνrs : ν.restrict s = (μ.restrict s).withDensity ρ
⊢ IntegrableOn f s ν

Tactic:
simpa [IntegrableOn, hνrs] using h_Int

Premises used: MeasureTheory.IntegrableOn
-- 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 ∂ν)
hg1 : Eq (α := ℝ) (∫ (x : α) in s, g x ∂μ) (∫ (x : α) in s, 1 ∂ν)
hν0 : ¬Eq (α := ℝ) (∫ (x : α) in s, 1 ∂ν) 0
hν0' : ENNReal.toReal ((ν : (a : Set α) → ENNReal) s) ≠ 0
hνfin : Ne (α := ENNReal) ((ν : (a : Set α) → ENNReal) s : ENNReal) (⊤ : ENNReal)
hν0'' : Ne (α := ENNReal) ((ν : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
⊢ IntegrableOn f s ν

Tactic:
have hint : IntegrableOn f s ν := by
      have hmul_ae : (fun x ↦ (ρ x).toReal * f x) =ᵐ[μ.restrict s] (fun x ↦ f x * g x) := by
        apply h_toReal_ae.mono
        intro x hx
        simp [hx, mul_comm]
      have h_IntOn : IntegrableOn (fun x ↦ (ρ x).toReal * f x) s μ := by
        rwa [integrableOn_congr_fun_ae hmul_ae]
      have h_Int : Integrable f ((μ.restrict s).withDensity ρ) := by
        rwa [integrable_withDensity_iff_integrable_smul₀' hρ_ae hρ_top, ← IntegrableOn]
      have hνrs : ν.restrict s = (μ.restrict s).withDensity ρ := by
        ext t ht
        simp [ht, ν, hs_meas]
      simpa [IntegrableOn, hνrs] using h_Int
-- 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 ∂ν)
hg1 : Eq (α := ℝ) (∫ (x : α) in s, g x ∂μ) (∫ (x : α) in s, 1 ∂ν)
hν0 : ¬Eq (α := ℝ) (∫ (x : α) in s, 1 ∂ν) 0
hν0' : ENNReal.toReal ((ν : (a : Set α) → ENNReal) s) ≠ 0
hνfin : Ne (α := ENNReal) ((ν : (a : Set α) → ENNReal) s : ENNReal) (⊤ : ENNReal)
hν0'' : Ne (α := ENNReal) ((ν : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
hint : IntegrableOn f s ν
neg :
  ∀ (c : α) (hc : c ∈ s) (h_ave : f c = ⨍ (x : α) in s, f x ∂ν),
    ∃ c ∈ s, ∫ (x : α) in s, f x * g x ∂μ = f c * ∫ (x : α) in s, g x ∂μ
⊢ ∃ c ∈ s, ∫ (x : α) in s, f x * g x ∂μ = f c * ∫ (x : α) in s, g x ∂μ

Tactic:
obtain ⟨c, hc, h_ave⟩ := exists_eq_setAverage hs_conn hf hint hνfin hν0''

Premises used: MeasureTheory.exists_eq_setAverage
-- 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 ∂ν)
hg1 : Eq (α := ℝ) (∫ (x : α) in s, g x ∂μ) (∫ (x : α) in s, 1 ∂ν)
hν0 : ¬Eq (α := ℝ) (∫ (x : α) in s, 1 ∂ν) 0
hν0' : ENNReal.toReal ((ν : (a : Set α) → ENNReal) s) ≠ 0
hνfin : Ne (α := ENNReal) ((ν : (a : Set α) → ENNReal) s : ENNReal) (⊤ : ENNReal)
hν0'' : Ne (α := ENNReal) ((ν : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
hint : IntegrableOn f s ν
c : α
hc : c ∈ s
h_ave : f c = ⨍ (x : α) in s, f x ∂ν
⊢ ∃ c ∈ s, ∫ (x : α) in s, f x * g x ∂μ = f c * ∫ (x : α) in s, g x ∂μ

Tactic:
⟨c, hc, ?_⟩

Premises used: And.intro, Exists.intro
-- 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 ∂ν)
hg1 : Eq (α := ℝ) (∫ (x : α) in s, g x ∂μ) (∫ (x : α) in s, 1 ∂ν)
hν0 : ¬Eq (α := ℝ) (∫ (x : α) in s, 1 ∂ν) 0
hν0' : ENNReal.toReal ((ν : (a : Set α) → ENNReal) s) ≠ 0
hνfin : Ne (α := ENNReal) ((ν : (a : Set α) → ENNReal) s : ENNReal) (⊤ : ENNReal)
hν0'' : Ne (α := ENNReal) ((ν : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
hint : IntegrableOn f s ν
c : α
hc : c ∈ s
h_ave : f c = ⨍ (x : α) in s, f x ∂ν
neg : ∫ (x : α) in s, f x * g x ∂μ = f c * ∫ (x : α) in s, g x ∂μ
⊢ ∃ c ∈ s, ∫ (x : α) in s, f x * g x ∂μ = f c * ∫ (x : α) in s, g x ∂μ

Tactic:
refine ⟨c, hc, ?_⟩
-- 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 ∂ν)
hg1 : Eq (α := ℝ) (∫ (x : α) in s, g x ∂μ) (∫ (x : α) in s, 1 ∂ν)
hν0 : ¬Eq (α := ℝ) (∫ (x : α) in s, 1 ∂ν) 0
hν0' : ENNReal.toReal ((ν : (a : Set α) → ENNReal) s) ≠ 0
hνfin : Ne (α := ENNReal) ((ν : (a : Set α) → ENNReal) s : ENNReal) (⊤ : ENNReal)
hν0'' : Ne (α := ENNReal) ((ν : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
hint : IntegrableOn f s ν
c : α
hc : c ∈ s
h_ave : f c = ⨍ (x : α) in s, f x ∂ν
⊢ Eq (α := ℝ) (∫ (x : α) in s, f x * g x ∂μ) (∫ (x : α) in s, f x ∂ν)

Tactic:
heq
-- 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 ∂ν)
hg1 : Eq (α := ℝ) (∫ (x : α) in s, g x ∂μ) (∫ (x : α) in s, 1 ∂ν)
hν0 : ¬Eq (α := ℝ) (∫ (x : α) in s, 1 ∂ν) 0
hν0' : ENNReal.toReal ((ν : (a : Set α) → ENNReal) s) ≠ 0
hνfin : Ne (α := ENNReal) ((ν : (a : Set α) → ENNReal) s : ENNReal) (⊤ : ENNReal)
hν0'' : Ne (α := ENNReal) ((ν : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
hint : IntegrableOn f s ν
c : α
hc : c ∈ s
h_ave : f c = ⨍ (x : α) in s, f x ∂ν
rw : ∫ (x : α) in s, f x ∂ν = HMul.hMul (α := ℝ) (⨍ (x : α) in s, f x ∂ν) (∫ (x : α) in s, 1 ∂ν)
⊢ ∫ (x : α) in s, f x ∂ν = f c * ∫ (x : α) in s, 1 ∂ν

Tactic:
rw [h_ave]
-- 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 ∂ν)
hg1 : Eq (α := ℝ) (∫ (x : α) in s, g x ∂μ) (∫ (x : α) in s, 1 ∂ν)
hν0 : ¬Eq (α := ℝ) (∫ (x : α) in s, 1 ∂ν) 0
hν0' : ENNReal.toReal ((ν : (a : Set α) → ENNReal) s) ≠ 0
hνfin : Ne (α := ENNReal) ((ν : (a : Set α) → ENNReal) s : ENNReal) (⊤ : ENNReal)
hν0'' : Ne (α := ENNReal) ((ν : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
hint : IntegrableOn f s ν
c : α
hc : c ∈ s
h_ave : f c = ⨍ (x : α) in s, f x ∂ν
simp : ∫ (x : α) in s, f x ∂ν = ((ν.real s)⁻¹ * ∫ (x : α) in s, f x ∂ν) * ν.real s
⊢ ∫ (x : α) in s, f x ∂ν = HMul.hMul (α := ℝ) (⨍ (x : α) in s, f x ∂ν) (∫ (x : α) in s, 1 ∂ν)

Tactic:
simp only [setAverage_eq, smul_eq_mul, integral_const, MeasurableSet.univ,
          measureReal_restrict_apply, Set.univ_inter, mul_one]

Premises used: Set.univ_inter, MeasureTheory.setAverage_eq, MeasureTheory.integral_const, smul_eq_mul, mul_one, MeasureTheory.measureReal_restrict_apply, MeasurableSet.univ