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'
n : ℕ
x : α
hx : x ∈ s \ u
⊢ t' ^ n * μ.real (v ∩ s) ≤ ∫ (y : α) in s, c y ^ n ∂μ

Tactic:
have B : t' ^ n * μ.real (v ∩ s) ≤ ∫ y in s, c y ^ n ∂μ :=
        calc
          t' ^ n * μ.real (v ∩ s) = ∫ _ in v ∩ s, t' ^ n ∂μ := by simp [mul_comm]
          _ ≤ ∫ y in v ∩ s, c y ^ n ∂μ := by
            apply setIntegral_mono_on _ _ (v_open.measurableSet.inter hs.measurableSet) _
            · refine integrableOn_const (C := t' ^ n) ?_
              exact (lt_of_le_of_lt (measure_mono inter_subset_right) hs.measure_lt_top).ne
            · exact (I n).mono inter_subset_right le_rfl
            · intro x hx
              exact pow_le_pow_left₀ t'_pos.le (hv hx).le _
          _ ≤ ∫ y in s, c y ^ n ∂μ :=
            setIntegral_mono_set (I n) (J n) (Eventually.of_forall inter_subset_right)
-- 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'
n : ℕ
x : α
hx : x ∈ s \ u
B : t' ^ n * μ.real (v ∩ s) ≤ ∫ (y : α) in s, c y ^ n ∂μ
simp_rw : c x ^ n / ∫ (x : α) in s, c x ^ n ∂μ ≤ t ^ n / (t' ^ n * μ.real (v ∩ s))
⊢ φ n x ≤ (μ.real (v ∩ s))⁻¹ * (t / t') ^ n

Tactic:
simp_rw [φ, ← div_eq_inv_mul, div_pow, div_div]

Premises used: div_pow, div_div, div_eq_inv_mul
-- 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'
n : ℕ
x : α
hx : x ∈ s \ u
B : t' ^ n * μ.real (v ∩ s) ≤ ∫ (y : α) in s, c y ^ n ∂μ
⊢ 0 < ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (v ∩ s))

Tactic:
have := ENNReal.toReal_pos (hμ v v_open x₀_v).ne'
        ((measure_mono inter_subset_right).trans_lt hs.measure_lt_top).ne
-- 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'
n : ℕ
x : α
hx : x ∈ s \ u
B : t' ^ n * μ.real (v ∩ s) ≤ ∫ (y : α) in s, c y ^ n ∂μ
this : 0 < ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (v ∩ s))
hac : 0 ≤ c x
hac₁ : c x ≤ t
⊢ c x ^ n / ∫ (x : α) in s, c x ^ n ∂μ ≤ t ^ n / (t' ^ n * μ.real (v ∩ s))

Tactic:
gcongr
-- 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'
n : ℕ
x : α
hx : x ∈ s \ u
B : t' ^ n * μ.real (v ∩ s) ≤ ∫ (y : α) in s, c y ^ n ∂μ
this : 0 < ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (v ∩ s))
⊢ 0 ≤ c x

Tactic:
hnc _ hx.1

Premises used: And.left
-- 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'
n : ℕ
x : α
hx : x ∈ s \ u
B : t' ^ n * μ.real (v ∩ s) ≤ ∫ (y : α) in s, c y ^ n ∂μ
this : 0 < ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (v ∩ s))
⊢ 0 ≤ c x

Tactic:
exact hnc _ hx.1

Premises used: And.left
-- 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'
n : ℕ
x : α
hx : x ∈ s \ u
B : t' ^ n * μ.real (v ∩ s) ≤ ∫ (y : α) in s, c y ^ n ∂μ
this : 0 < ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (v ∩ s))
⊢ c x ≤ t

Tactic:
ht x hx
-- 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'
n : ℕ
x : α
hx : x ∈ s \ u
B : t' ^ n * μ.real (v ∩ s) ≤ ∫ (y : α) in s, c y ^ n ∂μ
this : 0 < ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (v ∩ s))
⊢ c x ≤ t

