convert HasDerivAt.const_cpow (c := (N : ℂ)) (f := id) (f' := 1) (x := z) (hasDerivAt_id z)
  (by simp [z_ne_zero]) using 1
case convert_2.h
N : ℕ
z : ℂ
z_ne_zero : z ≠ 0
⊢ HasDerivAt (fun x => ↑N ^ x) (↑N ^ z * (↑N).log) z
case h.e'_7
N : ℕ
z : ℂ
z_ne_zero : z ≠ 0
⊢ ↑N ^ z * (↑N).log = ↑N ^ id z * (↑N).log * 1