case refine'_1
α : Type ?u.192
β : Type ?u.195
ι : Type ?u.198
f : ℕ → ℝ
r : ℝ
hr : Tendsto (fun n => ∑ i in Finset.range n, abs (f i)) atTop (𝓝 r)
⊢ ∀ (i : ℕ), 0 ≤ ‖f i‖

case refine'_2
α : Type ?u.192
β : Type ?u.195
ι : Type ?u.198
f : ℕ → ℝ
r : ℝ
hr : Tendsto (fun n => ∑ i in Finset.range n, abs (f i)) atTop (𝓝 r)
⊢ Tendsto (fun n => ∑ i in Finset.range n, ‖f i‖) atTop (𝓝 r)
α : Type ?u.192
β : Type ?u.195
ι : Type ?u.198
f : ℕ → ℝ
r : ℝ
hr : Tendsto (fun n => ∑ i in Finset.range n, abs (f i)) atTop (𝓝 r)
⊢ Summable f
refine' summable_of_summable_norm ⟨r, (hasSum_iff_tendsto_nat_of_nonneg _ _).2 _⟩
case refine'_2
α : Type ?u.192
β : Type ?u.195
ι : Type ?u.198
f : ℕ → ℝ
r : ℝ
hr : Tendsto (fun n => ∑ i in Finset.range n, abs (f i)) atTop (𝓝 r)
⊢ Tendsto (fun n => ∑ i in Finset.range n, ‖f i‖) atTop (𝓝 r)
case refine'_1
α : Type ?u.192
β : Type ?u.195
ι : Type ?u.198
f : ℕ → ℝ
r : ℝ
hr : Tendsto (fun n => ∑ i in Finset.range n, abs (f i)) atTop (𝓝 r)
⊢ ∀ (i : ℕ), 0 ≤ ‖f i‖

case refine'_2
α : Type ?u.192
β : Type ?u.195
ι : Type ?u.198
f : ℕ → ℝ
r : ℝ
hr : Tendsto (fun n => ∑ i in Finset.range n, abs (f i)) atTop (𝓝 r)
⊢ Tendsto (fun n => ∑ i in Finset.range n, ‖f i‖) atTop (𝓝 r)
exact fun i ↦ norm_nonneg _
no goals
case refine'_2
α : Type ?u.192
β : Type ?u.195
ι : Type ?u.198
f : ℕ → ℝ
r : ℝ
hr : Tendsto (fun n => ∑ i in Finset.range n, abs (f i)) atTop (𝓝 r)
⊢ Tendsto (fun n => ∑ i in Finset.range n, ‖f i‖) atTop (𝓝 r)
simpa only using hr