awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
α : Type u_1
E : Type u_2
hm : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
g : α → E
x₀ : α
s : Set α
inst_4 : CompleteSpace E
inst_5 : MetrizableSpace α
inst_6 : IsLocallyFiniteMeasure μ
hs : IsCompact s
hμ : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
c : α → ℝ
hc : ContinuousOn c s
h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀
hnc : ∀ x ∈ s, 0 ≤ c x
hnc₀ : 0 < c x₀
h₀ : x₀ ∈ s
hmg : IntegrableOn g s μ
hcg : ContinuousWithinAt g s x₀
φ : ℕ → α → ℝ := fun (n : ℕ) (x : α) ↦ (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ * c x ^ n
hnφ : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ φ n x
I : ∀ (n : ℕ), IntegrableOn (ε := ℝ) (fun (x : α) ↦ c x ^ n) s μ
J : ∀ (n : ℕ), (ae (μ.restrict s)).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ c x ^ n
P : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (∫ (x : α) in s, c x ^ n ∂μ)
hiφ : ∀ (n : ℕ), Eq (α := ℝ) (∫ (x : α) in s, φ n x ∂μ) 1
u : Set α
u_open : IsOpen[inst] u
x₀u : x₀ ∈ u
t : ℝ
t_pos : 0 ≤ t
tx₀ : t < c x₀
ht : ∀ x ∈ s \ u, c x ≤ t
t' : ℝ
tt' : t < t'
t'x₀ : t' < c x₀
t'_pos : 0 < t'
v : Set α
v_open : IsOpen[inst] v
x₀_v : x₀ ∈ v
hv : v ∩ s ⊆ c ⁻¹' Ioi t'
M : ∀ (n : ℕ), ∀ x ∈ s \ u, φ n x ≤ (μ.real (v ∩ s))⁻¹ * (t / t') ^ n
N : Tendsto (β := ℝ) (fun (n : ℕ) ↦ (μ.real (v ∩ s))⁻¹ * (t / t') ^ n) atTop (𝓝 0)
⊢ TendstoUniformlyOn φ 0 atTop (s \ u)

Tactic:
tendstoUniformlyOn_iff.2 fun ε εpos => ?_

Premises used: Iff.mpr, Metric.tendstoUniformlyOn_iff
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
α : Type u_1
E : Type u_2
hm : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
g : α → E
x₀ : α
s : Set α
inst_4 : CompleteSpace E
inst_5 : MetrizableSpace α
inst_6 : IsLocallyFiniteMeasure μ
hs : IsCompact s
hμ : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
c : α → ℝ
hc : ContinuousOn c s
h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀
hnc : ∀ x ∈ s, 0 ≤ c x
hnc₀ : 0 < c x₀
h₀ : x₀ ∈ s
hmg : IntegrableOn g s μ
hcg : ContinuousWithinAt g s x₀
φ : ℕ → α → ℝ := fun (n : ℕ) (x : α) ↦ (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ * c x ^ n
hnφ : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ φ n x
I : ∀ (n : ℕ), IntegrableOn (ε := ℝ) (fun (x : α) ↦ c x ^ n) s μ
J : ∀ (n : ℕ), (ae (μ.restrict s)).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ c x ^ n
P : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (∫ (x : α) in s, c x ^ n ∂μ)
hiφ : ∀ (n : ℕ), Eq (α := ℝ) (∫ (x : α) in s, φ n x ∂μ) 1
u : Set α
u_open : IsOpen[inst] u
x₀u : x₀ ∈ u
t : ℝ
t_pos : 0 ≤ t
tx₀ : t < c x₀
ht : ∀ x ∈ s \ u, c x ≤ t
t' : ℝ
tt' : t < t'
t'x₀ : t' < c x₀
t'_pos : 0 < t'
v : Set α
v_open : IsOpen[inst] v
x₀_v : x₀ ∈ v
hv : v ∩ s ⊆ c ⁻¹' Ioi t'
M : ∀ (n : ℕ), ∀ x ∈ s \ u, φ n x ≤ (μ.real (v ∩ s))⁻¹ * (t / t') ^ n
N : Tendsto (β := ℝ) (fun (n : ℕ) ↦ (μ.real (v ∩ s))⁻¹ * (t / t') ^ n) atTop (𝓝 0)
refine : ∀ (ε : ℝ) (εpos : ε > 0), ∀ᶠ (n : ℕ) in atTop, ∀ x ∈ s \ u, dist (0 x) (φ n x) < ε
⊢ TendstoUniformlyOn φ 0 atTop (s \ u)

Tactic:
refine tendstoUniformlyOn_iff.2 fun ε εpos => ?_

Premises used: Iff.mpr, Metric.tendstoUniformlyOn_iff
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
α : Type u_1
E : Type u_2
hm : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
g : α → E
x₀ : α
s : Set α
inst_4 : CompleteSpace E
inst_5 : MetrizableSpace α
inst_6 : IsLocallyFiniteMeasure μ
hs : IsCompact s
hμ : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
c : α → ℝ
hc : ContinuousOn c s
h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀
hnc : ∀ x ∈ s, 0 ≤ c x
hnc₀ : 0 < c x₀
h₀ : x₀ ∈ s
hmg : IntegrableOn g s μ
hcg : ContinuousWithinAt g s x₀
φ : ℕ → α → ℝ := fun (n : ℕ) (x : α) ↦ (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ * c x ^ n
hnφ : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ φ n x
I : ∀ (n : ℕ), IntegrableOn (ε := ℝ) (fun (x : α) ↦ c x ^ n) s μ
J : ∀ (n : ℕ), (ae (μ.restrict s)).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ c x ^ n
P : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (∫ (x : α) in s, c x ^ n ∂μ)
hiφ : ∀ (n : ℕ), Eq (α := ℝ) (∫ (x : α) in s, φ n x ∂μ) 1
u : Set α
u_open : IsOpen[inst] u
x₀u : x₀ ∈ u
t : ℝ
t_pos : 0 ≤ t
tx₀ : t < c x₀
ht : ∀ x ∈ s \ u, c x ≤ t
t' : ℝ
tt' : t < t'
t'x₀ : t' < c x₀
t'_pos : 0 < t'
v : Set α
v_open : IsOpen[inst] v
x₀_v : x₀ ∈ v
hv : v ∩ s ⊆ c ⁻¹' Ioi t'
M : ∀ (n : ℕ), ∀ x ∈ s \ u, φ n x ≤ (μ.real (v ∩ s))⁻¹ * (t / t') ^ n
N : Tendsto (β := ℝ) (fun (n : ℕ) ↦ (μ.real (v ∩ s))⁻¹ * (t / t') ^ n) atTop (𝓝 0)
ε : ℝ
εpos : ε > 0
h : ∀ (n : ℕ) (hn : (μ.real (v ∩ s))⁻¹ * (t / t') ^ n < ε) (x : α) (hx : x ∈ s \ u), dist (0 x) (φ n x) < ε
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ x ∈ s \ u, dist (0 x) (φ n x) < ε

Tactic:
filter_upwards [(tendsto_order.1 N).2 ε εpos] with n hn x hx

Premises used: tendsto_order, And.right, Iff.mp
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
α : Type u_1
E : Type u_2
hm : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
g : α → E
x₀ : α
s : Set α
inst_4 : CompleteSpace E
inst_5 : MetrizableSpace α
inst_6 : IsLocallyFiniteMeasure μ
hs : IsCompact s
hμ : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
c : α → ℝ
hc : ContinuousOn c s
h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀
hnc : ∀ x ∈ s, 0 ≤ c x
hnc₀ : 0 < c x₀
h₀ : x₀ ∈ s
hmg : IntegrableOn g s μ
hcg : ContinuousWithinAt g s x₀
φ : ℕ → α → ℝ := fun (n : ℕ) (x : α) ↦ (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ * c x ^ n
hnφ : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ φ n x
I : ∀ (n : ℕ), IntegrableOn (ε := ℝ) (fun (x : α) ↦ c x ^ n) s μ
J : ∀ (n : ℕ), (ae (μ.restrict s)).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ c x ^ n
P : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (∫ (x : α) in s, c x ^ n ∂μ)
hiφ : ∀ (n : ℕ), Eq (α := ℝ) (∫ (x : α) in s, φ n x ∂μ) 1
u : Set α
u_open : IsOpen[inst] u
x₀u : x₀ ∈ u
t : ℝ
t_pos : 0 ≤ t
tx₀ : t < c x₀
ht : ∀ x ∈ s \ u, c x ≤ t
t' : ℝ
tt' : t < t'
t'x₀ : t' < c x₀
t'_pos : 0 < t'
v : Set α
v_open : IsOpen[inst] v
x₀_v : x₀ ∈ v
hv : v ∩ s ⊆ c ⁻¹' Ioi t'
M : ∀ (n : ℕ), ∀ x ∈ s \ u, φ n x ≤ (μ.real (v ∩ s))⁻¹ * (t / t') ^ n
N : Tendsto (β := ℝ) (fun (n : ℕ) ↦ (μ.real (v ∩ s))⁻¹ * (t / t') ^ n) atTop (𝓝 0)
ε : ℝ
εpos : ε > 0
n : ℕ
hn : (μ.real (v ∩ s))⁻¹ * (t / t') ^ n < ε
x : α
hx : x ∈ s \ u
h : φ n x < ε
⊢ dist (0 x) (φ n x) < ε

Tactic:
simp only [Pi.zero_apply, dist_zero_left, Real.norm_of_nonneg (hnφ n x hx.1)]

Premises used: Pi.zero_apply, dist_zero_left, And.left, Real.norm_of_nonneg
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
α : Type u_1
E : Type u_2
hm : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
g : α → E
x₀ : α
s : Set α
inst_4 : CompleteSpace E
inst_5 : MetrizableSpace α
inst_6 : IsLocallyFiniteMeasure μ
hs : IsCompact s
hμ : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
c : α → ℝ
hc : ContinuousOn c s
h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀
hnc : ∀ x ∈ s, 0 ≤ c x
hnc₀ : 0 < c x₀
h₀ : x₀ ∈ s
hmg : IntegrableOn g s μ
hcg : ContinuousWithinAt g s x₀
φ : ℕ → α → ℝ := fun (n : ℕ) (x : α) ↦ (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ * c x ^ n
hnφ : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ φ n x
I : ∀ (n : ℕ), IntegrableOn (ε := ℝ) (fun (x : α) ↦ c x ^ n) s μ
J : ∀ (n : ℕ), (ae (μ.restrict s)).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ c x ^ n
P : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (∫ (x : α) in s, c x ^ n ∂μ)
hiφ : ∀ (n : ℕ), Eq (α := ℝ) (∫ (x : α) in s, φ n x ∂μ) 1
u : Set α
u_open : IsOpen[inst] u
x₀u : x₀ ∈ u
t : ℝ
t_pos : 0 ≤ t
tx₀ : t < c x₀
ht : ∀ x ∈ s \ u, c x ≤ t
t' : ℝ
tt' : t < t'
t'x₀ : t' < c x₀
t'_pos : 0 < t'
v : Set α
v_open : IsOpen[inst] v
x₀_v : x₀ ∈ v
hv : v ∩ s ⊆ c ⁻¹' Ioi t'
M : ∀ (n : ℕ), ∀ x ∈ s \ u, φ n x ≤ (μ.real (v ∩ s))⁻¹ * (t / t') ^ n
N : Tendsto (β := ℝ) (fun (n : ℕ) ↦ (μ.real (v ∩ s))⁻¹ * (t / t') ^ n) atTop (𝓝 0)
ε : ℝ
εpos : ε > 0
n : ℕ
hn : (μ.real (v ∩ s))⁻¹ * (t / t') ^ n < ε
x : α
hx : x ∈ s \ u
⊢ φ n x < ε

Tactic:
(M n x hx).trans_lt hn

Premises used: LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
α : Type u_1
E : Type u_2
hm : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
g : α → E
x₀ : α
s : Set α
inst_4 : CompleteSpace E
inst_5 : MetrizableSpace α
inst_6 : IsLocallyFiniteMeasure μ
hs : IsCompact s
hμ : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
c : α → ℝ
hc : ContinuousOn c s
h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀
hnc : ∀ x ∈ s, 0 ≤ c x
hnc₀ : 0 < c x₀
h₀ : x₀ ∈ s
hmg : IntegrableOn g s μ
hcg : ContinuousWithinAt g s x₀
φ : ℕ → α → ℝ := fun (n : ℕ) (x : α) ↦ (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ * c x ^ n
hnφ : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ φ n x
I : ∀ (n : ℕ), IntegrableOn (ε := ℝ) (fun (x : α) ↦ c x ^ n) s μ
J : ∀ (n : ℕ), (ae (μ.restrict s)).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ c x ^ n
P : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (∫ (x : α) in s, c x ^ n ∂μ)
hiφ : ∀ (n : ℕ), Eq (α := ℝ) (∫ (x : α) in s, φ n x ∂μ) 1
u : Set α
u_open : IsOpen[inst] u
x₀u : x₀ ∈ u
t : ℝ
t_pos : 0 ≤ t
tx₀ : t < c x₀
ht : ∀ x ∈ s \ u, c x ≤ t
t' : ℝ
tt' : t < t'
t'x₀ : t' < c x₀
t'_pos : 0 < t'
v : Set α
v_open : IsOpen[inst] v
x₀_v : x₀ ∈ v
hv : v ∩ s ⊆ c ⁻¹' Ioi t'
M : ∀ (n : ℕ), ∀ x ∈ s \ u, φ n x ≤ (μ.real (v ∩ s))⁻¹ * (t / t') ^ n
N : Tendsto (β := ℝ) (fun (n : ℕ) ↦ (μ.real (v ∩ s))⁻¹ * (t / t') ^ n) atTop (𝓝 0)
ε : ℝ
εpos : ε > 0
n : ℕ
hn : (μ.real (v ∩ s))⁻¹ * (t / t') ^ n < ε
x : α
hx : x ∈ s \ u
⊢ φ n x < ε

Tactic:
exact (M n x hx).trans_lt hn

Premises used: LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
α : Type u_1
E : Type u_2
hm : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
g : α → E
x₀ : α
s : Set α
inst_4 : CompleteSpace E
inst_5 : MetrizableSpace α
inst_6 : IsLocallyFiniteMeasure μ
hs : IsCompact s
hμ : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
c : α → ℝ
hc : ContinuousOn c s
h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀
hnc : ∀ x ∈ s, 0 ≤ c x
hnc₀ : 0 < c x₀
h₀ : x₀ ∈ s
hmg : IntegrableOn g s μ
hcg : ContinuousWithinAt g s x₀
φ : ℕ → α → ℝ := fun (n : ℕ) (x : α) ↦ (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ * c x ^ n
hnφ : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ φ n x
I : ∀ (n : ℕ), IntegrableOn (ε := ℝ) (fun (x : α) ↦ c x ^ n) s μ
J : ∀ (n : ℕ), (ae (μ.restrict s)).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ c x ^ n
P : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (∫ (x : α) in s, c x ^ n ∂μ)
hiφ : ∀ (n : ℕ), Eq (α := ℝ) (∫ (x : α) in s, φ n x ∂μ) 1
A : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → TendstoUniformlyOn φ 0 atTop (s \ u)
⊢ Tendsto (β := ℝ) (fun (i : ℕ) ↦ ∫ (x : α) in s, φ i x ∂μ) atTop (𝓝 1)

Tactic:
have B : Tendsto (fun i ↦ ∫ (x : α) in s, φ i x ∂μ) atTop (𝓝 1) :=
      tendsto_const_nhds.congr (fun n ↦ (hiφ n).symm)
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
α : Type u_1
E : Type u_2
hm : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
g : α → E
x₀ : α
s : Set α
inst_4 : CompleteSpace E
inst_5 : MetrizableSpace α
inst_6 : IsLocallyFiniteMeasure μ
hs : IsCompact s
hμ : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
c : α → ℝ
hc : ContinuousOn c s
h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀
hnc : ∀ x ∈ s, 0 ≤ c x
hnc₀ : 0 < c x₀
h₀ : x₀ ∈ s
hmg : IntegrableOn g s μ
hcg : ContinuousWithinAt g s x₀
φ : ℕ → α → ℝ := fun (n : ℕ) (x : α) ↦ (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ * c x ^ n
hnφ : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ φ n x
I : ∀ (n : ℕ), IntegrableOn (ε := ℝ) (fun (x : α) ↦ c x ^ n) s μ
J : ∀ (n : ℕ), (ae (μ.restrict s)).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ c x ^ n
P : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (∫ (x : α) in s, c x ^ n ∂μ)
hiφ : ∀ (n : ℕ), Eq (α := ℝ) (∫ (x : α) in s, φ n x ∂μ) 1
A : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → TendstoUniformlyOn φ 0 atTop (s \ u)
B : Tendsto (β := ℝ) (fun (i : ℕ) ↦ ∫ (x : α) in s, φ i x ∂μ) atTop (𝓝 1)
⊢ ∀ᶠ (i : ℕ) in atTop, AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ φ i x) (μ.restrict s)

Tactic:
apply Eventually.of_forall (fun n ↦ ((I n).const_mul _).aestronglyMeasurable)

Premises used: MeasureTheory.Integrable.aestronglyMeasurable, MeasureTheory.Integrable.const_mul, Filter.Eventually.of_forall
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
α : Type u_1
E : Type u_2
hm : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
g : α → E
x₀ : α
s : Set α
inst_4 : CompleteSpace E
inst_5 : MetrizableSpace α
inst_6 : IsLocallyFiniteMeasure μ
hs : IsCompact s
hμ : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
c : α → ℝ
hc : ContinuousOn c s
h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀
hnc : ∀ x ∈ s, 0 ≤ c x
hnc₀ : 0 < c x₀
h₀ : x₀ ∈ s
hmg : IntegrableOn g s μ
hcg : ContinuousWithinAt g s x₀
φ : ℕ → α → ℝ := fun (n : ℕ) (x : α) ↦ (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ * c x ^ n
hnφ : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ φ n x
I : ∀ (n : ℕ), IntegrableOn (ε := ℝ) (fun (x : α) ↦ c x ^ n) s μ
J : ∀ (n : ℕ), (ae (μ.restrict s)).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ c x ^ n
P : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (∫ (x : α) in s, c x ^ n ∂μ)
hiφ : ∀ (n : ℕ), Eq (α := ℝ) (∫ (x : α) in s, φ n x ∂μ) 1
A : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → TendstoUniformlyOn φ 0 atTop (s \ u)
B : Tendsto (β := ℝ) (fun (i : ℕ) ↦ ∫ (x : α) in s, φ i x ∂μ) atTop (𝓝 1)
⊢ ∀ᶠ (i : ℕ) in atTop, AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ φ i x) (μ.restrict s)

Tactic:
have C : ∀ᶠ (i : ℕ) in atTop, AEStronglyMeasurable (fun x ↦ φ i x) (μ.restrict s) := by
      apply Eventually.of_forall (fun n ↦ ((I n).const_mul _).aestronglyMeasurable)
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
α : Type u_1
E : Type u_2
hm : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
g : α → E
x₀ : α
s : Set α
inst_4 : CompleteSpace E
inst_5 : MetrizableSpace α
inst_6 : IsLocallyFiniteMeasure μ
hs : IsCompact s
hμ : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
c : α → ℝ
hc : ContinuousOn c s
h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀
hnc : ∀ x ∈ s, 0 ≤ c x
hnc₀ : 0 < c x₀
h₀ : x₀ ∈ s
hmg : IntegrableOn g s μ
hcg : ContinuousWithinAt g s x₀
φ : ℕ → α → ℝ := fun (n : ℕ) (x : α) ↦ (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ * c x ^ n
hnφ : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ φ n x
I : ∀ (n : ℕ), IntegrableOn (ε := ℝ) (fun (x : α) ↦ c x ^ n) s μ
J : ∀ (n : ℕ), (ae (μ.restrict s)).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ c x ^ n
P : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (∫ (x : α) in s, c x ^ n ∂μ)
hiφ : ∀ (n : ℕ), Eq (α := ℝ) (∫ (x : α) in s, φ n x ∂μ) 1
A : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → TendstoUniformlyOn φ 0 atTop (s \ u)
B : Tendsto (β := ℝ) (fun (i : ℕ) ↦ ∫ (x : α) in s, φ i x ∂μ) atTop (𝓝 1)
C : ∀ᶠ (i : ℕ) in atTop, AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ φ i x) (μ.restrict s)
⊢ Tendsto (fun (i : ℕ) ↦ ∫ (x : α) in s, φ i x • g x ∂μ) atTop (𝓝 (g x₀))

Tactic:
tendsto_setIntegral_peak_smul_of_integrableOn_of_tendsto hs.measurableSet
      hs.measurableSet (Subset.rfl) (self_mem_nhdsWithin)
      hs.measure_lt_top.ne (Eventually.of_forall hnφ) A B C hmg hcg

Premises used: tendsto_setIntegral_peak_smul_of_integrableOn_of_tendsto, Filter.Eventually.of_forall, Set.Subset.rfl, self_mem_nhdsWithin, IsCompact.measure_lt_top, LT.lt.ne, IsCompact.measurableSet
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
α : Type u_1
E : Type u_2
hm : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
g : α → E
x₀ : α
s : Set α
inst_4 : CompleteSpace E
inst_5 : MetrizableSpace α
inst_6 : IsLocallyFiniteMeasure μ
hs : IsCompact s
hμ : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
c : α → ℝ
hc : ContinuousOn c s
h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀
hnc : ∀ x ∈ s, 0 ≤ c x
hnc₀ : 0 < c x₀
h₀ : x₀ ∈ s
hmg : IntegrableOn g s μ
hcg : ContinuousWithinAt g s x₀
φ : ℕ → α → ℝ := fun (n : ℕ) (x : α) ↦ (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ * c x ^ n
hnφ : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ φ n x
I : ∀ (n : ℕ), IntegrableOn (ε := ℝ) (fun (x : α) ↦ c x ^ n) s μ
J : ∀ (n : ℕ), (ae (μ.restrict s)).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ c x ^ n
P : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (∫ (x : α) in s, c x ^ n ∂μ)
hiφ : ∀ (n : ℕ), Eq (α := ℝ) (∫ (x : α) in s, φ n x ∂μ) 1
A : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → TendstoUniformlyOn φ 0 atTop (s \ u)
B : Tendsto (β := ℝ) (fun (i : ℕ) ↦ ∫ (x : α) in s, φ i x ∂μ) atTop (𝓝 1)
C : ∀ᶠ (i : ℕ) in atTop, AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ φ i x) (μ.restrict s)
⊢ Tendsto (fun (i : ℕ) ↦ ∫ (x : α) in s, φ i x • g x ∂μ) atTop (𝓝 (g x₀))

Tactic:
exact tendsto_setIntegral_peak_smul_of_integrableOn_of_tendsto hs.measurableSet
      hs.measurableSet (Subset.rfl) (self_mem_nhdsWithin)
      hs.measure_lt_top.ne (Eventually.of_forall hnφ) A B C hmg hcg

Premises used: tendsto_setIntegral_peak_smul_of_integrableOn_of_tendsto, Filter.Eventually.of_forall, Set.Subset.rfl, self_mem_nhdsWithin, IsCompact.measure_lt_top, LT.lt.ne, IsCompact.measurableSet
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
α : Type u_1
E : Type u_2
hm : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
g : α → E
x₀ : α
s : Set α
inst_4 : CompleteSpace E
inst_5 : MetrizableSpace α
inst_6 : IsLocallyFiniteMeasure μ
hs : IsCompact s
hμ : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
c : α → ℝ
hc : ContinuousOn c s
h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀
hnc : ∀ x ∈ s, 0 ≤ c x
hnc₀ : 0 < c x₀
h₀ : x₀ ∈ s
hmg : IntegrableOn g s μ
hcg : ContinuousWithinAt g s x₀
φ : ℕ → α → ℝ := fun (n : ℕ) (x : α) ↦ (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ * c x ^ n
hnφ : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ φ n x
I : ∀ (n : ℕ), IntegrableOn (ε := ℝ) (fun (x : α) ↦ c x ^ n) s μ
J : ∀ (n : ℕ), (ae (μ.restrict s)).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ c x ^ n
P : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (∫ (x : α) in s, c x ^ n ∂μ)
hiφ : ∀ (n : ℕ), Eq (α := ℝ) (∫ (x : α) in s, φ n x ∂μ) 1
A : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → TendstoUniformlyOn φ 0 atTop (s \ u)
⊢ Tendsto (fun (i : ℕ) ↦ ∫ (x : α) in s, φ i x • g x ∂μ) atTop (𝓝 (g x₀))

Tactic:
have : Tendsto (fun i : ℕ => ∫ x : α in s, φ i x • g x ∂μ) atTop (𝓝 (g x₀)) := by
    have B : Tendsto (fun i ↦ ∫ (x : α) in s, φ i x ∂μ) atTop (𝓝 1) :=
      tendsto_const_nhds.congr (fun n ↦ (hiφ n).symm)
    have C : ∀ᶠ (i : ℕ) in atTop, AEStronglyMeasurable (fun x ↦ φ i x) (μ.restrict s) := by
      apply Eventually.of_forall (fun n ↦ ((I n).const_mul _).aestronglyMeasurable)
    exact tendsto_setIntegral_peak_smul_of_integrableOn_of_tendsto hs.measurableSet
      hs.measurableSet (Subset.rfl) (self_mem_nhdsWithin)
      hs.measure_lt_top.ne (Eventually.of_forall hnφ) A B C hmg hcg
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
α : Type u_1
E : Type u_2
hm : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
g : α → E
x₀ : α
s : Set α
inst_4 : CompleteSpace E
inst_5 : MetrizableSpace α
inst_6 : IsLocallyFiniteMeasure μ
hs : IsCompact s
hμ : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
c : α → ℝ
hc : ContinuousOn c s
h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀
hnc : ∀ x ∈ s, 0 ≤ c x
hnc₀ : 0 < c x₀
h₀ : x₀ ∈ s
hmg : IntegrableOn g s μ
hcg : ContinuousWithinAt g s x₀
φ : ℕ → α → ℝ := fun (n : ℕ) (x : α) ↦ (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ * c x ^ n
hnφ : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ φ n x
I : ∀ (n : ℕ), IntegrableOn (ε := ℝ) (fun (x : α) ↦ c x ^ n) s μ
J : ∀ (n : ℕ), (ae (μ.restrict s)).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ c x ^ n
P : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (∫ (x : α) in s, c x ^ n ∂μ)
hiφ : ∀ (n : ℕ), Eq (α := ℝ) (∫ (x : α) in s, φ n x ∂μ) 1
A : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → TendstoUniformlyOn φ 0 atTop (s \ u)
this : Tendsto (fun (i : ℕ) ↦ ∫ (x : α) in s, φ i x • g x ∂μ) atTop (𝓝 (g x₀))
⊢ Tendsto (fun (i : ℕ) ↦ ∫ (x : α) in s, φ i x • g x ∂μ) atTop (𝓝 (g x₀))

Tactic:
this
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
α : Type u_1
E : Type u_2
hm : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
g : α → E
x₀ : α
s : Set α
inst_4 : CompleteSpace E
inst_5 : MetrizableSpace α
inst_6 : IsLocallyFiniteMeasure μ
hs : IsCompact s
hμ : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
c : α → ℝ
hc : ContinuousOn c s
h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀
hnc : ∀ x ∈ s, 0 ≤ c x
hnc₀ : 0 < c x₀
h₀ : x₀ ∈ s
hmg : IntegrableOn g s μ
hcg : ContinuousWithinAt g s x₀
φ : ℕ → α → ℝ := fun (n : ℕ) (x : α) ↦ (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ * c x ^ n
hnφ : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ φ n x
I : ∀ (n : ℕ), IntegrableOn (ε := ℝ) (fun (x : α) ↦ c x ^ n) s μ
J : ∀ (n : ℕ), (ae (μ.restrict s)).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ c x ^ n
P : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (∫ (x : α) in s, c x ^ n ∂μ)
hiφ : ∀ (n : ℕ), Eq (α := ℝ) (∫ (x : α) in s, φ n x ∂μ) 1
A : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → TendstoUniformlyOn φ 0 atTop (s \ u)
this : Tendsto (fun (i : ℕ) ↦ ∫ (x : α) in s, φ i x • g x ∂μ) atTop (𝓝 (g x₀))
h :
  ∀ (x : ℕ),
    HSMul.hSMul (α := ℝ) (β := E) (∫ (x_1 : α) in s, c x_1 ^ x ∂μ)⁻¹ (∫ (x_1 : α) in s, c x_1 ^ x • g x_1 ∂μ) =
      ∫ (x_1 : α) in s, φ x x_1 • g x_1 ∂μ
⊢ Tendsto
    (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ (∫ (x : α) in s, c x ^ n • g x ∂μ))
    atTop (𝓝 (g x₀))

Tactic:
convert! this
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
α : Type u_1
E : Type u_2
hm : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
g : α → E
x₀ : α
s : Set α
inst_4 : CompleteSpace E
inst_5 : MetrizableSpace α
inst_6 : IsLocallyFiniteMeasure μ
hs : IsCompact s
hμ : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
c : α → ℝ
hc : ContinuousOn c s
h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀
hnc : ∀ x ∈ s, 0 ≤ c x
hnc₀ : 0 < c x₀
h₀ : x₀ ∈ s
hmg : IntegrableOn g s μ
hcg : ContinuousWithinAt g s x₀
φ : ℕ → α → ℝ := fun (n : ℕ) (x : α) ↦ (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ * c x ^ n
hnφ : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ φ n x
I : ∀ (n : ℕ), IntegrableOn (ε := ℝ) (fun (x : α) ↦ c x ^ n) s μ
J : ∀ (n : ℕ), (ae (μ.restrict s)).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ c x ^ n
P : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (∫ (x : α) in s, c x ^ n ∂μ)
hiφ : ∀ (n : ℕ), Eq (α := ℝ) (∫ (x : α) in s, φ n x ∂μ) 1
A : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → TendstoUniformlyOn φ 0 atTop (s \ u)
this : Tendsto (fun (i : ℕ) ↦ ∫ (x : α) in s, φ i x • g x ∂μ) atTop (𝓝 (g x₀))
x : ℕ
h :
  HSMul.hSMul (α := ℝ) (β := E) (∫ (x_1 : α) in s, c x_1 ^ x ∂μ)⁻¹ (∫ (x_1 : α) in s, c x_1 ^ x • g x_1 ∂μ) =
    ∫ (x_1 : α) in s, ((∫ (x_2 : α) in s, c x_2 ^ x ∂μ)⁻¹ * c x_1 ^ x) • g x_1 ∂μ
h₁ :
  HSMul.hSMul (α := ℝ) (β := E) (∫ (x_1 : α) in s, c x_1 ^ x ∂μ)⁻¹ (∫ (x_1 : α) in s, c x_1 ^ x • g x_1 ∂μ) =
    ∫ (x_1 : α) in s, HSMul.hSMul (α := ℝ) (∫ (x_2 : α) in s, c x_2 ^ x ∂μ)⁻¹ (c x_1 ^ x • g x_1) ∂μ
⊢ HSMul.hSMul (α := ℝ) (β := E) (∫ (x_1 : α) in s, c x_1 ^ x ∂μ)⁻¹ (∫ (x_1 : α) in s, c x_1 ^ x • g x_1 ∂μ) =
    ∫ (x_1 : α) in s, φ x x_1 • g x_1 ∂μ

Tactic:
simp_rw [φ, ← smul_smul, integral_smul]

Premises used: MeasureTheory.integral_smul, smul_smul