-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem U_neg_sub_one (n : ℤ) : U R (-n - 1) = -U R (n - 1)

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

Tactic:
have h₁ := U_add_one R n

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

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

Tactic:
have h₁ := U_eq R n

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

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ U R (-n - 1) = -U R (n - 1)

Tactic:
induction n using Polynomial.Chebyshev.induct with
| zero => simp
| one => simp
| add_two n ih1 ih2 =>
  have h₁ := U_add_one R n
  have h₂ := U_sub_two R (-n - 1)
  linear_combination (norm := ring_nf) 2 * (X : R[X]) * ih1 - ih2 + h₁ + h₂
| neg_add_one n ih1 ih2 =>
  have h₁ := U_eq R n
  have h₂ := U_sub_two R (-n)
  linear_combination (norm := ring_nf) 2 * (X : R[X]) * ih1 - ih2 + h₁ + h₂

Result:
no goals

Proof state:
case one
R : Type u_1
inst✝ : CommRing R
⊢ U R (-1 - 1) = -U R (1 - 1)

Tactic:
simp

Result:
no goals

Proof state:
case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : U R (-(↑n + 1) - 1) = -U R (↑n + 1 - 1)
ih2 : U R (-↑n - 1) = -U R (↑n - 1)
h₁ : U R (↑n + 1) = 2 * X * U R ↑n - U R (↑n - 1)
h₂ : U R (-↑n - 1 - 2) = 2 * X * U R (-↑n - 1 - 1) - U R (-↑n - 1)
⊢ U R (-(↑n + 2) - 1) = -U R (↑n + 2 - 1)

Tactic:
linear_combination (norm := ring_nf) 2 * (X : R[X]) * ih1 - ih2 + h₁ + h₂

Result:
no goals

Proof state:
case zero
R : Type u_1
inst✝ : CommRing R
⊢ U R (-0 - 1) = -U R (0 - 1)

Tactic:
simp

Result:
no goals

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

Tactic:
have h₂ := U_sub_two R (-n)

Result:
case neg_add_one
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : U R (- -↑n - 1) = -U R (-↑n - 1)
ih2 : U R (-(-↑n + 1) - 1) = -U R (-↑n + 1 - 1)
h₁ : U R ↑n = 2 * X * U R (↑n - 1) - U R (↑n - 2)
h₂ : U R (-↑n - 2) = 2 * X * U R (-↑n - 1) - U R (-↑n)
⊢ U R (-(-↑n - 1) - 1) = -U R (-↑n - 1 - 1)

Proof state:
case neg_add_one
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : U R (- -↑n - 1) = -U R (-↑n - 1)
ih2 : U R (-(-↑n + 1) - 1) = -U R (-↑n + 1 - 1)
h₁ : U R ↑n = 2 * X * U R (↑n - 1) - U R (↑n - 2)
h₂ : U R (-↑n - 2) = 2 * X * U R (-↑n - 1) - U R (-↑n)
⊢ U R (-(-↑n - 1) - 1) = -U R (-↑n - 1 - 1)

Tactic:
linear_combination (norm := ring_nf) 2 * (X : R[X]) * ih1 - ih2 + h₁ + h₂

Result:
no goals

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

Tactic:
have h₂ := U_sub_two R (-n - 1)

Result:
case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : U R (-(↑n + 1) - 1) = -U R (↑n + 1 - 1)
ih2 : U R (-↑n - 1) = -U R (↑n - 1)
h₁ : U R (↑n + 1) = 2 * X * U R ↑n - U R (↑n - 1)
h₂ : U R (-↑n - 1 - 2) = 2 * X * U R (-↑n - 1 - 1) - U R (-↑n - 1)
⊢ U R (-(↑n + 2) - 1) = -U R (↑n + 2 - 1)