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 ∂ν)
⊢ Eq (α := ℝ) (∫ (x : α) in s, g x ∂μ) (∫ (x : α) in s, 1 ∂ν)

Tactic:
have hg1 : ∫ x in s, g x ∂μ = ∫ x in s, (1 : ℝ) ∂ν := by
    have h := setIntegral_withDensity_eq_setIntegral_toReal_smul₀
      hρ_ae hρ_top (fun _ ↦ (1 : ℝ)) hs_meas
    calc
      _ = ∫ x in s, (ρ x).toReal ∂μ := by rw [integral_congr_ae h_toReal_ae]
      _ = _ := by 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 ∂ν)
hg1 : Eq (α := ℝ) (∫ (x : α) in s, g x ∂μ) (∫ (x : α) in s, 1 ∂ν)
pos :
  ∀ (hν0 : Eq (α := ℝ) (∫ (x : α) in s, 1 ∂ν) 0), ∃ c ∈ s, ∫ (x : α) in s, f x * g x ∂μ = f c * ∫ (x : α) in s, g x ∂μ
neg :
  ∀ (hν0 : ¬Eq (α := ℝ) (∫ (x : α) in s, 1 ∂ν) 0), ∃ 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:
by_cases hν0 : ∫ x in s, (1 : ℝ) ∂ν = 0

Premises used: OfNat.ofNat
-- 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
pos : ∀ (c : α) (hc : c ∈ s), ∃ 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:
rcases hs_conn.nonempty with ⟨c, hc⟩

Premises used: IsConnected.nonempty
-- 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
c : α
hc : c ∈ s
⊢ ∃ 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
c : α
hc : c ∈ s
pos : ∫ (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
c : α
hc : c ∈ s
⊢ 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
c : α
hc : c ∈ s
rw :
  ∀ (hg1 : g =ᶠ[ae (μ.restrict s)] 0) (hν0 : Eq (α := ℝ) (∫ (x : α) in s, 1 ∂ν) 0) (c : α) (hc : c ∈ s),
    Eq (α := ℝ) (∫ (x : α) in s, f x ∂ν) 0
⊢ Eq (α := ℝ) (∫ (x : α) in s, f x ∂ν) 0

Tactic:
rw [hν0, setIntegral_eq_zero_iff_of_nonneg_ae hg0 hg] at hg1

Premises used: MeasureTheory.setIntegral_eq_zero_iff_of_nonneg_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 : g =ᶠ[ae (μ.restrict s)] 0
hν0 : Eq (α := ℝ) (∫ (x : α) in s, 1 ∂ν) 0
c : α
hc : c ∈ s
apply : ∀ (x : α), g x = 0 x → Eq (α := ℝ) ((fun (x : α) ↦ f x * g x) x) (0 x)
⊢ (ae (μ.restrict s)).EventuallyEq (β := ℝ) (fun (x : α) ↦ f x * g x) 0

Tactic:
apply hg1.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
heq : Eq (α := ℝ) (∫ (x : α) in s, f x * g x ∂μ) (∫ (x : α) in s, f x ∂ν)
hg1 : g =ᶠ[ae (μ.restrict s)] 0
hν0 : Eq (α := ℝ) (∫ (x : α) in s, 1 ∂ν) 0
c : α
hc : c ∈ s
x : α
hx : g x = 0 x
⊢ Eq (α := ℝ) ((fun (x : α) ↦ f x * g x) x) (0 x)

Tactic:
simp [hx]
-- 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 : g =ᶠ[ae (μ.restrict s)] 0
hν0 : Eq (α := ℝ) (∫ (x : α) in s, 1 ∂ν) 0
c : α
hc : c ∈ s
⊢ (ae (μ.restrict s)).EventuallyEq (β := ℝ) (fun (x : α) ↦ f x * g x) 0

Tactic:
have heq_ae : (fun x ↦ f x * g x) =ᵐ[μ.restrict s] 0 := by
            apply hg1.mono
            intro x hx
            simp [hx]
-- 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 : g =ᶠ[ae (μ.restrict s)] 0
hν0 : Eq (α := ℝ) (∫ (x : α) in s, 1 ∂ν) 0
c : α
hc : c ∈ s
heq_ae : (ae (μ.restrict s)).EventuallyEq (β := ℝ) (fun (x : α) ↦ f x * g x) 0
⊢ Eq (α := ℝ) (∫ (x : α) in s, f x * g x ∂μ) 0

Tactic:
simpa using integral_congr_ae heq_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 ∂ν)
hg1 : g =ᶠ[ae (μ.restrict s)] 0
hν0 : Eq (α := ℝ) (∫ (x : α) in s, 1 ∂ν) 0
c : α
hc : c ∈ s
⊢ Eq (α := ℝ) (∫ (x : α) in s, f x * g x ∂μ) 0

