-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev.lean
theorem T_complex_cos (n : ℤ) : (T ℂ n).eval (cos θ) = cos (n * θ)

Proof state:
case zero
θ : ℂ
⊢ eval (cos θ) (T ℂ 0) = cos (↑0 * θ)

Tactic:
simp

Result:
no goals

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

Tactic:
simp only [T_sub_one, eval_sub, eval_mul, eval_X, eval_ofNat, ih1, ih2, sub_eq_iff_eq_add',
  cos_add_cos]

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

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

Tactic:
push_cast

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

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

Tactic:
push_cast

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

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

Tactic:
simp

Result:
no goals

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

Tactic:
ring_nf

Result:
no goals

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

Tactic:
ring_nf

Result:
no goals

Proof state:
θ : ℂ
n : ℤ
⊢ eval (cos θ) (T ℂ n) = cos (↑n * θ)

Tactic:
induction n using Polynomial.Chebyshev.induct with
| zero => simp
| one => simp
| add_two n ih1 ih2 =>
  simp only [T_add_two, eval_sub, eval_mul, eval_X, eval_ofNat, ih1, ih2, sub_eq_iff_eq_add,
    cos_add_cos]
  push_cast
  ring_nf
| neg_add_one n ih1 ih2 =>
  simp only [T_sub_one, eval_sub, eval_mul, eval_X, eval_ofNat, ih1, ih2, sub_eq_iff_eq_add',
    cos_add_cos]
  push_cast
  ring_nf

Result:
no goals

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

Tactic:
simp only [T_add_two, eval_sub, eval_mul, eval_X, eval_ofNat, ih1, ih2, sub_eq_iff_eq_add,
  cos_add_cos]

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