awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (hypothesis)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
⊢ IsLittleO.{0, u_1, 0} (E := α) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) fun (n : ℕ) ↦ ∑ i ∈ range n, g i
have B : ∀ (n : ℕ), norm (E := ℝ) (∑ i ∈ range n, g i) = ∑ i ∈ range n, g i
Tactic: have B : ∀ n, ‖∑ i ∈ range n, g i‖ = ∑ i ∈ range n, g i := fun n => by
    rwa [Real.norm_eq_abs, abs_sum_of_nonneg']
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), norm (E := ℝ) (∑ i ∈ range n, g i) = ∑ i ∈ range n, g i
⊢ IsLittleO.{0, u_1, 0} (E := α) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) fun (n : ℕ) ↦ ∑ i ∈ range n, g i
have apply : ∀ (ε : ℝ) (εpos : 0 < ε),
  ∀ᶠ (x : ℕ) in atTop, norm.{u_1} (E := α) (∑ i ∈ range x, f i) ≤ ε * norm (E := ℝ) (∑ i ∈ range x, g i)
Tactic: apply isLittleO_iff.2 fun ε εpos => _
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), norm (E := ℝ) (∑ i ∈ range n, g i) = ∑ i ∈ range n, g i
ε : ℝ
εpos : 0 < ε
⊢ ∀ᶠ (x : ℕ) in atTop, norm.{u_1} (E := α) (∑ i ∈ range x, f i) ≤ ε * norm (E := ℝ) (∑ i ∈ range x, g i)
have obtain : ∀ (N : ℕ) (hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b),
  ∀ᶠ (x : ℕ) in atTop, norm.{u_1} (E := α) (∑ i ∈ range x, f i) ≤ ε * norm (E := ℝ) (∑ i ∈ range x, g i)
Tactic: obtain ⟨N, hN⟩ : ∃ N : ℕ, ∀ b : ℕ, N ≤ b → ‖f b‖ ≤ ε / 2 * g b := by
    simpa only [A, eventually_atTop] using isLittleO_iff.mp h (half_pos εpos)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), norm (E := ℝ) (∑ i ∈ range n, g i) = ∑ i ∈ range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
⊢ IsLittleO.{0, u_1, 0} (E := α) (F := ℝ) atTop (fun (x : ℕ) ↦ ∑ i ∈ range N, f i) fun (n : ℕ) ↦ ∑ i ∈ range n, g i
have apply : Eq.{u_1 + 1} (α := α) (∑ i ∈ range N, f i) 0 ∨
  Tendsto (α := ℕ) (Function.comp (β := ℝ) norm fun (n : ℕ) ↦ ∑ i ∈ range n, g i) atTop atTop
