apply cpow_tendsto s_re_gt |>.sub_const _ |>.div_const _ |>.add
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 1 < s.re
s_ne_zero : s ≠ 0
s_ne_one : s ≠ 1
⊢ Tendsto (fun x => (↑x ^ (1 - s) - ↑N ^ (1 - s)) / (1 - s) + 1 / 2 * (1 / ↑x ^ s)) atTop
    (𝓝 ((0 - ↑N ^ (1 - s)) / (1 - s) + 0))
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 1 < s.re
s_ne_zero : s ≠ 0
s_ne_one : s ≠ 1
⊢ Tendsto (fun x => 1 / 2 * (1 / ↑x ^ s)) atTop (𝓝 0)