awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
⊢ HasSum (fun (n : ℕ) ↦ (z * I) ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ) / I)
    ((NormedSpace.exp (-z * I) - NormedSpace.exp (z * I)) * I / 2)
have refine : ∀ (k : ℕ),
  HasSum
    (fun (c : Fin 2) ↦
      ((-z * I) ^ (2 * (k, c).1 + (↑(k, c).2 : ℕ)) / (↑(2 * (k, c).1 + (↑(k, c).2 : ℕ))! : ℂ) -
            (z * I) ^ (2 * (k, c).1 + (↑(k, c).2 : ℕ)) / (↑(2 * (k, c).1 + (↑(k, c).2 : ℕ))! : ℂ)) *
          I /
        2)
    ((z * I) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ) / I)
Tactic: refine this.prod_fiberwise fun k => ?_
-- 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 : ℕ
⊢ HasSum
    (fun (c : Fin 2) ↦
      ((-z * I) ^ (2 * (k, c).1 + (↑(k, c).2 : ℕ)) / (↑(2 * (k, c).1 + (↑(k, c).2 : ℕ))! : ℂ) -
            (z * I) ^ (2 * (k, c).1 + (↑(k, c).2 : ℕ)) / (↑(2 * (k, c).1 + (↑(k, c).2 : ℕ))! : ℂ)) *
          I /
        2)
    ((z * I) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ) / I)
have dsimp : HasSum
  (fun (c : Fin 2) ↦
    ((-z * I) ^ (2 * k + (↑c : ℕ)) / (↑(2 * k + (↑c : ℕ))! : ℂ) -
          (z * I) ^ (2 * k + (↑c : ℕ)) / (↑(2 * k + (↑c : ℕ))! : ℂ)) *
        I /
      2)
  ((z * I) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ) / I)
Tactic: dsimp only
-- 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 : ℕ
⊢ HasSum
    (fun (c : Fin 2) ↦
      ((-z * I) ^ (2 * k + (↑c : ℕ)) / (↑(2 * k + (↑c : ℕ))! : ℂ) -
            (z * I) ^ (2 * k + (↑c : ℕ)) / (↑(2 * k + (↑c : ℕ))! : ℂ)) *
          I /
        2)
    ((z * I) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ) / I)
have h : (z * I) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ) / I =
  ∑ b : Fin 2,
    ((-z * I) ^ (2 * k + (↑b : ℕ)) / (↑(2 * k + (↑b : ℕ))! : ℂ) -
          (z * I) ^ (2 * k + (↑b : ℕ)) / (↑(2 * k + (↑b : ℕ))! : ℂ)) *
        I /
      2
Tactic: convert! hasSum_fintype (_ : Fin 2 → ℂ) using 1
-- 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 : ℕ
⊢ (z * I) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ) / I =
    ∑ b : Fin 2,
      ((-z * I) ^ (2 * k + (↑b : ℕ)) / (↑(2 * k + (↑b : ℕ))! : ℂ) -
            (z * I) ^ (2 * k + (↑b : ℕ)) / (↑(2 * k + (↑b : ℕ))! : ℂ)) *
          I /
        2
have 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
Tactic: rw [Fin.sum_univ_two]
-- 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 : ℕ
⊢ (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 : (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
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]
-- 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
⊢ (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₁ : (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
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]
-- 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
⊢ (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₂ : (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
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]
-- 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
⊢ (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₃ : (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
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]
-- 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
⊢ (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 * 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
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]
-- 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
⊢ (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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Series (goal)
Goal:
z : ℂ
⊢ HasSum (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * z ^ (2 * n) / (↑(2 * n)! : ℂ)) (cos z)
have h : Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * z ^ (2 * n) / (↑(2 * n)! : ℂ)) fun (n : ℕ) ↦
  (z * I) ^ (2 * n) / (↑(2 * n)! : ℂ)
Tactic: convert! Complex.hasSum_cos' z using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Series (goal)
Goal:
z : ℂ
⊢ Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * z ^ (2 * n) / (↑(2 * n)! : ℂ)) fun (n : ℕ) ↦
    (z * I) ^ (2 * n) / (↑(2 * n)! : ℂ)
have h : Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * z ^ (2 * n) / (↑(2 * n)! : ℂ)) fun (n : ℕ) ↦
  z ^ (2 * n) * I ^ (2 * n) / (↑(2 * n)! : ℂ)
Tactic: simp_rw [mul_pow, pow_mul, Complex.I_sq, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Series (goal)
Goal:
z : ℂ
h :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * z ^ (2 * n) / (↑(2 * n)! : ℂ)) fun (n : ℕ) ↦
    z ^ (2 * n) * I ^ (2 * n) / (↑(2 * n)! : ℂ)
⊢ Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * z ^ (2 * n) / (↑(2 * n)! : ℂ)) fun (n : ℕ) ↦
    (z * I) ^ (2 * n) / (↑(2 * n)! : ℂ)
have h₁ : Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * HPow.hPow (β := ℕ) z 2 ^ n / (↑(2 * n)! : ℂ)) fun (n : ℕ) ↦
  HPow.hPow (β := ℕ) z 2 ^ n * HPow.hPow (β := ℕ) I 2 ^ n / (↑(2 * n)! : ℂ)
