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