simp_rw [norm_natCast_cpow_of_re_ne_zero _ this]
case hf
s : ℂ
s_re_gt : 1 < s.re
this : s.re ≠ 0
⊢ Summable fun a => ‖↑a ^ s‖⁻¹
case hf
s : ℂ
s_re_gt : 1 < s.re
this : s.re ≠ 0
⊢ Summable fun a => (↑a ^ s.re)⁻¹