convert HasDerivAt.mul (c := fun z ↦ - (N : ℂ) ^ z) (d := fun z ↦ z⁻¹) (c' := - (N : ℂ) ^ z * Real.log N)
  (d' := - (z ^ 2)⁻¹) ?_ ?_ using 1
N : ℕ
z : ℂ
z_ne_zero : z ≠ 0
⊢ HasDerivAt (fun z => -↑N ^ z * z⁻¹) (↑N ^ z * (z ^ 2)⁻¹ - ↑(↑N).log * ↑N ^ z * z⁻¹) z
case h.e'_7
N : ℕ
z : ℂ
z_ne_zero : z ≠ 0
⊢ ↑N ^ z * (z ^ 2)⁻¹ - ↑(↑N).log * ↑N ^ z * z⁻¹ = -↑N ^ z * ↑(↑N).log * z⁻¹ + -↑N ^ z * -(z ^ 2)⁻¹

case convert_2
N : ℕ
z : ℂ
z_ne_zero : z ≠ 0
⊢ HasDerivAt (fun z => -↑N ^ z) (-↑N ^ z * ↑(↑N).log) z

case convert_3
N : ℕ
z : ℂ
z_ne_zero : z ≠ 0
⊢ HasDerivAt (fun z => z⁻¹) (-(z ^ 2)⁻¹) z