Tactic: apply isLittleO_const_left.2
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (hypothesis)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), norm (E := ℝ) (∑ i ∈ range n, g i) = ∑ i ∈ range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
⊢ ∀ᶠ (x : ℕ) in atTop, norm.{u_1} (E := α) (∑ i ∈ range x, f i) ≤ ε * norm (E := ℝ) (∑ i ∈ range x, g i)
have this : IsLittleO.{0, u_1, 0} (E := α) (F := ℝ) atTop (fun (x : ℕ) ↦ ∑ i ∈ range N, f i) fun (n : ℕ) ↦ ∑ i ∈ range n, g i
Tactic: have : (fun _ : ℕ => ∑ i ∈ range N, f i) =o[atTop] fun n : ℕ => ∑ i ∈ range n, g i := by
    apply isLittleO_const_left.2
    exact Or.inr (h'g.congr fun n => (B n).symm)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), norm (E := ℝ) (∑ i ∈ range n, g i) = ∑ i ∈ range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : IsLittleO.{0, u_1, 0} (E := α) (F := ℝ) atTop (fun (x : ℕ) ↦ ∑ i ∈ range N, f i) fun (n : ℕ) ↦ ∑ i ∈ range n, g i
⊢ ∀ᶠ (x : ℕ) in atTop, norm.{u_1} (E := α) (∑ i ∈ range x, f i) ≤ ε * norm (E := ℝ) (∑ i ∈ range x, g i)
have h₁ : ∀ (n : ℕ) (hn : norm.{u_1} (E := α) (∑ i ∈ range N, f i) ≤ ε / 2 * norm (E := ℝ) (∑ i ∈ range n, g i))
  (Nn : n ∈ Set.Ici N), norm.{u_1} (E := α) (∑ i ∈ range n, f i) ≤ ε * norm (E := ℝ) (∑ i ∈ range n, g i)
Tactic: filter_upwards [isLittleO_iff.1 this (half_pos εpos), Ici_mem_atTop N] with n hn Nn
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), norm (E := ℝ) (∑ i ∈ range n, g i) = ∑ i ∈ range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : IsLittleO.{0, u_1, 0} (E := α) (F := ℝ) atTop (fun (x : ℕ) ↦ ∑ i ∈ range N, f i) fun (n : ℕ) ↦ ∑ i ∈ range n, g i
n : ℕ
hn : norm.{u_1} (E := α) (∑ i ∈ range N, f i) ≤ ε / 2 * norm (E := ℝ) (∑ i ∈ range n, g i)
Nn : n ∈ Set.Ici N
⊢ norm.{u_1} (E := α) (∑ i ∈ range n, f i) = ‖HAdd.hAdd (α := α) (∑ i ∈ range N, f i) (∑ i ∈ Ico N n, f i)‖
have rw : norm.{u_1} (E := α) (∑ i ∈ range n, f i) = norm.{u_1} (E := α) (∑ k ∈ range n, f k)
Tactic: rw [sum_range_add_sum_Ico _ Nn]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), norm (E := ℝ) (∑ i ∈ range n, g i) = ∑ i ∈ range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : IsLittleO.{0, u_1, 0} (E := α) (F := ℝ) atTop (fun (x : ℕ) ↦ ∑ i ∈ range N, f i) fun (n : ℕ) ↦ ∑ i ∈ range n, g i
n : ℕ
hn : norm.{u_1} (E := α) (∑ i ∈ range N, f i) ≤ ε / 2 * norm (E := ℝ) (∑ i ∈ range n, g i)
Nn : n ∈ Set.Ici N
⊢ norm.{u_1} (E := α) (∑ i ∈ range N, f i) + ∑ i ∈ Ico N n, ε / 2 * g i ≤
    norm.{u_1} (E := α) (∑ i ∈ range N, f i) + ∑ i ∈ range n, ε / 2 * g i
have bc : ∀ i ∈ range n, i ∉ Ico N n → 0 ≤ ε / 2 * g i
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), norm (E := ℝ) (∑ i ∈ range n, g i) = ∑ i ∈ range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : IsLittleO.{0, u_1, 0} (E := α) (F := ℝ) atTop (fun (x : ℕ) ↦ ∑ i ∈ range N, f i) fun (n : ℕ) ↦ ∑ i ∈ range n, g i
n : ℕ
hn : norm.{u_1} (E := α) (∑ i ∈ range N, f i) ≤ ε / 2 * norm (E := ℝ) (∑ i ∈ range n, g i)
Nn : n ∈ Set.Ici N
bc : ∀ i ∈ range n, i ∉ Ico N n → 0 ≤ ε / 2 * g i
⊢ norm.{u_1} (E := α) (∑ i ∈ range N, f i) + ∑ i ∈ Ico N n, ε / 2 * g i ≤
    norm.{u_1} (E := α) (∑ i ∈ range N, f i) + ∑ i ∈ range n, ε / 2 * g i
