awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
u : Set F
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hu : 0 ∈ u
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
h'u : ball 0 δ ⊆ u
M : ℝ
Mpos : M > 0
hM : ∀ ⦃x : F⦄, Membership.mem (γ := Set F) (closedBall 0 M)ᶜ x → ‖x‖ ^ finrank ℝ F * φ x < δ ^ finrank ℝ F * ε
c : ℝ
hc : M / δ < c
x : F
hx : x ∈ uᶜ
cpos : 0 < c
hδx : δ ≤ ‖x‖
a : Membership.mem (γ := Set F) (closedBall 0 M)ᶜ (c • x)
⊢ ‖c • x‖ ^ finrank ℝ F * φ (c • x) < δ ^ finrank ℝ F * ε

Tactic:
apply hM
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
u : Set F
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hu : 0 ∈ u
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
h'u : ball 0 δ ⊆ u
M : ℝ
Mpos : M > 0
hM : ∀ ⦃x : F⦄, Membership.mem (γ := Set F) (closedBall 0 M)ᶜ x → ‖x‖ ^ finrank ℝ F * φ x < δ ^ finrank ℝ F * ε
c : ℝ
hc : M / δ < c
x : F
hx : x ∈ uᶜ
cpos : 0 < c
hδx : δ ≤ ‖x‖
a :
  ∀ (hc : M < c * δ) (x : F) (hx : x ∈ uᶜ) (cpos : 0 < c) (hδx : δ ≤ ‖x‖),
    Membership.mem (γ := Set F) (closedBall 0 M)ᶜ (c • x)
⊢ Membership.mem (γ := Set F) (closedBall 0 M)ᶜ (c • x)

Tactic:
rw [div_lt_iff₀ δpos] at hc

Premises used: div_lt_iff₀
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
u : Set F
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hu : 0 ∈ u
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
h'u : ball 0 δ ⊆ u
M : ℝ
Mpos : M > 0
hM : ∀ ⦃x : F⦄, Membership.mem (γ := Set F) (closedBall 0 M)ᶜ x → ‖x‖ ^ finrank ℝ F * φ x < δ ^ finrank ℝ F * ε
c : ℝ
hc : M < c * δ
x : F
hx : x ∈ uᶜ
cpos : 0 < c
hδx : δ ≤ ‖x‖
a : M < c * ‖x‖
⊢ Membership.mem (γ := Set F) (closedBall 0 M)ᶜ (c • x)

Tactic:
simp only [mem_compl_iff, mem_closedBall, dist_zero_right, norm_smul, Real.norm_eq_abs,
          abs_of_nonneg cpos.le, not_le]

Premises used: not_le, norm_smul, LT.lt.le, abs_of_nonneg, Metric.mem_closedBall, dist_zero_right, Set.mem_compl_iff, Real.norm_eq_abs
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
u : Set F
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hu : 0 ∈ u
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
h'u : ball 0 δ ⊆ u
M : ℝ
Mpos : M > 0
hM : ∀ ⦃x : F⦄, Membership.mem (γ := Set F) (closedBall 0 M)ᶜ x → ‖x‖ ^ finrank ℝ F * φ x < δ ^ finrank ℝ F * ε
c : ℝ
hc : M < c * δ
x : F
hx : x ∈ uᶜ
cpos : 0 < c
hδx : δ ≤ ‖x‖
ha : 0 ≤ c
⊢ c * δ ≤ c * ‖x‖

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
u : Set F
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hu : 0 ∈ u
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
h'u : ball 0 δ ⊆ u
M : ℝ
Mpos : M > 0
hM : ∀ ⦃x : F⦄, Membership.mem (γ := Set F) (closedBall 0 M)ᶜ x → ‖x‖ ^ finrank ℝ F * φ x < δ ^ finrank ℝ F * ε
c : ℝ
hc : M < c * δ
x : F
hx : x ∈ uᶜ
cpos : 0 < c
hδx : δ ≤ ‖x‖
⊢ M < c * ‖x‖

