convert finsetSum_tendsto_tsum (f := fun n ↦ f (n + 1)) (N := N) ?_ using 1
N : ℕ
s : ℂ
s_re_gt : 1 < s.re
f : ℕ → ℂ := fun n => 1 / ↑n ^ s
hf : Summable fun n => 1 / ↑n ^ s
⊢ Tendsto (fun k => ∑ x ∈ Finset.Ico (N + 1) (k + 1), 1 / ↑x ^ s) atTop (𝓝 (∑' (n : ℕ), 1 / (↑n + ↑N + 1) ^ s))
case h.e'_3
N : ℕ
s : ℂ
s_re_gt : 1 < s.re
f : ℕ → ℂ := fun n => 1 / ↑n ^ s
hf : Summable fun n => 1 / ↑n ^ s
⊢ (fun k => ∑ x ∈ Finset.Ico (N + 1) (k + 1), 1 / ↑x ^ s) = fun k => ∑ n ∈ Finset.Ico N k, f (n + 1)

case h.e'_5
N : ℕ
s : ℂ
s_re_gt : 1 < s.re
f : ℕ → ℂ := fun n => 1 / ↑n ^ s
hf : Summable fun n => 1 / ↑n ^ s
⊢ 𝓝 (∑' (n : ℕ), 1 / (↑n + ↑N + 1) ^ s) = 𝓝 (∑' (n : ℕ), f (n + N + 1))

N : ℕ
s : ℂ
s_re_gt : 1 < s.re
f : ℕ → ℂ := fun n => 1 / ↑n ^ s
hf : Summable fun n => 1 / ↑n ^ s
⊢ Summable fun n => f (n + 1)