case h.e'_5
z : ℂ
⊢ (fun n => (-1) ^ n * z ^ (2 * n + 1) / ↑(2 * n + 1)!) = fun n => (z * I) ^ (2 * n + 1) / ↑(2 * n + 1)! / I
z : ℂ
⊢ HasSum (fun n => (-1) ^ n * z ^ (2 * n + 1) / ↑(2 * n + 1)!) (sin z)
convert Complex.hasSum_sin' z using 1
no goals
case h.e'_5
z : ℂ
⊢ (fun n => (-1) ^ n * z ^ (2 * n + 1) / ↑(2 * n + 1)!) = fun n => (z * I) ^ (2 * n + 1) / ↑(2 * n + 1)! / I
simp_rw [mul_pow, pow_succ', pow_mul, Complex.I_sq, ← mul_assoc, mul_div_assoc, div_right_comm,
  div_self Complex.I_ne_zero, mul_comm _ ((-1 : ℂ) ^ _), mul_one_div, mul_div_assoc, mul_assoc]