-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Series (goal)
Goal:
z : ℂ
this :
  HasSum
    (fun (x : ℕ × Fin 2) ↦
      ((-z * I) ^ (2 * x.1 + (↑x.2 : ℕ)) / (↑(2 * x.1 + (↑x.2 : ℕ))! : ℂ) -
            (z * I) ^ (2 * x.1 + (↑x.2 : ℕ)) / (↑(2 * x.1 + (↑x.2 : ℕ))! : ℂ)) *
          I /
        2)
    ((NormedSpace.exp (-z * I) - NormedSpace.exp (z * I)) * I / 2)
k : ℕ
h :
  (z * I) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ) / I =
    ((-z * I) ^ (2 * k + 0) / (↑(2 * k + 0)! : ℂ) - (z * I) ^ (2 * k + 0) / (↑(2 * k + 0)! : ℂ)) * I / 2 +
      ((-z * I) ^ (2 * k + (↑1 : ℕ)) / (↑(2 * k + (↑1 : ℕ))! : ℂ) -
            (z * I) ^ (2 * k + (↑1 : ℕ)) / (↑(2 * k + (↑1 : ℕ))! : ℂ)) *
          I /
        2
h₁ :
  (z * I) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ) / I =
    ((-z * I) ^ (2 * k + 0) / (↑(2 * k + 0)! : ℂ) - (z * I) ^ (2 * k + 0) / (↑(2 * k + 0)! : ℂ)) * I / 2 +
      ((-z * I) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ) - (z * I) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ)) * I / 2
h₂ :
  (z * I) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ) / I =
    ((-z * I) ^ (2 * k) / (↑(2 * k)! : ℂ) - (z * I) ^ (2 * k) / (↑(2 * k)! : ℂ)) * I / 2 +
      ((-z * I) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ) - (z * I) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ)) * I / 2
h₃ :
  (z * I) ^ (2 * k) * (z * I) / (↑(2 * k + 1)! : ℂ) / I =
    ((-z * I) ^ (2 * k) / (↑(2 * k)! : ℂ) - (z * I) ^ (2 * k) / (↑(2 * k)! : ℂ)) * I / 2 +
      ((-z * I) ^ (2 * k) * (-z * I) / (↑(2 * k + 1)! : ℂ) - (z * I) ^ (2 * k) * (z * I) / (↑(2 * k + 1)! : ℂ)) * I / 2
h₄ :
  HPow.hPow (β := ℕ) (z * I) 2 ^ k * (z * I) / (↑(2 * k + 1)! : ℂ) / I =
    (HPow.hPow (β := ℕ) (-z * I) 2 ^ k / (↑(2 * k)! : ℂ) - HPow.hPow (β := ℕ) (z * I) 2 ^ k / (↑(2 * k)! : ℂ)) * I / 2 +
      (HPow.hPow (β := ℕ) (-z * I) 2 ^ k * (-z * I) / (↑(2 * k + 1)! : ℂ) -
            HPow.hPow (β := ℕ) (z * I) 2 ^ k * (z * I) / (↑(2 * k + 1)! : ℂ)) *
          I /
        2
h₅ :
  HPow.hPow (β := ℕ) z 2 ^ k * HPow.hPow (β := ℕ) I 2 ^ k * (z * I) / (↑(2 * k + 1)! : ℂ) / I =
    (HPow.hPow (β := ℕ) (-z) 2 ^ k * HPow.hPow (β := ℕ) I 2 ^ k / (↑(2 * k)! : ℂ) -
            HPow.hPow (β := ℕ) z 2 ^ k * HPow.hPow (β := ℕ) I 2 ^ k / (↑(2 * k)! : ℂ)) *
          I /
        2 +
      (HPow.hPow (β := ℕ) (-z) 2 ^ k * HPow.hPow (β := ℕ) I 2 ^ k * (-z * I) / (↑(2 * k + 1)! : ℂ) -
            HPow.hPow (β := ℕ) z 2 ^ k * HPow.hPow (β := ℕ) I 2 ^ k * (z * I) / (↑(2 * k + 1)! : ℂ)) *
          I /
        2
⊢ (z * I) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ) / I =
    ((-z * I) ^ (2 * k + (↑0 : ℕ)) / (↑(2 * k + (↑0 : ℕ))! : ℂ) -
            (z * I) ^ (2 * k + (↑0 : ℕ)) / (↑(2 * k + (↑0 : ℕ))! : ℂ)) *
          I /
        2 +
      ((-z * I) ^ (2 * k + (↑1 : ℕ)) / (↑(2 * k + (↑1 : ℕ))! : ℂ) -
            (z * I) ^ (2 * k + (↑1 : ℕ)) / (↑(2 * k + (↑1 : ℕ))! : ℂ)) *
          I /
        2
have h₆ : HPow.hPow (β := ℕ) z 2 ^ k * HPow.hPow (β := ℕ) I 2 ^ k * (z * I) / (↑(2 * k + 1)! : ℂ) / I =
  (HPow.hPow (β := ℕ) z 2 ^ k * HPow.hPow (β := ℕ) I 2 ^ k / (↑(2 * k)! : ℂ) -
          HPow.hPow (β := ℕ) z 2 ^ k * HPow.hPow (β := ℕ) I 2 ^ k / (↑(2 * k)! : ℂ)) *
        I /
      2 +
    (HPow.hPow (β := ℕ) z 2 ^ k * HPow.hPow (β := ℕ) I 2 ^ k * (-z * I) / (↑(2 * k + 1)! : ℂ) -
          HPow.hPow (β := ℕ) z 2 ^ k * HPow.hPow (β := ℕ) I 2 ^ k * (z * I) / (↑(2 * k + 1)! : ℂ)) *
        I /
      2
Tactic: simp_rw [Fin.val_zero, Fin.val_one, add_zero, pow_succ, pow_mul, mul_pow, neg_sq, sub_self,
    zero_mul, zero_div, zero_add, neg_mul, mul_neg, neg_div, ← neg_add', ← two_mul,
    neg_mul, neg_div, mul_assoc, mul_div_cancel_left₀ _ (two_ne_zero : (2 : ℂ) ≠ 0), Complex.div_I]