Tactic:
exact ht x hx
-- 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'
⊢ ∀ (n : ℕ), ∀ x ∈ s \ u, φ n x ≤ (μ.real (v ∩ s))⁻¹ * (t / t') ^ n

Tactic:
have M : ∀ n, ∀ x ∈ s \ u, φ n x ≤ (μ.real (v ∩ s))⁻¹ * (t / t') ^ n := by
      intro n x hx
      have B : t' ^ n * μ.real (v ∩ s) ≤ ∫ y in s, c y ^ n ∂μ :=
        calc
          t' ^ n * μ.real (v ∩ s) = ∫ _ in v ∩ s, t' ^ n ∂μ := by simp [mul_comm]
          _ ≤ ∫ y in v ∩ s, c y ^ n ∂μ := by
            apply setIntegral_mono_on _ _ (v_open.measurableSet.inter hs.measurableSet) _
            · refine integrableOn_const (C := t' ^ n) ?_
              exact (lt_of_le_of_lt (measure_mono inter_subset_right) hs.measure_lt_top).ne
            · exact (I n).mono inter_subset_right le_rfl
            · intro x hx
              exact pow_le_pow_left₀ t'_pos.le (hv hx).le _
          _ ≤ ∫ y in s, c y ^ n ∂μ :=
            setIntegral_mono_set (I n) (J n) (Eventually.of_forall inter_subset_right)
      simp_rw [φ, ← div_eq_inv_mul, div_pow, div_div]
      have := ENNReal.toReal_pos (hμ v v_open x₀_v).ne'
        ((measure_mono inter_subset_right).trans_lt hs.measure_lt_top).ne
      gcongr
      · exact hnc _ hx.1
      · exact ht x hx
-- 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
apply : Tendsto (α := ℕ) (HPow.hPow (t / t')) atTop (𝓝 0)
⊢ Tendsto (fun (n : ℕ) ↦ (μ.real (v ∩ s))⁻¹ * (t / t') ^ n) atTop (𝓝 ((μ.real (v ∩ s))⁻¹ * 0))

Tactic:
apply Tendsto.mul tendsto_const_nhds _

Premises used: tendsto_const_nhds, Filter.Tendsto.mul
-- 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
apply : t / t' < 1
⊢ Tendsto (α := ℕ) (HPow.hPow (t / t')) atTop (𝓝 0)

Tactic:
apply tendsto_pow_atTop_nhds_zero_of_lt_one (div_nonneg t_pos t'_pos.le)

Premises used: LT.lt.le, tendsto_pow_atTop_nhds_zero_of_lt_one, div_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
⊢ t / t' < 1

Tactic:
(div_lt_one t'_pos).2 tt'

Premises used: Iff.mpr, div_lt_one
-- 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
⊢ t / t' < 1

Tactic:
exact (div_lt_one t'_pos).2 tt'

Premises used: Iff.mpr, div_lt_one
-- 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
⊢ Tendsto (fun (n : ℕ) ↦ (μ.real (v ∩ s))⁻¹ * (t / t') ^ n) atTop (𝓝 ((μ.real (v ∩ s))⁻¹ * 0))

Tactic:
have N :
      Tendsto (fun n => (μ.real (v ∩ s))⁻¹ * (t / t') ^ n) atTop
        (𝓝 ((μ.real (v ∩ s))⁻¹ * 0)) := by
      apply Tendsto.mul tendsto_const_nhds _
      apply tendsto_pow_atTop_nhds_zero_of_lt_one (div_nonneg t_pos t'_pos.le)
      exact (div_lt_one t'_pos).2 tt'
-- 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 (𝓝 ((μ.real (v ∩ s))⁻¹ * 0))
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ (μ.real (v ∩ s))⁻¹ * (t / t') ^ n) atTop (𝓝 0)

Tactic:
rw [mul_zero] at N

Premises used: MulZeroClass.mul_zero