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 ∂ν)
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)
⊢ Integrable f ((μ.restrict s).withDensity ρ)
have rwa₁ : IntegrableOn (ε := ℝ) (fun (x : α) ↦ (ρ x).toReal • f x) s μ
Tactic: rwa [integrable_withDensity_iff_integrable_smul₀' hρ_ae hρ_top, ← IntegrableOn]
-- 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
h_IntOn : IntegrableOn (ε := ℝ) (fun (x : α) ↦ (ρ x).toReal * f x) s μ
⊢ IntegrableOn f s ν
have h_Int : 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]
-- 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 μ
h_Int : Integrable f ((μ.restrict s).withDensity ρ)
⊢ ν.restrict s = (μ.restrict s).withDensity ρ
have h : ∀ (t : Set α) (ht : MeasurableSet t),
  Eq (α := ENNReal) ((ν.restrict s : (a : Set α) → ENNReal) t : ENNReal)
    (((μ.restrict s).withDensity ρ : (a : Set α) → ENNReal) t : ENNReal)
Tactic: ext t ht
-- 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
h_IntOn : IntegrableOn (ε := ℝ) (fun (x : α) ↦ (ρ x).toReal * f x) s μ
h_Int : Integrable f ((μ.restrict s).withDensity ρ)
⊢ IntegrableOn f s ν
have hνrs : ν.restrict s = (μ.restrict s).withDensity ρ
Tactic: have hνrs : ν.restrict s = (μ.restrict s).withDensity ρ := by
        ext t ht
        simp [ht, ν, hs_meas]
-- 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)
⊢ ∃ c ∈ s, ∫ (x : α) in s, f x * g x ∂μ = f c * ∫ (x : α) in s, g x ∂μ
have hint : 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
-- 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)
hint : IntegrableOn f s ν
⊢ ∃ c ∈ s, ∫ (x : α) in s, f x * g x ∂μ = f c * ∫ (x : α) in s, g x ∂μ
have 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 ∂μ
Tactic: obtain ⟨c, hc, h_ave⟩ := exists_eq_setAverage hs_conn hf hint hνfin 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
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 ∂μ
have neg : ∫ (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
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 ∂ν
⊢ ∫ (x : α) in s, f x ∂ν = f c * ∫ (x : α) in s, 1 ∂ν
have rw : ∫ (x : α) in s, f x ∂ν = HMul.hMul (α := ℝ) (⨍ (x : α) in s, f x ∂ν) (∫ (x : α) in s, 1 ∂ν)
Tactic: rw [h_ave]
-- 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)
hint : IntegrableOn f s ν
c : α
hc : c ∈ s
h_ave : f c = ⨍ (x : α) in s, f x ∂ν
⊢ ∫ (x : α) in s, f x ∂ν = HMul.hMul (α := ℝ) (⨍ (x : α) in s, f x ∂ν) (∫ (x : α) in s, 1 ∂ν)
have simp : ∫ (x : α) in s, f x ∂ν = ((ν.real s)⁻¹ * ∫ (x : α) in s, f x ∂ν) * ν.real s
Tactic: simp only [setAverage_eq, smul_eq_mul, integral_const, MeasurableSet.univ,
          measureReal_restrict_apply, Set.univ_inter, mul_one]
