have const := @tendsto_const_nhds (x := ∑ i in Finset.range N, f i) ℕ _ atTop
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)))
N : ℕ
f : ℕ → ℂ
hf : Summable f
this : Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 (∑' (n : ℕ), f n))
const : Tendsto (fun x => ∑ i ∈ Finset.range N, f i) atTop (𝓝 (∑ i ∈ Finset.range N, f i))
⊢ Tendsto (fun k => ∑ n ∈ Finset.Ico N k, f n) atTop (𝓝 (∑' (n : ℕ), f (n + N)))