have := Summable.hasSum_iff_tendsto_nat hf (m := ∑' (n : ℕ), f n) |>.mp hf.hasSum
N : ℕ
f : ℕ → ℂ
hf : Summable f
⊢ Tendsto (fun k => ∑ n ∈ Finset.Ico N k, f n) atTop (𝓝 (∑' (n : ℕ), f (n + N)))
N : ℕ
f : ℕ → ℂ
hf : Summable f
this : Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 (∑' (n : ℕ), f n))
⊢ Tendsto (fun k => ∑ n ∈ Finset.Ico N k, f n) atTop (𝓝 (∑' (n : ℕ), f (n + N)))