simp only [one_div, Nat.cast_add, Nat.cast_one, f]
case h.e'_5.e_x.e_f.h
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 = f (n + N + 1)
no goals