have bc₁ : Ico N n ⊆ range n
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), norm (E := ℝ) (∑ i ∈ range n, g i) = ∑ i ∈ range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : IsLittleO.{0, u_1, 0} (E := α) (F := ℝ) atTop (fun (x : ℕ) ↦ ∑ i ∈ range N, f i) fun (n : ℕ) ↦ ∑ i ∈ range n, g i
n : ℕ
hn : norm.{u_1} (E := α) (∑ i ∈ range N, f i) ≤ ε / 2 * norm (E := ℝ) (∑ i ∈ range n, g i)
Nn : n ∈ Set.Ici N
⊢ Ico N n ⊆ range n
have bc : Ico N n ⊆ Ico 0 n
Tactic: rw [range_eq_Ico]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), norm (E := ℝ) (∑ i ∈ range n, g i) = ∑ i ∈ range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : IsLittleO.{0, u_1, 0} (E := α) (F := ℝ) atTop (fun (x : ℕ) ↦ ∑ i ∈ range N, f i) fun (n : ℕ) ↦ ∑ i ∈ range n, g i
n : ℕ
hn : norm.{u_1} (E := α) (∑ i ∈ range N, f i) ≤ ε / 2 * norm (E := ℝ) (∑ i ∈ range n, g i)
Nn : n ∈ Set.Ici N
⊢ norm.{u_1} (E := α) (∑ i ∈ range N, f i) + ∑ i ∈ range n, ε / 2 * g i ≤
    ε / 2 * norm (E := ℝ) (∑ i ∈ range n, g i) + ε / 2 * ∑ i ∈ range n, g i
have rw : norm.{u_1} (E := α) (∑ i ∈ range N, f i) + ε / 2 * ∑ i ∈ range n, g i ≤
  ε / 2 * norm (E := ℝ) (∑ i ∈ range n, g i) + ε / 2 * ∑ i ∈ range n, g i
Tactic: rw [← mul_sum]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), norm (E := ℝ) (∑ i ∈ range n, g i) = ∑ i ∈ range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : IsLittleO.{0, u_1, 0} (E := α) (F := ℝ) atTop (fun (x : ℕ) ↦ ∑ i ∈ range N, f i) fun (n : ℕ) ↦ ∑ i ∈ range n, g i
n : ℕ
hn : norm.{u_1} (E := α) (∑ i ∈ range N, f i) ≤ ε / 2 * norm (E := ℝ) (∑ i ∈ range n, g i)
Nn : n ∈ Set.Ici N
⊢ ε / 2 * norm (E := ℝ) (∑ i ∈ range n, g i) + ε / 2 * ∑ i ∈ range n, g i = ε * norm (E := ℝ) (∑ i ∈ range n, g i)
have simp : ε / 2 * ∑ i ∈ range n, g i + ε / 2 * ∑ i ∈ range n, g i = ε * ∑ i ∈ range n, g i
Tactic: simp only [B]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), norm (E := ℝ) (∑ i ∈ range n, g i) = ∑ i ∈ range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : IsLittleO.{0, u_1, 0} (E := α) (F := ℝ) atTop (fun (x : ℕ) ↦ ∑ i ∈ range N, f i) fun (n : ℕ) ↦ ∑ i ∈ range n, g i
n : ℕ
hn : norm.{u_1} (E := α) (∑ i ∈ range N, f i) ≤ ε / 2 * norm (E := ℝ) (∑ i ∈ range n, g i)
Nn : n ∈ Set.Ici N
⊢ norm.{u_1} (E := α) (∑ i ∈ range n, f i) ≤ ε * norm (E := ℝ) (∑ i ∈ range n, g i)
have i : norm.{u_1} (E := α) (∑ i ∈ range n, f i) = ‖HAdd.hAdd (α := α) (∑ i ∈ range N, f i) (∑ i ∈ Ico N n, f i)‖
Tactic: calc
    ‖∑ i ∈ range n, f i‖ = ‖(∑ i ∈ range N, f i) + ∑ i ∈ Ico N n, f i‖ := by
      rw [sum_range_add_sum_Ico _ Nn]
    _ ≤ ‖∑ i ∈ range N, f i‖ + ‖∑ i ∈ Ico N n, f i‖ := norm_add_le _ _
    _ ≤ ‖∑ i ∈ range N, f i‖ + ∑ i ∈ Ico N n, ε / 2 * g i :=
      (add_le_add le_rfl (norm_sum_le_of_le _ fun i hi => hN _ (mem_Ico.1 hi).1))
    _ ≤ ‖∑ i ∈ range N, f i‖ + ∑ i ∈ range n, ε / 2 * g i := by
      gcongr
      · exact fun i _ _ ↦ mul_nonneg (half_pos εpos).le (hg i)
      · rw [range_eq_Ico]
        exact Ico_subset_Ico zero_le le_rfl
    _ ≤ ε / 2 * ‖∑ i ∈ range n, g i‖ + ε / 2 * ∑ i ∈ range n, g i := by rw [← mul_sum]; gcongr
    _ = ε * ‖∑ i ∈ range n, g i‖ := by
      simp only [B]
      ring
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), norm (E := ℝ) (∑ i ∈ range n, g i) = ∑ i ∈ range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : IsLittleO.{0, u_1, 0} (E := α) (F := ℝ) atTop (fun (x : ℕ) ↦ ∑ i ∈ range N, f i) fun (n : ℕ) ↦ ∑ i ∈ range n, g i
n : ℕ
hn : norm.{u_1} (E := α) (∑ i ∈ range N, f i) ≤ ε / 2 * norm (E := ℝ) (∑ i ∈ range n, g i)
Nn : n ∈ Set.Ici N
i : norm.{u_1} (E := α) (∑ i ∈ range n, f i) = ‖HAdd.hAdd (α := α) (∑ i ∈ range N, f i) (∑ i ∈ Ico N n, f i)‖
⊢ norm.{u_1} (E := α) (∑ i ∈ range n, f i) ≤ ε * norm (E := ℝ) (∑ i ∈ range n, g i)
have i₁ : norm.{u_1} (E := α) (∑ i ∈ range N, f i) + ∑ i ∈ Ico N n, ε / 2 * g i ≤
  norm.{u_1} (E := α) (∑ i ∈ range N, f i) + ∑ i ∈ range n, ε / 2 * g i
