-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem U_eval_neg_one (n : ℤ) : (U R n).eval (-1) = n.negOnePow * (n + 1)

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

Tactic:
norm_num

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

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

Tactic:
ring

Result:
no goals

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

Tactic:
ring

Result:
no goals

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

Tactic:
norm_cast

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

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

Tactic:
simp

Result:
case one
R : Type u_1
inst✝ : CommRing R
⊢ -2 = -1 + -1

Proof state:
case one
R : Type u_1
inst✝ : CommRing R
⊢ -2 = -1 + -1

Tactic:
norm_num

Result:
no goals

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

Tactic:
induction n using Polynomial.Chebyshev.induct with
| zero => simp
| one => simp; norm_num
| add_two n ih1 ih2 =>
  simp only [U_add_two, eval_sub, eval_mul, eval_ofNat, eval_X, mul_neg, mul_one, ih1,
    Int.cast_add, Int.cast_natCast, Int.cast_one, neg_mul, ih2, Int.cast_ofNat, Int.negOnePow_add,
    Int.negOnePow_def 2]
  norm_cast
  norm_num
  ring
| neg_add_one n ih1 ih2 =>
  simp only [U_sub_one, eval_sub, eval_mul, eval_ofNat, eval_X, mul_neg, mul_one, ih1,
    Int.cast_neg, Int.cast_natCast, Int.negOnePow_neg, neg_mul, ih2, Int.cast_add, Int.cast_one,
    Int.cast_sub, sub_add_cancel, Int.negOnePow_sub, Int.negOnePow_add]
  norm_cast
  norm_num
  ring

Result:
no goals

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

Tactic:
simp only [U_add_two, eval_sub, eval_mul, eval_ofNat, eval_X, mul_neg, mul_one, ih1,
  Int.cast_add, Int.cast_natCast, Int.cast_one, neg_mul, ih2, Int.cast_ofNat, Int.negOnePow_add,
  Int.negOnePow_def 2]

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

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

Tactic:
simp

Result:
no goals

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

Tactic:
simp only [U_sub_one, eval_sub, eval_mul, eval_ofNat, eval_X, mul_neg, mul_one, ih1,
  Int.cast_neg, Int.cast_natCast, Int.negOnePow_neg, neg_mul, ih2, Int.cast_add, Int.cast_one,
  Int.cast_sub, sub_add_cancel, Int.negOnePow_sub, Int.negOnePow_add]

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

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

Tactic:
norm_cast

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

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

Tactic:
norm_num

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