simp_rw [mul_comm_div, one_mul, one_div, cpow_neg]
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 / ↑N ^ s)) atTop (𝓝 (↑N ^ (-s) / 2))
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 => (↑N ^ s)⁻¹ / 2) atTop (𝓝 ((↑N ^ s)⁻¹ / 2))