Tactic:
have heq_zero : ∫ x in s, f x * g x ∂μ = 0 := by
          have heq_ae : (fun x ↦ f x * g x) =ᵐ[μ.restrict s] 0 := by
            apply hg1.mono
            intro x hx
            simp [hx]
          simpa using integral_congr_ae heq_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 : g =ᶠ[ae (μ.restrict s)] 0
hν0 : Eq (α := ℝ) (∫ (x : α) in s, 1 ∂ν) 0
c : α
hc : c ∈ s
heq_zero : Eq (α := ℝ) (∫ (x : α) in s, f x * g x ∂μ) 0
rw : Eq (α := ℝ) (∫ (x : α) in s, f x * g x ∂μ) 0
rw₁ rw₂ : Eq (α := ℝ) 0 0
⊢ Eq (α := ℝ) (∫ (x : α) in s, f x ∂ν) 0

Tactic:
rw [← heq, heq_zero]
-- 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
c : α
hc : c ∈ s
⊢ 0 = f c * ∫ (x : α) in s, g x ∂μ

Tactic:
simp [hν0, hg1]
-- 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
c : α
hc : c ∈ s
_ : Eq (α := ℝ) (∫ (x : α) in s, f x ∂ν) 0
_₁ : 0 = f c * ∫ (x : α) in s, g x ∂μ
⊢ ∫ (x : α) in s, f x * g x ∂μ = f c * ∫ (x : α) in s, g x ∂μ

Tactic:
calc
      _ = ∫ x in s, f x ∂ν := heq
      _ = 0 := by
        rw [hν0, setIntegral_eq_zero_iff_of_nonneg_ae hg0 hg] at hg1
        have heq_zero : ∫ x in s, f x * g x ∂μ = 0 := by
          have heq_ae : (fun x ↦ f x * g x) =ᵐ[μ.restrict s] 0 := by
            apply hg1.mono
            intro x hx
            simp [hx]
          simpa using integral_congr_ae heq_ae
        rw [← heq, heq_zero]
      _ = _ := by simp [hν0, hg1]
-- 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
⊢ ENNReal.toReal ((ν : (a : Set α) → ENNReal) s) ≠ 0

Tactic:
simpa using hν0
-- 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
⊢ ENNReal.toReal ((ν : (a : Set α) → ENNReal) s) ≠ 0

Tactic:
have hν0' : (ν s).toReal ≠ 0 := by simpa using hν0
-- 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
this : Eq (α := ENNReal) ((ν : (a : Set α) → ENNReal) s : ENNReal) (⊤ : ENNReal)
apply : ENNReal.toReal ((ν : (a : Set α) → ENNReal) s) = 0
⊢ False

Tactic:
apply hν0'
-- 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
this : Eq (α := ENNReal) ((ν : (a : Set α) → ENNReal) s : ENNReal) (⊤ : ENNReal)
⊢ ENNReal.toReal ((ν : (a : Set α) → ENNReal) s) = 0

Tactic:
simp [this]
-- 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
⊢ Ne (α := ENNReal) ((ν : (a : Set α) → ENNReal) s : ENNReal) (⊤ : ENNReal)

Tactic:
have hνfin : ν s ≠ ⊤ := by intro this; apply hν0'; simp [this]
-- 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)
this : Eq (α := ENNReal) ((ν : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
apply : ENNReal.toReal ((ν : (a : Set α) → ENNReal) s) = 0
⊢ False

Tactic:
apply hν0'
-- 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)
this : Eq (α := ENNReal) ((ν : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
⊢ ENNReal.toReal ((ν : (a : Set α) → ENNReal) s) = 0

Tactic:
simp [this]
-- 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)
⊢ Ne (α := ENNReal) ((ν : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)

Tactic:
have hν0'' : ν s ≠ 0 := by intro this; apply hν0'; simp [this]
-- 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)
apply :
  ∀ (x : α),
    (fun (x : α) ↦ (ρ x).toReal) x = g x →
      Eq (α := ℝ) ((fun (x : α) ↦ (ρ x).toReal * f x) x) ((fun (x : α) ↦ f x * g x) x)
⊢ (ae (μ.restrict s)).EventuallyEq (β := ℝ) (fun (x : α) ↦ (ρ x).toReal * f x) fun (x : α) ↦ f x * g x

Tactic:
apply h_toReal_ae.mono

Premises used: Filter.Eventually.mono