-- 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 : ℕ))! : ℂ)) /
        2)
    ((NormedSpace.exp (z * I) + NormedSpace.exp (-z * I)) / 2)
k : ℕ
h :
  (z * I) ^ (2 * k) / (↑(2 * k)! : ℂ) =
    ((z * I) ^ (2 * k + 0) / (↑(2 * k + 0)! : ℂ) + (-z * I) ^ (2 * k + 0) / (↑(2 * k + 0)! : ℂ)) / 2 +
      ((z * I) ^ (2 * k + (↑1 : ℕ)) / (↑(2 * k + (↑1 : ℕ))! : ℂ) +
          (-z * I) ^ (2 * k + (↑1 : ℕ)) / (↑(2 * k + (↑1 : ℕ))! : ℂ)) /
        2
h₁ :
  (z * I) ^ (2 * k) / (↑(2 * k)! : ℂ) =
    ((z * I) ^ (2 * k + 0) / (↑(2 * k + 0)! : ℂ) + (-z * I) ^ (2 * k + 0) / (↑(2 * k + 0)! : ℂ)) / 2 +
      ((z * I) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ) + (-z * I) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ)) / 2
h₂ :
  (z * I) ^ (2 * k) / (↑(2 * k)! : ℂ) =
    ((z * I) ^ (2 * k) / (↑(2 * k)! : ℂ) + (-z * I) ^ (2 * k) / (↑(2 * k)! : ℂ)) / 2 +
      ((z * I) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ) + (-z * I) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ)) / 2
h₃ :
  (z * I) ^ (2 * k) / (↑(2 * k)! : ℂ) =
    ((z * I) ^ (2 * k) / (↑(2 * k)! : ℂ) + (-z * I) ^ (2 * k) / (↑(2 * k)! : ℂ)) / 2 +
      ((z * I) ^ (2 * k) * (z * I) / (↑(2 * k + 1)! : ℂ) + (-z * I) ^ (2 * k) * (-z * I) / (↑(2 * k + 1)! : ℂ)) / 2
h₄ :
  HPow.hPow (β := ℕ) (z * I) 2 ^ k / (↑(2 * k)! : ℂ) =
    (HPow.hPow (β := ℕ) (z * I) 2 ^ k / (↑(2 * k)! : ℂ) + HPow.hPow (β := ℕ) (-z * I) 2 ^ k / (↑(2 * k)! : ℂ)) / 2 +
      (HPow.hPow (β := ℕ) (z * I) 2 ^ k * (z * I) / (↑(2 * k + 1)! : ℂ) +
          HPow.hPow (β := ℕ) (-z * I) 2 ^ k * (-z * I) / (↑(2 * k + 1)! : ℂ)) /
        2
h₅ :
  HPow.hPow (β := ℕ) z 2 ^ k * HPow.hPow (β := ℕ) I 2 ^ k / (↑(2 * k)! : ℂ) =
    (HPow.hPow (β := ℕ) z 2 ^ k * HPow.hPow (β := ℕ) I 2 ^ k / (↑(2 * k)! : ℂ) +
          HPow.hPow (β := ℕ) (-z) 2 ^ k * HPow.hPow (β := ℕ) I 2 ^ k / (↑(2 * k)! : ℂ)) /
        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)! : ℂ)) /
        2
⊢ (z * I) ^ (2 * k) / (↑(2 * k)! : ℂ) =
    ((z * I) ^ (2 * k + (↑0 : ℕ)) / (↑(2 * k + (↑0 : ℕ))! : ℂ) +
          (-z * I) ^ (2 * k + (↑0 : ℕ)) / (↑(2 * k + (↑0 : ℕ))! : ℂ)) /
        2 +
      ((z * I) ^ (2 * k + (↑1 : ℕ)) / (↑(2 * k + (↑1 : ℕ))! : ℂ) +
          (-z * I) ^ (2 * k + (↑1 : ℕ)) / (↑(2 * k + (↑1 : ℕ))! : ℂ)) /
        2
have h₆ : HPow.hPow (β := ℕ) z 2 ^ k * HPow.hPow (β := ℕ) I 2 ^ k / (↑(2 * k)! : ℂ) =
  (HPow.hPow (β := ℕ) z 2 ^ k * HPow.hPow (β := ℕ) I 2 ^ k / (↑(2 * k)! : ℂ) +
        HPow.hPow (β := ℕ) z 2 ^ k * HPow.hPow (β := ℕ) I 2 ^ k / (↑(2 * k)! : ℂ)) /
      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)! : ℂ)) /
      2
Tactic: simp_rw [Fin.val_zero, Fin.val_one, add_zero, pow_succ, pow_mul, mul_pow, neg_sq, ← two_mul,
    neg_mul, mul_neg, neg_div, add_neg_cancel, zero_div, add_zero,
    mul_div_cancel_left₀ _ (two_ne_zero : (2 : ℂ) ≠ 0)]