-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Series.lean
theorem Complex.hasSum_sin' (z : ℂ) :
    HasSum (fun n : ℕ => (z * Complex.I) ^ (2 * n + 1) / ↑(2 * n + 1)! / Complex.I)
      (Complex.sin z)

Proof state:
z : ℂ
⊢ HasSum (fun n => (z * I) ^ (2 * n + 1) / ↑(2 * n + 1)! / I)
    ((NormedSpace.exp ℂ (-z * I) - NormedSpace.exp ℂ (z * I)) * I / 2)

Tactic:
have := (((expSeries_div_hasSum_exp ℂ (-z * Complex.I)).sub
  (expSeries_div_hasSum_exp ℂ (z * Complex.I))).mul_right Complex.I).div_const 2

Result:
z : ℂ
this :
  HasSum (fun i => ((-z * I) ^ i / ↑i ! - (z * I) ^ i / ↑i !) * 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)

Proof state:
z : ℂ
this :
  HasSum (fun i => ((-z * I) ^ i / ↑i ! - (z * I) ^ i / ↑i !) * 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)

Tactic:
replace := (Nat.divModEquiv 2).symm.hasSum_iff.mpr this

Result:
z : ℂ
this :
  HasSum ((fun i => ((-z * I) ^ i / ↑i ! - (z * I) ^ i / ↑i !) * I / 2) ∘ ⇑(Nat.divModEquiv 2).symm)
    ((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)

Proof state:
z : ℂ
this :
  HasSum
    (fun x =>
      ((-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 =>
      ((-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:
dsimp only

Result:
z : ℂ
this :
  HasSum
    (fun x =>
      ((-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 => ((-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)

Proof state:
z : ℂ
this :
  HasSum ((fun i => ((-z * I) ^ i / ↑i ! - (z * I) ^ i / ↑i !) * I / 2) ∘ ⇑(Nat.divModEquiv 2).symm)
    ((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)

Tactic:
dsimp [Function.comp_def] at this

Result:
z : ℂ
this :
  HasSum
    (fun x =>
      ((-z * I) ^ (x.1 * 2 + ↑x.2) / ↑(x.1 * 2 + ↑x.2)! - (z * I) ^ (x.1 * 2 + ↑x.2) / ↑(x.1 * 2 + ↑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)

Proof state:
z : ℂ
this :
  HasSum
    (fun x =>
      ((-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)

Tactic:
refine this.prod_fiberwise fun k => ?_

Result:
z : ℂ
this :
  HasSum
    (fun x =>
      ((-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 =>
      ((-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)

Proof state:
z : ℂ
this :
  HasSum
    (fun x =>
      ((-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 => ((-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:
convert hasSum_fintype (_ : Fin 2 → ℂ) using 1

Result:
case h.e'_6
z : ℂ
this :
  HasSum
    (fun x =>
      ((-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

Proof state:
case h.e'_6
z : ℂ
this :
  HasSum
    (fun x =>
      ((-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

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]

Result:
no goals

Proof state:
case h.e'_6
z : ℂ
this :
  HasSum
    (fun x =>
      ((-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

Tactic:
rw [Fin.sum_univ_two]

Result:
case h.e'_6
z : ℂ
this :
  HasSum
    (fun x =>
      ((-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

Proof state:
z : ℂ
⊢ HasSum (fun n => (z * I) ^ (2 * n + 1) / ↑(2 * n + 1)! / I) (sin z)

Tactic:
rw [Complex.sin, Complex.exp_eq_exp_ℂ]

Result:
z : ℂ
⊢ HasSum (fun n => (z * I) ^ (2 * n + 1) / ↑(2 * n + 1)! / I)
    ((NormedSpace.exp ℂ (-z * I) - NormedSpace.exp ℂ (z * I)) * I / 2)

Proof state:
z : ℂ
this :
  HasSum
    (fun x =>
      ((-z * I) ^ (x.1 * 2 + ↑x.2) / ↑(x.1 * 2 + ↑x.2)! - (z * I) ^ (x.1 * 2 + ↑x.2) / ↑(x.1 * 2 + ↑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)

Tactic:
simp_rw [← mul_comm 2 _] at this

Result:
z : ℂ
this :
  HasSum
    (fun x =>
      ((-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)