-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem T_neg (n : ℤ) : T R (-n) = T R n

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

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

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

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

Tactic:
have h₁ := T_add_two R n

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

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

Tactic:
ring

Result:
no goals

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

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

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

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

Tactic:
rfl

Result:
no goals

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

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

Result:
no goals

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

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

Result:
no goals

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

Tactic:
have h₁ := T_add_one R n

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

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

Tactic:
induction n using Polynomial.Chebyshev.induct with
| zero => rfl
| one => show 2 * X * 1 - X = X; ring
| add_two n ih1 ih2 =>
  have h₁ := T_add_two R n
  have h₂ := T_sub_two R (-n)
  linear_combination (norm := ring_nf) (2 * (X : R[X])) * ih1 - ih2 - h₁ + h₂
| neg_add_one n ih1 ih2 =>
  have h₁ := T_add_one R n
  have h₂ := T_sub_one 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
⊢ T R (-1) = T R 1

Tactic:
show 2 * X * 1 - X = X

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