α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
h : Tendsto f atTop (𝓝 0)
this :
  Tendsto (fun n => ∑ i in range n, 1) atTop atTop → (fun n => ∑ i in range n, f i) =o[atTop] fun n => ∑ i in range n, 1
⊢ (fun n => ∑ i in range n, f i) =o[atTop] fun n => ↑n
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
h : Tendsto f atTop (𝓝 0)
⊢ (fun n => ∑ i in range n, f i) =o[atTop] fun n => ↑n
have := ((isLittleO_one_iff ℝ).2 h).sum_range fun i => zero_le_one
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
h : Tendsto f atTop (𝓝 0)
this : Tendsto (fun n => ↑n) atTop atTop → (fun n => ∑ i in range n, f i) =o[atTop] fun n => ↑n
⊢ (fun n => ∑ i in range n, f i) =o[atTop] fun n => ↑n
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
h : Tendsto f atTop (𝓝 0)
this :
  Tendsto (fun n => ∑ i in range n, 1) atTop atTop → (fun n => ∑ i in range n, f i) =o[atTop] fun n => ∑ i in range n, 1
⊢ (fun n => ∑ i in range n, f i) =o[atTop] fun n => ↑n
simp only [sum_const, card_range, Nat.smul_one_eq_coe] at this
no goals
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
h : Tendsto f atTop (𝓝 0)
this : Tendsto (fun n => ↑n) atTop atTop → (fun n => ∑ i in range n, f i) =o[atTop] fun n => ↑n
⊢ (fun n => ∑ i in range n, f i) =o[atTop] fun n => ↑n
exact this tendsto_nat_cast_atTop_atTop