convert HasDerivAt.comp (h₂ := fun z ↦ -(N : ℂ) ^ z / z) (h := fun z ↦ 1 - z) (h' := -1)
  (h₂' := ((N : ℂ) ^ (1 - s) / (1 - s) ^ 2 - Real.log (N : ℝ) * (N : ℂ) ^ (1 - s) / (1 - s)))
  (x := s) ?_ ?_ using 1
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ HasDerivAt (fun x => -↑N ^ (1 - x) / (1 - x)) (-↑N ^ (1 - s) / (1 - s) ^ 2 + ↑(↑N).log * ↑N ^ (1 - s) / (1 - s)) s
case h.e'_7
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ -↑N ^ (1 - s) / (1 - s) ^ 2 + ↑(↑N).log * ↑N ^ (1 - s) / (1 - s) =
    (↑N ^ (1 - s) / (1 - s) ^ 2 - ↑(↑N).log * ↑N ^ (1 - s) / (1 - s)) * -1

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)

case convert_2
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ HasDerivAt (fun z => 1 - z) (-1) s