convert hasDerivAt_neg' s |>.const_cpow (c := n) (by aesop) using 1
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
n : ℕ
a✝ : n ∈ Finset.range (N + 1)
⊢ HasDerivAt (fun x => 1 / ↑n ^ x) (-1 / ↑n ^ s * ↑(↑n).log) s
case h.e'_6
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
n : ℕ
a✝ : n ∈ Finset.range (N + 1)
⊢ (fun x => 1 / ↑n ^ x) = fun x => ↑n ^ (-x)

case h.e'_7
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
n : ℕ
a✝ : n ∈ Finset.range (N + 1)
⊢ -1 / ↑n ^ s * ↑(↑n).log = ↑n ^ (-s) * (↑n).log * -1