Tactic:
exact hc.trans_le (by gcongr)

Premises used: LT.lt.trans_le
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
u : Set F
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hu : 0 ∈ u
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
h'u : ball 0 δ ⊆ u
M : ℝ
Mpos : M > 0
hM : ∀ ⦃x : F⦄, Membership.mem (γ := Set F) (closedBall 0 M)ᶜ x → ‖x‖ ^ finrank ℝ F * φ x < δ ^ finrank ℝ F * ε
c : ℝ
hc : M / δ < c
x : F
hx : x ∈ uᶜ
cpos : 0 < c
hδx : δ ≤ ‖x‖
δ₁ : δ ^ finrank ℝ F * (c ^ finrank ℝ F * φ (c • x)) ≤ ‖x‖ ^ finrank ℝ F * (c ^ finrank ℝ F * φ (c • x))
δ₂ : ‖x‖ ^ finrank ℝ F * (c ^ finrank ℝ F * φ (c • x)) = ‖c • x‖ ^ finrank ℝ F * φ (c • x)
δ₃ : ‖c • x‖ ^ finrank ℝ F * φ (c • x) < δ ^ finrank ℝ F * ε
⊢ δ ^ finrank ℝ F * (c ^ finrank ℝ F * φ (c • x)) < δ ^ finrank ℝ F * ε

Tactic:
calc
      δ ^ finrank ℝ F * (c ^ finrank ℝ F * φ (c • x))
      _ ≤ ‖x‖ ^ finrank ℝ F * (c ^ finrank ℝ F * φ (c • x)) := by
        gcongr; exact mul_nonneg (by positivity) (hφ _)
      _ = ‖c • x‖ ^ finrank ℝ F * φ (c • x) := by
        simp [norm_smul, abs_of_pos cpos, mul_pow]; ring
      _ < δ ^ finrank ℝ F * ε := by
        apply hM
        rw [div_lt_iff₀ δpos] at hc
        simp only [mem_compl_iff, mem_closedBall, dist_zero_right, norm_smul, Real.norm_eq_abs,
          abs_of_nonneg cpos.le, not_le]
        exact hc.trans_le (by gcongr)

Premises used: Real, HMul.hMul, HPow.hPow, HSMul.hSMul, Module.finrank
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
rw : Tendsto (β := ℝ) (fun (c : ℝ) ↦ ∫ (x : F) in closedBall 0 c, φ x ∂μ) atTop (𝓝 (∫ (x : F), φ x ∂μ))
⊢ Tendsto (β := ℝ) (fun (c : ℝ) ↦ ∫ (x : F) in closedBall 0 c, φ x ∂μ) atTop (𝓝 1)