-- 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)
hint : IntegrableOn f s ν
c : α
hc : c ∈ s
h_ave : f c = ⨍ (x : α) in s, f x ∂ν
⊢ ∫ (x : α) in s, f x * g x ∂μ = f c * ∫ (x : α) in s, g x ∂μ
have _ : ∫ (x : α) in s, f x ∂ν = f c * ∫ (x : α) in s, 1 ∂ν
Tactic: calc
      _ = ∫ x in s, f x ∂ν := heq
      _ = f c * ∫ x in s, (1 : ℝ) ∂ν := by
        rw [h_ave]
        simp only [setAverage_eq, smul_eq_mul, integral_const, MeasurableSet.univ,
          measureReal_restrict_apply, Set.univ_inter, mul_one]
        rw [measureReal_def]
        field_simp
      _ = _ := by simp [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
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 ∂ν
_ : ∫ (x : α) in s, f x ∂ν = f c * ∫ (x : α) in s, 1 ∂ν
⊢ ∫ (x : α) in s, f x * g x ∂μ = f c * ∫ (x : α) in s, g x ∂μ
have _₁ : f c * ∫ (x : α) in s, 1 ∂ν = f c * ∫ (x : α) in s, g x ∂μ
Tactic: calc
      _ = ∫ x in s, f x ∂ν := heq
      _ = f c * ∫ x in s, (1 : ℝ) ∂ν := by
        rw [h_ave]
        simp only [setAverage_eq, smul_eq_mul, integral_const, MeasurableSet.univ,
          measureReal_restrict_apply, Set.univ_inter, mul_one]
        rw [measureReal_def]
        field_simp
      _ = _ := by simp [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 ∈ s, 0 ≤ g x
⊢ ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
have rw : ∀ᵐ (x : α) ∂μ, x ∈ s → 0 ≤ g x
Tactic: rw [ae_restrict_iff' hs_meas]
-- 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 ∈ s, 0 ≤ g x
⊢ ∃ c ∈ s, ∫ (x : α) in s, f x * g x ∂μ = f c * ∫ (x : α) in s, g x ∂μ
have hg0_ae : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
Tactic: have hg0_ae : ∀ᵐ x ∂(μ.restrict s), 0 ≤ g x := by
    rw [ae_restrict_iff' hs_meas]
    exact ae_of_all μ hg0
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.PeakFunction (goal)
Goal:
α : Type u_1
E : Type u_2
ι : Type u_3
hm : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s t : Set α
φ : ι → α → ℝ
a : E
hs : MeasurableSet s
h'st : t ∈ 𝓝[s] x₀
hlφ : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)
hmg : IntegrableOn g s μ
hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)
⊢ ∃ (u : Set α), IsOpen[inst] u ∧ x₀ ∈ u ∧ s ∩ u ⊆ t ∧ ∀ x ∈ u ∩ s, g x ∈ ball a 1
have rcases : ∀ (u : Set α) (u_open : IsOpen[inst] u) (x₀u : x₀ ∈ u) (hu : u ∩ s ⊆ t ∩ g ⁻¹' ball a 1),
  ∃ (u : Set α), IsOpen[inst] u ∧ x₀ ∈ u ∧ s ∩ u ⊆ t ∧ ∀ x ∈ u ∩ s, g x ∈ ball a 1
Tactic: rcases mem_nhdsWithin.1 (Filter.inter_mem h'st (hcg (ball_mem_nhds _ zero_lt_one)))
      with ⟨u, u_open, x₀u, hu⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.PeakFunction (goal)
Goal:
α : Type u_1
E : Type u_2
ι : Type u_3
hm : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s t : Set α
φ : ι → α → ℝ
a : E
hs : MeasurableSet s
h'st : t ∈ 𝓝[s] x₀
hlφ : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)
hmg : IntegrableOn g s μ
hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)
u : Set α
u_open : IsOpen[inst] u
x₀u : x₀ ∈ u
hu : u ∩ s ⊆ t ∩ g ⁻¹' ball a 1
⊢ ∃ (u : Set α), IsOpen[inst] u ∧ x₀ ∈ u ∧ s ∩ u ⊆ t ∧ ∀ x ∈ u ∩ s, g x ∈ ball a 1
have refine : s ∩ u ⊆ t
Tactic: refine ⟨u, u_open, x₀u, ?_, hu.trans inter_subset_right⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.PeakFunction (goal)
Goal:
α : Type u_1
E : Type u_2
ι : Type u_3
hm : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s t : Set α
φ : ι → α → ℝ
a : E
hs : MeasurableSet s
h'st : t ∈ 𝓝[s] x₀
hlφ : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)
hmg : IntegrableOn g s μ
hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)
u : Set α
u_open : IsOpen[inst] u
x₀u : x₀ ∈ u
hu : u ∩ s ⊆ t ∩ g ⁻¹' ball a 1
⊢ s ∩ u ⊆ t
have rw : u ∩ s ⊆ t
Tactic: rw [inter_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.PeakFunction (goal)
Goal:
α : Type u_1
E : Type u_2
ι : Type u_3
hm : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s t : Set α
φ : ι → α → ℝ
a : E
hs : MeasurableSet s
h'st : t ∈ 𝓝[s] x₀
hlφ : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)
hmg : IntegrableOn g s μ
hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)
⊢ ∀ᶠ (i : ι) in l, IntegrableOn.{u_1, u_2} (ε := E) (fun (x : α) ↦ φ i x • g x) s μ
have obtain : ∀ (u : Set α) (u_open : IsOpen[inst] u) (x₀u : x₀ ∈ u) (ut : s ∩ u ⊆ t) (hu : ∀ x ∈ u ∩ s, g x ∈ ball a 1),
  ∀ᶠ (i : ι) in l, IntegrableOn.{u_1, u_2} (ε := E) (fun (x : α) ↦ φ i x • g x) s μ