Tactic: calc
    ‖∑ i ∈ range n, f i‖ = ‖(∑ i ∈ range N, f i) + ∑ i ∈ Ico N n, f i‖ := by
      rw [sum_range_add_sum_Ico _ Nn]
    _ ≤ ‖∑ i ∈ range N, f i‖ + ‖∑ i ∈ Ico N n, f i‖ := norm_add_le _ _
    _ ≤ ‖∑ i ∈ range N, f i‖ + ∑ i ∈ Ico N n, ε / 2 * g i :=
      (add_le_add le_rfl (norm_sum_le_of_le _ fun i hi => hN _ (mem_Ico.1 hi).1))
    _ ≤ ‖∑ i ∈ range N, f i‖ + ∑ i ∈ range n, ε / 2 * g i := by
      gcongr
      · exact fun i _ _ ↦ mul_nonneg (half_pos εpos).le (hg i)
      · rw [range_eq_Ico]
        exact Ico_subset_Ico zero_le le_rfl
    _ ≤ ε / 2 * ‖∑ i ∈ range n, g i‖ + ε / 2 * ∑ i ∈ range n, g i := by rw [← mul_sum]; gcongr
    _ = ε * ‖∑ i ∈ range n, g i‖ := by
      simp only [B]
      ring
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), norm (E := ℝ) (∑ i ∈ range n, g i) = ∑ i ∈ range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : IsLittleO.{0, u_1, 0} (E := α) (F := ℝ) atTop (fun (x : ℕ) ↦ ∑ i ∈ range N, f i) fun (n : ℕ) ↦ ∑ i ∈ range n, g i
n : ℕ
hn : norm.{u_1} (E := α) (∑ i ∈ range N, f i) ≤ ε / 2 * norm (E := ℝ) (∑ i ∈ range n, g i)
Nn : n ∈ Set.Ici N
i : norm.{u_1} (E := α) (∑ i ∈ range n, f i) = ‖HAdd.hAdd (α := α) (∑ i ∈ range N, f i) (∑ i ∈ Ico N n, f i)‖
i₁ :
  norm.{u_1} (E := α) (∑ i ∈ range N, f i) + ∑ i ∈ Ico N n, ε / 2 * g i ≤
    norm.{u_1} (E := α) (∑ i ∈ range N, f i) + ∑ i ∈ range n, ε / 2 * g i
