simp only [Finset.mem_Ico, Finset.map_add_right_Ico]
case h.e'_2.h.a
N : ℕ
s : ℂ
s_re_gt : 1 < s.re
f : ℕ → ℂ := fun n => 1 / ↑n ^ s
hf : Summable fun n => 1 / ↑n ^ s
k n : ℕ
⊢ n ∈ Finset.Ico (N + 1) (k + 1) ↔ n ∈ Finset.map (addRightEmbedding 1) (Finset.Ico N k)
no goals