-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem C_eval_neg_two (n : ℤ) : (C R n).eval (-2) = 2 * n.negOnePow

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

Tactic:
norm_num

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

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

Tactic:
simp only [C_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 (-2) (C R (-↑n)) = 2 * ↑↑(-↑n).negOnePow
ih2 : eval (-2) (C R (-↑n + 1)) = 2 * ↑↑(-↑n + 1).negOnePow
⊢ -(2 * (2 * ↑↑(-↑n).negOnePow)) + 2 * ↑↑(-↑n).negOnePow = -(2 * ↑↑(-↑n).negOnePow)

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

Tactic:
simp

Result:
no goals

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

Tactic:
norm_cast

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

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

Tactic:
simp only [C_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 (-2) (C R (↑n + 1)) = 2 * ↑↑(↑n + 1).negOnePow
ih2 : eval (-2) (C R ↑n) = 2 * ↑↑(↑n).negOnePow
⊢ 2 * (2 * ↑↑(↑n).negOnePow) - 2 * ↑↑(↑n).negOnePow = 2 * ↑↑((↑n).negOnePow * (-1) ^ 2)

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

Tactic:
ring

Result:
no goals

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

Tactic:
induction n using Polynomial.Chebyshev.induct with
| zero => simp
| one => simp
| add_two n ih1 ih2 =>
  simp only [C_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 [C_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 one
R : Type u_1
inst✝ : CommRing R
⊢ eval (-2) (C R 1) = 2 * ↑↑(Int.negOnePow 1)

Tactic:
simp

Result:
no goals

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

Tactic:
ring

Result:
no goals