⊢ norm.{u_1} (E := α) (∑ i ∈ range n, f i) ≤ ε * norm (E := ℝ) (∑ i ∈ range n, g i)
have i₂ : norm.{u_1} (E := α) (∑ i ∈ range N, f i) + ∑ i ∈ range n, ε / 2 * g i ≤
  ε / 2 * norm (E := ℝ) (∑ i ∈ range n, g i) + ε / 2 * ∑ i ∈ range n, g i
Tactic: calc
    ‖∑ i ∈ range n, f i‖ = ‖(∑ i ∈ range N, f i) + ∑ i ∈ Ico N n, f i‖ := by
      rw [sum_range_add_sum_Ico _ Nn]
    _ ≤ ‖∑ i ∈ range N, f i‖ + ‖∑ i ∈ Ico N n, f i‖ := norm_add_le _ _
    _ ≤ ‖∑ i ∈ range N, f i‖ + ∑ i ∈ Ico N n, ε / 2 * g i :=
      (add_le_add le_rfl (norm_sum_le_of_le _ fun i hi => hN _ (mem_Ico.1 hi).1))
    _ ≤ ‖∑ i ∈ range N, f i‖ + ∑ i ∈ range n, ε / 2 * g i := by
      gcongr
      · exact fun i _ _ ↦ mul_nonneg (half_pos εpos).le (hg i)
      · rw [range_eq_Ico]
        exact Ico_subset_Ico zero_le le_rfl
    _ ≤ ε / 2 * ‖∑ i ∈ range n, g i‖ + ε / 2 * ∑ i ∈ range n, g i := by rw [← mul_sum]; gcongr
    _ = ε * ‖∑ i ∈ range n, g i‖ := by
      simp only [B]
      ring
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), norm (E := ℝ) (∑ i ∈ range n, g i) = ∑ i ∈ range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : IsLittleO.{0, u_1, 0} (E := α) (F := ℝ) atTop (fun (x : ℕ) ↦ ∑ i ∈ range N, f i) fun (n : ℕ) ↦ ∑ i ∈ range n, g i
n : ℕ
hn : norm.{u_1} (E := α) (∑ i ∈ range N, f i) ≤ ε / 2 * norm (E := ℝ) (∑ i ∈ range n, g i)
Nn : n ∈ Set.Ici N
i : norm.{u_1} (E := α) (∑ i ∈ range n, f i) = ‖HAdd.hAdd (α := α) (∑ i ∈ range N, f i) (∑ i ∈ Ico N n, f i)‖
i₁ :
  norm.{u_1} (E := α) (∑ i ∈ range N, f i) + ∑ i ∈ Ico N n, ε / 2 * g i ≤
    norm.{u_1} (E := α) (∑ i ∈ range N, f i) + ∑ i ∈ range n, ε / 2 * g i
i₂ :
  norm.{u_1} (E := α) (∑ i ∈ range N, f i) + ∑ i ∈ range n, ε / 2 * g i ≤
    ε / 2 * norm (E := ℝ) (∑ i ∈ range n, g i) + ε / 2 * ∑ i ∈ range n, g i
