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