Tactic: simp_rw [mul_pow, pow_mul, Complex.I_sq, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Series (goal)
Goal:
z : ℂ
h :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * z ^ (2 * n) / (↑(2 * n)! : ℂ)) fun (n : ℕ) ↦
    z ^ (2 * n) * I ^ (2 * n) / (↑(2 * n)! : ℂ)
h₁ :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * HPow.hPow (β := ℕ) z 2 ^ n / (↑(2 * n)! : ℂ)) fun (n : ℕ) ↦
    HPow.hPow (β := ℕ) z 2 ^ n * HPow.hPow (β := ℕ) I 2 ^ n / (↑(2 * n)! : ℂ)
⊢ Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * z ^ (2 * n) / (↑(2 * n)! : ℂ)) fun (n : ℕ) ↦
    (z * I) ^ (2 * n) / (↑(2 * n)! : ℂ)
have h₂ : Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * HPow.hPow (β := ℕ) z 2 ^ n / (↑(2 * n)! : ℂ)) fun (n : ℕ) ↦
  HPow.hPow (β := ℕ) z 2 ^ n * HPow.hPow (α := ℂ) (-1) n / (↑(2 * n)! : ℂ)
Tactic: simp_rw [mul_pow, pow_mul, Complex.I_sq, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Series (goal)
Goal:
z : ℂ
⊢ HasSum (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * z ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ)) (sin z)
have h : Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * z ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ)) fun (n : ℕ) ↦
  (z * I) ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ) / I
Tactic: convert! Complex.hasSum_sin' z using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Series (goal)
Goal:
z : ℂ
⊢ Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * z ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ)) fun (n : ℕ) ↦
    (z * I) ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ) / I
have h : Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * z ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ)) fun (n : ℕ) ↦
  z ^ (2 * n + 1) * I ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ) / I
Tactic: 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Series (goal)
Goal:
z : ℂ
h :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * z ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ)) fun (n : ℕ) ↦
    z ^ (2 * n + 1) * I ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ) / I
⊢ Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * z ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ)) fun (n : ℕ) ↦
    (z * I) ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ) / I
have h₁ : Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * (z ^ (2 * n) * z) / (↑(2 * n + 1)! : ℂ)) fun (n : ℕ) ↦
  z ^ (2 * n) * z * (I ^ (2 * n) * I) / (↑(2 * n + 1)! : ℂ) / I
Tactic: 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Series (goal)
Goal:
z : ℂ
h :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * z ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ)) fun (n : ℕ) ↦
    z ^ (2 * n + 1) * I ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ) / I
h₁ :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * (z ^ (2 * n) * z) / (↑(2 * n + 1)! : ℂ)) fun (n : ℕ) ↦
    z ^ (2 * n) * z * (I ^ (2 * n) * I) / (↑(2 * n + 1)! : ℂ) / I
⊢ Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * z ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ)) fun (n : ℕ) ↦
    (z * I) ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ) / I
have h₂ : Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * (HPow.hPow (β := ℕ) z 2 ^ n * z) / (↑(2 * n + 1)! : ℂ))
  fun (n : ℕ) ↦ HPow.hPow (β := ℕ) z 2 ^ n * z * (HPow.hPow (β := ℕ) I 2 ^ n * I) / (↑(2 * n + 1)! : ℂ) / I
Tactic: 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Series (goal)
Goal:
z : ℂ
h :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * z ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ)) fun (n : ℕ) ↦
    z ^ (2 * n + 1) * I ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ) / I
h₁ :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * (z ^ (2 * n) * z) / (↑(2 * n + 1)! : ℂ)) fun (n : ℕ) ↦
    z ^ (2 * n) * z * (I ^ (2 * n) * I) / (↑(2 * n + 1)! : ℂ) / I
h₂ :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * (HPow.hPow (β := ℕ) z 2 ^ n * z) / (↑(2 * n + 1)! : ℂ))
    fun (n : ℕ) ↦ HPow.hPow (β := ℕ) z 2 ^ n * z * (HPow.hPow (β := ℕ) I 2 ^ n * I) / (↑(2 * n + 1)! : ℂ) / I
⊢ Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * z ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ)) fun (n : ℕ) ↦
    (z * I) ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ) / I
have h₃ : Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * (HPow.hPow (β := ℕ) z 2 ^ n * z) / (↑(2 * n + 1)! : ℂ))
  fun (n : ℕ) ↦ HPow.hPow (β := ℕ) z 2 ^ n * z * (HPow.hPow (α := ℂ) (-1) n * I) / (↑(2 * n + 1)! : ℂ) / I
Tactic: 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]