-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev.lean
theorem U_complex_cos (n : ℤ) : (U ℂ n).eval (cos θ) * sin θ = sin ((n + 1) * θ)

Proof state:
case add_two
θ : ℂ
n : ℕ
ih1 : eval (cos θ) (U ℂ (↑n + 1)) * sin θ = sin ((↑(↑n + 1) + 1) * θ)
ih2 : eval (cos θ) (U ℂ ↑n) * sin θ = sin ((↑↑n + 1) * θ)
⊢ 2 * (cos θ * sin ((↑n + 1 + 1) * θ)) =
    2 * (sin (((↑n + 2 + 1) * θ + (↑n + 1) * θ) / 2) * cos (((↑n + 2 + 1) * θ - (↑n + 1) * θ) / 2))

Tactic:
ring_nf

Result:
no goals

Proof state:
case neg_add_one
θ : ℂ
n : ℕ
ih1 : eval (cos θ) (U ℂ (-↑n)) * sin θ = sin ((↑(-↑n) + 1) * θ)
ih2 : eval (cos θ) (U ℂ (-↑n + 1)) * sin θ = sin ((↑(-↑n + 1) + 1) * θ)
⊢ 2 * (cos θ * sin ((-↑n + 1) * θ)) =
    2 * (sin (((-↑n + 1 + 1) * θ + (-↑n - 1 + 1) * θ) / 2) * cos (((-↑n + 1 + 1) * θ - (-↑n - 1 + 1) * θ) / 2))

Tactic:
ring_nf

Result:
no goals

Proof state:
case one
θ : ℂ
⊢ 2 * cos θ * sin θ = 2 * sin θ * cos θ

Tactic:
ring

Result:
no goals

Proof state:
case add_two
θ : ℂ
n : ℕ
ih1 : eval (cos θ) (U ℂ (↑n + 1)) * sin θ = sin ((↑(↑n + 1) + 1) * θ)
ih2 : eval (cos θ) (U ℂ ↑n) * sin θ = sin ((↑↑n + 1) * θ)
⊢ eval (cos θ) (U ℂ (↑n + 2)) * sin θ = sin ((↑(↑n + 2) + 1) * θ)

Tactic:
simp only [U_add_two, add_sub_cancel_right, eval_sub, eval_mul, eval_X, eval_ofNat, sub_mul,
  mul_assoc, ih1, ih2, sub_eq_iff_eq_add, sin_add_sin]

Result:
case add_two
θ : ℂ
n : ℕ
ih1 : eval (cos θ) (U ℂ (↑n + 1)) * sin θ = sin ((↑(↑n + 1) + 1) * θ)
ih2 : eval (cos θ) (U ℂ ↑n) * sin θ = sin ((↑↑n + 1) * θ)
⊢ 2 * (cos θ * sin ((↑(↑n + 1) + 1) * θ)) =
    2 * (sin (((↑(↑n + 2) + 1) * θ + (↑↑n + 1) * θ) / 2) * cos (((↑(↑n + 2) + 1) * θ - (↑↑n + 1) * θ) / 2))

Proof state:
case add_two
θ : ℂ
n : ℕ
ih1 : eval (cos θ) (U ℂ (↑n + 1)) * sin θ = sin ((↑(↑n + 1) + 1) * θ)
ih2 : eval (cos θ) (U ℂ ↑n) * sin θ = sin ((↑↑n + 1) * θ)
⊢ 2 * (cos θ * sin ((↑(↑n + 1) + 1) * θ)) =
    2 * (sin (((↑(↑n + 2) + 1) * θ + (↑↑n + 1) * θ) / 2) * cos (((↑(↑n + 2) + 1) * θ - (↑↑n + 1) * θ) / 2))

Tactic:
push_cast

Result:
case add_two
θ : ℂ
n : ℕ
ih1 : eval (cos θ) (U ℂ (↑n + 1)) * sin θ = sin ((↑(↑n + 1) + 1) * θ)
ih2 : eval (cos θ) (U ℂ ↑n) * sin θ = sin ((↑↑n + 1) * θ)
⊢ 2 * (cos θ * sin ((↑n + 1 + 1) * θ)) =
    2 * (sin (((↑n + 2 + 1) * θ + (↑n + 1) * θ) / 2) * cos (((↑n + 2 + 1) * θ - (↑n + 1) * θ) / 2))