⊢ norm.{u_1} (E := α) (∑ i ∈ range n, f i) ≤ ε * norm (E := ℝ) (∑ i ∈ range n, g i)
have i₃ : ε / 2 * norm (E := ℝ) (∑ i ∈ range n, g i) + ε / 2 * ∑ i ∈ range n, g i = ε * norm (E := ℝ) (∑ i ∈ range n, g i)
Tactic: calc
    ‖∑ i ∈ range n, f i‖ = ‖(∑ i ∈ range N, f i) + ∑ i ∈ Ico N n, f i‖ := by
      rw [sum_range_add_sum_Ico _ Nn]
    _ ≤ ‖∑ i ∈ range N, f i‖ + ‖∑ i ∈ Ico N n, f i‖ := norm_add_le _ _
    _ ≤ ‖∑ i ∈ range N, f i‖ + ∑ i ∈ Ico N n, ε / 2 * g i :=
      (add_le_add le_rfl (norm_sum_le_of_le _ fun i hi => hN _ (mem_Ico.1 hi).1))
    _ ≤ ‖∑ i ∈ range N, f i‖ + ∑ i ∈ range n, ε / 2 * g i := by
      gcongr
      · exact fun i _ _ ↦ mul_nonneg (half_pos εpos).le (hg i)
      · rw [range_eq_Ico]
        exact Ico_subset_Ico zero_le le_rfl
    _ ≤ ε / 2 * ‖∑ i ∈ range n, g i‖ + ε / 2 * ∑ i ∈ range n, g i := by rw [← mul_sum]; gcongr
    _ = ε * ‖∑ i ∈ range n, g i‖ := by
      simp only [B]
      ring
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (hypothesis)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
f : ℕ → α
h : Tendsto f atTop (𝓝 0)
⊢ IsLittleO.{0, u_1, 0} (E := α) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) fun (n : ℕ) ↦ (↑n : ℝ)
have this : ∀ (h'g : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, 1) atTop atTop),
  IsLittleO.{0, u_1, 0} (E := α) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) fun (n : ℕ) ↦ ∑ i ∈ range n, 1
Tactic: have := ((isLittleO_one_iff ℝ).2 h).sum_range fun i => zero_le_one
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (hypothesis)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
f : ℕ → α
h : Tendsto f atTop (𝓝 0)
this :
  ∀ (h'g : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, 1) atTop atTop),
    IsLittleO.{0, u_1, 0} (E := α) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) fun (n : ℕ) ↦ ∑ i ∈ range n, 1
⊢ IsLittleO.{0, u_1, 0} (E := α) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) fun (n : ℕ) ↦ (↑n : ℝ)
have this₁ : ∀ (h'g : Tendsto (β := ℝ) (fun (n : ℕ) ↦ (↑n : ℝ)) atTop atTop),
  IsLittleO.{0, u_1, 0} (E := α) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) fun (n : ℕ) ↦ (↑n : ℝ)
Tactic: simp only [sum_const, card_range, Nat.smul_one_eq_cast] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
⊢ Tendsto (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, u i)) atTop (𝓝 l)
have rw : IsLittleO.{0, u_1, 0} (E := E) (F := ℝ) atTop
  (fun (x : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑x : ℝ)⁻¹ (∑ i ∈ range x, u i) - l) fun (_x : ℕ) ↦ 1
Tactic: rw [← tendsto_sub_nhds_zero_iff, ← isLittleO_one_iff ℝ]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
⊢ IsLittleO.{0, u_1, 0} (E := E) (F := ℝ) atTop
    (fun (x : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑x : ℝ)⁻¹ (∑ i ∈ range x, u i) - l) fun (_x : ℕ) ↦ 1
have this : IsLittleO.{0, u_1, 0} (E := E) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ i ∈ range n, (u i - l)) fun (n : ℕ) ↦ (↑n : ℝ)
Tactic: have := Asymptotics.isLittleO_sum_range_of_tendsto_zero (tendsto_sub_nhds_zero_iff.2 h)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
this : IsLittleO.{0, u_1, 0} (E := E) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ i ∈ range n, (u i - l)) fun (n : ℕ) ↦ (↑n : ℝ)
⊢ IsLittleO.{0, u_1, 0} (E := E) (F := ℝ) atTop
    (fun (x : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑x : ℝ)⁻¹ (∑ i ∈ range x, u i) - l) fun (_x : ℕ) ↦ 1
have apply : EventuallyEq.{0, u_1} (β := E) atTop (fun (x : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑x : ℝ)⁻¹ (∑ i ∈ range x, (u i - l)))
  fun (x : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑x : ℝ)⁻¹ (∑ i ∈ range x, u i) - l
Tactic: apply ((isBigO_refl (fun n : ℕ => (n : ℝ)⁻¹) atTop).smul_isLittleO this).congr' _ _
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
this : IsLittleO.{0, u_1, 0} (E := E) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ i ∈ range n, (u i - l)) fun (n : ℕ) ↦ (↑n : ℝ)
apply :
  EventuallyEq.{0, u_1} (β := E) atTop
    (fun (x : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑x : ℝ)⁻¹ (∑ i ∈ range x, (u i - l))) fun (x : ℕ) ↦
    HSMul.hSMul (α := ℝ) (β := E) (↑x : ℝ)⁻¹ (∑ i ∈ range x, u i) - l
