awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanValue (goal)
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 ∂ν)
⊢ ∃ c ∈ s, ∫ (x : α) in s, f x * g x ∂μ = f c * ∫ (x : α) in s, g x ∂μ
have 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 ∂μ
Tactic: by_cases hν0 : ∫ x in s, (1 : ℝ) ∂ν = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanValue (goal)
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 ∂μ
⊢ ∃ c ∈ s, ∫ (x : α) in s, f x * g x ∂μ = f c * ∫ (x : α) in s, g x ∂μ
have 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 ∂μ
Tactic: by_cases hν0 : ∫ x in s, (1 : ℝ) ∂ν = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanValue (goal)
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 ∈ s, ∫ (x : α) in s, f x * g x ∂μ = f c * ∫ (x : α) in s, g x ∂μ
have pos : ∀ (c : α) (hc : c ∈ s), ∃ c ∈ s, ∫ (x : α) in s, f x * g x ∂μ = f c * ∫ (x : α) in s, g x ∂μ
Tactic: rcases hs_conn.nonempty with ⟨c, hc⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanValue (goal)
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 ∂μ
have pos : ∫ (x : α) in s, f x * g x ∂μ = f c * ∫ (x : α) in s, g x ∂μ
Tactic: refine ⟨c, hc, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanValue (goal)
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
have 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
Tactic: rw [hν0, setIntegral_eq_zero_iff_of_nonneg_ae hg0 hg] at hg1
Cleared hypotheses: hg1, hν0, c, hc
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanValue (goal)
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
have apply : ∀ (x : α), g x = 0 x → Eq (α := ℝ) ((fun (x : α) ↦ f x * g x) x) (0 x)
Tactic: apply hg1.mono
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanValue (hypothesis)
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
have heq_ae : (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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanValue (hypothesis)
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 ∂ν) 0
have heq_zero : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanValue (goal)
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
⊢ Eq (α := ℝ) (∫ (x : α) in s, f x ∂ν) 0
have rw₁ : Eq (α := ℝ) 0 0
Tactic: rw [← heq, heq_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanValue (goal)
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
⊢ ∫ (x : α) in s, f x * g x ∂μ = f c * ∫ (x : α) in s, g x ∂μ
have _ : Eq (α := ℝ) (∫ (x : α) in s, f x ∂ν) 0
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanValue (goal)
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
⊢ ∫ (x : α) in s, f x * g x ∂μ = f c * ∫ (x : α) in s, g x ∂μ
have _₁ : 0 = 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanValue (hypothesis)
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 ∈ s, ∫ (x : α) in s, f x * g x ∂μ = f c * ∫ (x : α) in s, g x ∂μ
have hν0' : ENNReal.toReal ((ν : (a : Set α) → ENNReal) s) ≠ 0
Tactic: have hν0' : (ν s).toReal ≠ 0 := by simpa using hν0
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanValue (goal)
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)
⊢ False
have apply : ENNReal.toReal ((ν : (a : Set α) → ENNReal) s) = 0
Tactic: apply hν0'
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanValue (hypothesis)
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
⊢ ∃ c ∈ s, ∫ (x : α) in s, f x * g x ∂μ = f c * ∫ (x : α) in s, g x ∂μ
have hνfin : Ne (α := ENNReal) ((ν : (a : Set α) → ENNReal) s : ENNReal) (⊤ : ENNReal)
Tactic: have hνfin : ν s ≠ ⊤ := by intro this; apply hν0'; simp [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanValue (goal)
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)
⊢ False
have apply : ENNReal.toReal ((ν : (a : Set α) → ENNReal) s) = 0
Tactic: apply hν0'
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanValue (hypothesis)
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)
⊢ ∃ c ∈ s, ∫ (x : α) in s, f x * g x ∂μ = f c * ∫ (x : α) in s, g x ∂μ
have hν0'' : Ne (α := ENNReal) ((ν : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
Tactic: have hν0'' : ν s ≠ 0 := by intro this; apply hν0'; simp [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanValue (goal)
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
have apply : ∀ (x : α),
  (fun (x : α) ↦ (ρ x).toReal) x = g x →
    Eq (α := ℝ) ((fun (x : α) ↦ (ρ x).toReal * f x) x) ((fun (x : α) ↦ f x * g x) x)
Tactic: apply h_toReal_ae.mono
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanValue (hypothesis)
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 ν
have hmul_ae : (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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanValue (hypothesis)
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 f s ν
have h_IntOn : 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanValue (goal)
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 ρ)
have rwa : Integrable (ε := ℝ) (fun (x : α) ↦ (ρ x).toReal • f x) (μ.restrict s)
Tactic: rwa [integrable_withDensity_iff_integrable_smul₀' hρ_ae hρ_top, ← IntegrableOn]