simp only [natCast_log, neg_mul, cpow_ofNat, mul_neg, neg_neg]
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 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)⁻¹