Proof state:
case one
θ : ℂ
⊢ eval (cos θ) (U ℂ 1) * sin θ = sin ((↑1 + 1) * θ)

Tactic:
simp [one_add_one_eq_two, sin_two_mul]

Result:
case one
θ : ℂ
⊢ 2 * cos θ * sin θ = 2 * sin θ * cos θ

Proof state:
case neg_add_one
θ : ℂ
n : ℕ
ih1 : eval (cos θ) (U ℂ (-↑n)) * sin θ = sin ((↑(-↑n) + 1) * θ)
ih2 : eval (cos θ) (U ℂ (-↑n + 1)) * sin θ = sin ((↑(-↑n + 1) + 1) * θ)
⊢ eval (cos θ) (U ℂ (-↑n - 1)) * sin θ = sin ((↑(-↑n - 1) + 1) * θ)

Tactic:
simp only [U_sub_one, add_sub_cancel_right, eval_sub, eval_mul, eval_X, eval_ofNat, sub_mul,
  mul_assoc, ih1, ih2, sub_eq_iff_eq_add', sin_add_sin]

Result:
case neg_add_one
θ : ℂ
n : ℕ
ih1 : eval (cos θ) (U ℂ (-↑n)) * sin θ = sin ((↑(-↑n) + 1) * θ)
ih2 : eval (cos θ) (U ℂ (-↑n + 1)) * sin θ = sin ((↑(-↑n + 1) + 1) * θ)
⊢ 2 * (cos θ * sin ((↑(-↑n) + 1) * θ)) =
    2 *
      (sin (((↑(-↑n + 1) + 1) * θ + (↑(-↑n - 1) + 1) * θ) / 2) *
        cos (((↑(-↑n + 1) + 1) * θ - (↑(-↑n - 1) + 1) * θ) / 2))

Proof state:
case zero
θ : ℂ
⊢ eval (cos θ) (U ℂ 0) * sin θ = sin ((↑0 + 1) * θ)

Tactic:
simp

Result:
no goals

Proof state:
θ : ℂ
n : ℤ
⊢ eval (cos θ) (U ℂ n) * sin θ = sin ((↑n + 1) * θ)

Tactic:
induction n using Polynomial.Chebyshev.induct with
| zero => simp
| one => simp [one_add_one_eq_two, sin_two_mul]; ring
| add_two n ih1 ih2 =>
  simp only [U_add_two, add_sub_cancel_right, eval_sub, eval_mul, eval_X, eval_ofNat, sub_mul,
    mul_assoc, ih1, ih2, sub_eq_iff_eq_add, sin_add_sin]
  push_cast
  ring_nf
| neg_add_one n ih1 ih2 =>
  simp only [U_sub_one, add_sub_cancel_right, eval_sub, eval_mul, eval_X, eval_ofNat, sub_mul,
    mul_assoc, ih1, ih2, sub_eq_iff_eq_add', sin_add_sin]
  push_cast
  ring_nf

Result:
no goals

Proof state:
case neg_add_one
θ : ℂ
n : ℕ
ih1 : eval (cos θ) (U ℂ (-↑n)) * sin θ = sin ((↑(-↑n) + 1) * θ)
ih2 : eval (cos θ) (U ℂ (-↑n + 1)) * sin θ = sin ((↑(-↑n + 1) + 1) * θ)
⊢ 2 * (cos θ * sin ((↑(-↑n) + 1) * θ)) =
    2 *
      (sin (((↑(-↑n + 1) + 1) * θ + (↑(-↑n - 1) + 1) * θ) / 2) *
        cos (((↑(-↑n + 1) + 1) * θ - (↑(-↑n - 1) + 1) * θ) / 2))

Tactic:
push_cast

Result:
case neg_add_one
θ : ℂ
n : ℕ
ih1 : eval (cos θ) (U ℂ (-↑n)) * sin θ = sin ((↑(-↑n) + 1) * θ)
ih2 : eval (cos θ) (U ℂ (-↑n + 1)) * sin θ = sin ((↑(-↑n + 1) + 1) * θ)
⊢ 2 * (cos θ * sin ((-↑n + 1) * θ)) =
    2 * (sin (((-↑n + 1 + 1) * θ + (-↑n - 1 + 1) * θ) / 2) * cos (((-↑n + 1 + 1) * θ - (-↑n - 1 + 1) * θ) / 2))