-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem T_eval_neg_one (n : ℤ) : (T R n).eval (-1) = n.negOnePow

Proof state:
case zero
R : Type u_1
inst✝ : CommRing R
⊢ eval (-1) (T R 0) = ↑↑(Int.negOnePow 0)

Tactic:
simp

Result:
no goals

Proof state:
case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval (-1) (T R (↑n + 1)) = ↑↑(↑n + 1).negOnePow
ih2 : eval (-1) (T R ↑n) = ↑↑(↑n).negOnePow
⊢ 2 * ↑↑(↑n).negOnePow - ↑↑(↑n).negOnePow = ↑↑(↑n).negOnePow

Tactic:
ring

Result:
no goals

Proof state:
case one
R : Type u_1
inst✝ : CommRing R
⊢ eval (-1) (T R 1) = ↑↑(Int.negOnePow 1)

Tactic:
simp

Result:
no goals

Proof state:
case neg_add_one
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval (-1) (T R (-↑n)) = ↑↑(-↑n).negOnePow
ih2 : eval (-1) (T R (-↑n + 1)) = ↑↑(-↑n + 1).negOnePow
⊢ eval (-1) (T R (-↑n - 1)) = ↑↑(-↑n - 1).negOnePow

Tactic:
simp only [T_sub_one, eval_sub, eval_mul, eval_ofNat, eval_X, mul_neg, mul_one, ih1, neg_mul,
  ih2, Int.negOnePow_add, Int.negOnePow_one, Units.val_neg, Int.cast_neg, sub_neg_eq_add,
  Int.negOnePow_sub]

Result:
case neg_add_one
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval (-1) (T R (-↑n)) = ↑↑(-↑n).negOnePow
ih2 : eval (-1) (T R (-↑n + 1)) = ↑↑(-↑n + 1).negOnePow
⊢ -(2 * ↑↑(-↑n).negOnePow) + ↑↑(-↑n).negOnePow = -↑↑(-↑n).negOnePow

Proof state:
case neg_add_one
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval (-1) (T R (-↑n)) = ↑↑(-↑n).negOnePow
ih2 : eval (-1) (T R (-↑n + 1)) = ↑↑(-↑n + 1).negOnePow
⊢ -(2 * ↑↑(-↑n).negOnePow) + ↑↑(-↑n).negOnePow = -↑↑(-↑n).negOnePow

Tactic:
ring

Result:
no goals

Proof state:
case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval (-1) (T R (↑n + 1)) = ↑↑(↑n + 1).negOnePow
ih2 : eval (-1) (T R ↑n) = ↑↑(↑n).negOnePow
⊢ eval (-1) (T R (↑n + 2)) = ↑↑(↑n + 2).negOnePow

Tactic:
simp only [T_add_two, eval_sub, eval_mul, eval_ofNat, eval_X, mul_neg, mul_one, ih1,
  Int.negOnePow_add, Int.negOnePow_one, Units.val_neg, Int.cast_neg, neg_mul, neg_neg, ih2,
  Int.negOnePow_def 2]

Result:
case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval (-1) (T R (↑n + 1)) = ↑↑(↑n + 1).negOnePow
ih2 : eval (-1) (T R ↑n) = ↑↑(↑n).negOnePow
⊢ 2 * ↑↑(↑n).negOnePow - ↑↑(↑n).negOnePow = ↑↑((↑n).negOnePow * (-1) ^ 2)

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ eval (-1) (T R n) = ↑↑n.negOnePow

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_ofNat, eval_X, mul_neg, mul_one, ih1,
    Int.negOnePow_add, Int.negOnePow_one, Units.val_neg, Int.cast_neg, neg_mul, neg_neg, ih2,
    Int.negOnePow_def 2]
  norm_cast
  norm_num
  ring
| neg_add_one n ih1 ih2 =>
  simp only [T_sub_one, eval_sub, eval_mul, eval_ofNat, eval_X, mul_neg, mul_one, ih1, neg_mul,
    ih2, Int.negOnePow_add, Int.negOnePow_one, Units.val_neg, Int.cast_neg, sub_neg_eq_add,
    Int.negOnePow_sub]
  ring

Result:
no goals

Proof state:
case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval (-1) (T R (↑n + 1)) = ↑↑(↑n + 1).negOnePow
ih2 : eval (-1) (T R ↑n) = ↑↑(↑n).negOnePow
⊢ 2 * ↑↑(↑n).negOnePow - ↑↑(↑n).negOnePow = ↑↑((↑n).negOnePow * (-1) ^ 2)

Tactic:
norm_num

Result:
case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : eval (-1) (T R (↑n + 1)) = ↑↑(↑n + 1).negOnePow
ih2 : eval (-1) (T R ↑n) = ↑↑(↑n).negOnePow
⊢ 2 * ↑↑(↑n).negOnePow - ↑↑(↑n).negOnePow = ↑↑(↑n).negOnePow