Tactic: obtain ⟨u, u_open, x₀u, ut, hu⟩ :
      ∃ u, IsOpen u ∧ x₀ ∈ u ∧ s ∩ u ⊆ t ∧ ∀ x ∈ u ∩ s, g x ∈ ball a 1 := by
    rcases mem_nhdsWithin.1 (Filter.inter_mem h'st (hcg (ball_mem_nhds _ zero_lt_one)))
      with ⟨u, u_open, x₀u, hu⟩
    refine ⟨u, u_open, x₀u, ?_, hu.trans inter_subset_right⟩
    rw [inter_comm]
    exact hu.trans inter_subset_left
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.PeakFunction (goal)
Goal:
α : Type u_1
E : Type u_2
ι : Type u_3
hm : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s t : Set α
φ : ι → α → ℝ
a : E
hs : MeasurableSet s
h'st : t ∈ 𝓝[s] x₀
hlφ : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)
hmg : IntegrableOn g s μ
hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)
u : Set α
u_open : IsOpen[inst] u
x₀u : x₀ ∈ u
ut : s ∩ u ⊆ t
hu : ∀ x ∈ u ∩ s, g x ∈ ball a 1
⊢ ∀ᶠ (i : ι) in l, IntegrableOn.{u_1, u_2} (ε := E) (fun (x : α) ↦ φ i x • g x) s μ
have rw : ∀ (hiφ : Tendsto (β := ℝ) (fun (e : ι) ↦ ‖HSub.hSub (α := ℝ) (∫ (x : α) in t, φ e x ∂μ) 1‖) l (𝓝 0))
  (h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)) (hmg : IntegrableOn g s μ)
  (hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)) (u : Set α) (u_open : IsOpen[inst] u) (x₀u : x₀ ∈ u) (ut : s ∩ u ⊆ t)
  (hu : ∀ x ∈ u ∩ s, g x ∈ ball a 1), ∀ᶠ (i : ι) in l, IntegrableOn.{u_1, u_2} (ε := E) (fun (x : α) ↦ φ i x • g x) s μ
Tactic: rw [tendsto_iff_norm_sub_tendsto_zero] at hiφ
Cleared hypotheses: hiφ, h'iφ, hmg, hcg, u, u_open, x₀u, ut, hu
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.PeakFunction (goal)
Goal:
α : Type u_1
E : Type u_2
ι : Type u_3
hm : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s t : Set α
φ : ι → α → ℝ
a : E
hs : MeasurableSet s
h'st : t ∈ 𝓝[s] x₀
hlφ : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : Tendsto (β := ℝ) (fun (e : ι) ↦ ‖HSub.hSub (α := ℝ) (∫ (x : α) in t, φ e x ∂μ) 1‖) l (𝓝 0)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)
hmg : IntegrableOn g s μ
hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)
u : Set α
u_open : IsOpen[inst] u
x₀u : x₀ ∈ u
ut : s ∩ u ⊆ t
hu : ∀ x ∈ u ∩ s, g x ∈ ball a 1
⊢ ∀ᶠ (i : ι) in l, IntegrableOn.{u_1, u_2} (ε := E) (fun (x : α) ↦ φ i x • g x) s μ
have h : ∀ (i : ι) (hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < 1) (h'i : ‖HSub.hSub (α := ℝ) (∫ (x : α) in t, φ i x ∂μ) 1‖ < 1)
  (h''i : AEStronglyMeasurable (φ i) (μ.restrict s)), IntegrableOn.{u_1, u_2} (ε := E) (fun (x : α) ↦ φ i x • g x) s μ
Tactic: filter_upwards [tendstoUniformlyOn_iff.1 (hlφ u u_open x₀u) 1 zero_lt_one,
    (tendsto_order.1 hiφ).2 1 zero_lt_one, h'iφ] with i hi h'i h''i