⊢ IsLittleO.{0, u_1, 0} (E := E) (F := ℝ) atTop
    (fun (x : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑x : ℝ)⁻¹ (∑ i ∈ range x, u i) - l) fun (_x : ℕ) ↦ 1
have apply₁ : EventuallyEq (β := ℝ) atTop (fun (x : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := ℝ) (↑x : ℝ)⁻¹ (↑x : ℝ)) fun (_x : ℕ) ↦ 1
Tactic: apply ((isBigO_refl (fun n : ℕ => (n : ℝ)⁻¹) atTop).smul_isLittleO this).congr' _ _
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
this : IsLittleO.{0, u_1, 0} (E := E) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ i ∈ range n, (u i - l)) fun (n : ℕ) ↦ (↑n : ℝ)
⊢ EventuallyEq.{0, u_1} (β := E) atTop
    (fun (x : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑x : ℝ)⁻¹ (∑ i ∈ range x, (u i - l))) fun (x : ℕ) ↦
    HSMul.hSMul (α := ℝ) (β := E) (↑x : ℝ)⁻¹ (∑ i ∈ range x, u i) - l
have h₁ : ∀ (n : ℕ) (npos : Membership.mem (γ := Set ℕ) (Set.Ici 1) n),
  HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, (u i - l)) =
    HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, u i) - l
Tactic: filter_upwards [Ici_mem_atTop 1] with n npos
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
this : IsLittleO.{0, u_1, 0} (E := E) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ i ∈ range n, (u i - l)) fun (n : ℕ) ↦ (↑n : ℝ)
n : ℕ
npos : Membership.mem (γ := Set ℕ) (Set.Ici 1) n
⊢ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, (u i - l)) =
    HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, u i) - l
have nposℝ : LT.lt (α := ℝ) 0 (↑n : ℝ)
Tactic: have nposℝ : (0 : ℝ) < n := Nat.cast_pos.2 npos
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
this : IsLittleO.{0, u_1, 0} (E := E) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ i ∈ range n, (u i - l)) fun (n : ℕ) ↦ (↑n : ℝ)
n : ℕ
npos : Membership.mem (γ := Set ℕ) (Set.Ici 1) n
nposℝ : LT.lt (α := ℝ) 0 (↑n : ℝ)
⊢ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, (u i - l)) =
    HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, u i) - l
have h₁ : HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (n • l) = l
Tactic: simp only [smul_sub, sum_sub_distrib, sum_const, card_range, sub_right_inj]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
this : IsLittleO.{0, u_1, 0} (E := E) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ i ∈ range n, (u i - l)) fun (n : ℕ) ↦ (↑n : ℝ)
n : ℕ
npos : Membership.mem (γ := Set ℕ) (Set.Ici 1) n
nposℝ : LT.lt (α := ℝ) 0 (↑n : ℝ)
⊢ HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (n • l) = l
have h₁ : HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (HSMul.hSMul (α := ℝ) (↑n : ℝ) l) = l
Tactic: rw [← Nat.cast_smul_eq_nsmul ℝ, smul_smul, inv_mul_cancel₀ nposℝ.ne', one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
this : IsLittleO.{0, u_1, 0} (E := E) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ i ∈ range n, (u i - l)) fun (n : ℕ) ↦ (↑n : ℝ)
n : ℕ
npos : Membership.mem (γ := Set ℕ) (Set.Ici 1) n
nposℝ : LT.lt (α := ℝ) 0 (↑n : ℝ)
h₁ : HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (HSMul.hSMul (α := ℝ) (↑n : ℝ) l) = l
⊢ HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (n • l) = l
have h₂ : HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑n : ℝ) • l = l
Tactic: rw [← Nat.cast_smul_eq_nsmul ℝ, smul_smul, inv_mul_cancel₀ nposℝ.ne', one_smul]