Tactic:
rw [← h'φ]
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
⊢ Tendsto (β := ℝ) (fun (c : ℝ) ↦ ∫ (x : F) in closedBall 0 c, φ x ∂μ) atTop (𝓝 (∫ (x : F), φ x ∂μ))

Tactic:
(aecover_closedBall tendsto_id).integral_tendsto_of_countably_generated I

Premises used: Filter.tendsto_id, MeasureTheory.AECover.integral_tendsto_of_countably_generated, MeasureTheory.aecover_closedBall
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
⊢ Tendsto (β := ℝ) (fun (c : ℝ) ↦ ∫ (x : F) in closedBall 0 c, φ x ∂μ) atTop (𝓝 (∫ (x : F), φ x ∂μ))

Tactic:
exact (aecover_closedBall tendsto_id).integral_tendsto_of_countably_generated I

Premises used: Filter.tendsto_id, MeasureTheory.AECover.integral_tendsto_of_countably_generated, MeasureTheory.aecover_closedBall
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
⊢ Tendsto (β := ℝ) (fun (c : ℝ) ↦ ∫ (x : F) in closedBall 0 c, φ x ∂μ) atTop (𝓝 1)

Tactic:
have : Tendsto (fun c ↦ ∫ (x : F) in closedBall 0 c, φ x ∂μ) atTop (𝓝 1) := by
      rw [← h'φ]
      exact (aecover_closedBall tendsto_id).integral_tendsto_of_countably_generated I
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
this : Tendsto (β := ℝ) (fun (c : ℝ) ↦ ∫ (x : F) in closedBall 0 c, φ x ∂μ) atTop (𝓝 1)
hiφ :
  EventuallyEq (β := ℝ) atTop (fun (c : ℝ) ↦ ∫ (x : F) in closedBall 0 c, φ x ∂μ) fun (i : ℝ) ↦
    ∫ (x : F) in closedBall 0 1, i ^ finrank ℝ F * φ (i • x) ∂μ
⊢ Tendsto (β := ℝ) (fun (i : ℝ) ↦ ∫ (x : F) in closedBall 0 1, i ^ finrank ℝ F * φ (i • x) ∂μ) atTop (𝓝 1)

Tactic:
apply this.congr'

Premises used: Filter.Tendsto.congr'
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
this : Tendsto (β := ℝ) (fun (c : ℝ) ↦ ∫ (x : F) in closedBall 0 c, φ x ∂μ) atTop (𝓝 1)
c : ℝ
h₁ :
  ∀ (hc : 0 < c),
    Eq (α := ℝ) (∫ (x : F) in closedBall 0 c, φ x ∂μ) (∫ (x : F) in closedBall 0 1, c ^ finrank ℝ F * φ (c • x) ∂μ)
⊢ Membership.mem (γ := Set ℝ) (Ioi 0) c →
    Eq (α := ℝ) (∫ (x : F) in closedBall 0 c, φ x ∂μ) (∫ (x : F) in closedBall 0 1, c ^ finrank ℝ F * φ (c • x) ∂μ)

Tactic:
(hc : 0 < c)
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
this : Tendsto (β := ℝ) (fun (c : ℝ) ↦ ∫ (x : F) in closedBall 0 c, φ x ∂μ) atTop (𝓝 1)
h₁ :
  ∀ (c : ℝ) (hc : 0 < c),
    Eq (α := ℝ) (∫ (x : F) in closedBall 0 c, φ x ∂μ) (∫ (x : F) in closedBall 0 1, c ^ finrank ℝ F * φ (c • x) ∂μ)
⊢ EventuallyEq (β := ℝ) atTop (fun (c : ℝ) ↦ ∫ (x : F) in closedBall 0 c, φ x ∂μ) fun (i : ℝ) ↦
    ∫ (x : F) in closedBall 0 1, i ^ finrank ℝ F * φ (i • x) ∂μ

Tactic:
filter_upwards [Ioi_mem_atTop 0] with c (hc : 0 < c)

Premises used: Filter.Ioi_mem_atTop, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
this : Tendsto (β := ℝ) (fun (c : ℝ) ↦ ∫ (x : F) in closedBall 0 c, φ x ∂μ) atTop (𝓝 1)
c : ℝ
hc : 0 < c
⊢ c ^ finrank ℝ F ≠ 0

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
this : Tendsto (β := ℝ) (fun (c : ℝ) ↦ ∫ (x : F) in closedBall 0 c, φ x ∂μ) atTop (𝓝 1)
c : ℝ
hc : 0 < c
h₁ :
  ∫ (x : F) in closedBall 0 c, φ x ∂μ =
    HMul.hMul (α := ℝ) 1 (∫ (x : F) in closedBall (HSMul.hSMul (β := F) c 0) (‖c‖ * 1), φ x ∂μ)
⊢ Eq (α := ℝ) (∫ (x : F) in closedBall 0 c, φ x ∂μ) (∫ (x : F) in closedBall 0 1, c ^ finrank ℝ F * φ (c • x) ∂μ)

Tactic:
rw [integral_const_mul, setIntegral_comp_smul_of_pos _ _ _ hc, smul_eq_mul, ← mul_assoc,
      mul_inv_cancel₀ (by positivity), _root_.smul_closedBall _ _ zero_le_one]

Premises used: MeasureTheory.integral_const_mul, mul_inv_cancel₀, mul_assoc, zero_le_one, smul_eq_mul, MeasureTheory.Measure.setIntegral_comp_smul_of_pos, smul_closedBall
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
this : Tendsto (β := ℝ) (fun (c : ℝ) ↦ ∫ (x : F) in closedBall 0 c, φ x ∂μ) atTop (𝓝 1)
c : ℝ
hc : 0 < c
⊢ ∫ (x : F) in closedBall 0 c, φ x ∂μ =
    HMul.hMul (α := ℝ) 1 (∫ (x : F) in closedBall (HSMul.hSMul (β := F) c 0) (‖c‖ * 1), φ x ∂μ)

Tactic:
simp [abs_of_nonneg hc.le]

Premises used: LT.lt.le, abs_of_nonneg
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
c : ℝ
h₁ : ∀ (hc : 0 < c), AEStronglyMeasurable (β := ℝ) (fun (x : F) ↦ c ^ finrank ℝ F * φ (c • x)) μ
⊢ Membership.mem (γ := Set ℝ) (Ioi 0) c → AEStronglyMeasurable (β := ℝ) (fun (x : F) ↦ c ^ finrank ℝ F * φ (c • x)) μ

Tactic:
(hc : 0 < c)
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
h₁ : ∀ (c : ℝ) (hc : 0 < c), AEStronglyMeasurable (β := ℝ) (fun (x : F) ↦ c ^ finrank ℝ F * φ (c • x)) μ
⊢ ∀ᶠ (i : ℝ) in atTop, AEStronglyMeasurable (β := ℝ) (fun (x : F) ↦ i ^ finrank ℝ F * φ (i • x)) μ

Tactic:
filter_upwards [Ioi_mem_atTop 0] with c (hc : 0 < c)

Premises used: Filter.Ioi_mem_atTop, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
c : ℝ
hc : 0 < c
⊢ AEStronglyMeasurable (β := ℝ) (fun (x : F) ↦ c ^ finrank ℝ F * φ (c • x)) μ

Tactic:
(I.comp_smul hc.ne').aestronglyMeasurable.const_mul _

Premises used: MeasureTheory.Integrable.aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.const_mul, LT.lt.ne', MeasureTheory.Integrable.comp_smul
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
c : ℝ
hc : 0 < c
⊢ AEStronglyMeasurable (β := ℝ) (fun (x : F) ↦ c ^ finrank ℝ F * φ (c • x)) μ

Tactic:
exact (I.comp_smul hc.ne').aestronglyMeasurable.const_mul _

Premises used: MeasureTheory.Integrable.aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.const_mul, LT.lt.ne', MeasureTheory.Integrable.comp_smul
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
⊢ Integrable g μ

Tactic:
hg
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
⊢ Integrable g μ

Tactic:
exact hg
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
⊢ Tendsto g (𝓝 0) (𝓝 (g 0))

Tactic:
h'g

Premises used: ContinuousAt
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
⊢ Tendsto g (𝓝 0) (𝓝 (g 0))

Tactic:
exact h'g
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
x₀ : F
hg : Integrable g μ
h'g : ContinuousAt g x₀
f : (x : F) → E := fun (x : F) ↦ g (x₀ - x)
⊢ Integrable f μ

Tactic:
simpa [f, sub_eq_add_neg] using (hg.comp_add_left x₀).comp_neg

Premises used: sub_eq_add_neg, MeasureTheory.Integrable.comp_add_left, MeasureTheory.Integrable.comp_neg
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
x₀ : F
hg : Integrable g μ
h'g : ContinuousAt g x₀
f : (x : F) → E := fun (x : F) ↦ g (x₀ - x)
⊢ Integrable f μ

Tactic:
have If : Integrable f μ := by simpa [f, sub_eq_add_neg] using (hg.comp_add_left x₀).comp_neg