exact HasDerivAt_cpow_over_var N (by rw [sub_ne_zero]; exact s_ne_one.symm)
case convert_1
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ HasDerivAt (fun z => -↑N ^ z / z) (↑N ^ (1 - s) / (1 - s) ^ 2 - ↑(↑N).log * ↑N ^ (1 - s) / (1 - s))
    ((fun z => 1 - z) s)
no goals