rw [tsum_eq_partial_add_tail f hf (N := N), add_comm, add_sub_cancel_right] at this
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))
this :
  Tendsto (fun x => ∑ i ∈ Finset.range x, f i - ∑ i ∈ Finset.range N, f i) atTop
    (𝓝 (∑' (n : ℕ), f n - ∑ i ∈ Finset.range N, f i))
⊢ 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))
this : Tendsto (fun x => ∑ i ∈ Finset.range x, f i - ∑ i ∈ Finset.range N, f i) atTop (𝓝 (∑' (n : ℕ), f (n + N)))
⊢ Tendsto (fun k => ∑ n ∈ Finset.Ico N k, f n) atTop (𝓝 (∑' (n : ℕ), f (n + N)))