rw [(by simp only [sub_re, one_re, neg_sub] : (1 - s).re = - (s - 1).re)]
s : ℂ
s_re_gt : 1 < s.re
one_sub_s_re_ne : (1 - s).re ≠ 0
⊢ Tendsto (fun x => ↑x ^ (1 - s).re) atTop (𝓝 0)
s : ℂ
s_re_gt : 1 < s.re
one_sub_s_re_ne : (1 - s).re ≠ 0
⊢ Tendsto (fun x => ↑x ^ (-(s - 1).re)) atTop (𝓝 0)