simp_rw [norm_inv, Complex.norm_natCast_cpow_of_re_ne_zero _ <| ne_of_gt hs]
s : ℂ
hs : 0 < s.re
⊢ Tendsto (fun x => ‖(↑x ^ s)⁻¹‖) atTop (𝓝 0)
s : ℂ
hs : 0 < s.re
⊢ Tendsto (fun x => (↑x ^ s.re)⁻¹) atTop (𝓝 0)