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

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

Tactic:
rfl

Result:
no goals

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

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

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

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

Tactic:
have h₁ := C_add_one R n

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

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

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

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

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

Tactic:
show X * 2 - X = X

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

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

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

Result:
no goals

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

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

Result:
no goals

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

Tactic:
have h₁ := C_add_two R n

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

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

Tactic:
induction n using Polynomial.Chebyshev.induct with
| zero => rfl
| one => show X * 2 - X = X; ring
| add_two n ih1 ih2 =>
  have h₁ := C_add_two R n
  have h₂ := C_sub_two R (-n)
  linear_combination (norm := ring_nf) (X:R[X]) * ih1 - ih2 - h₁ + h₂
| neg_add_one n ih1 ih2 =>
  have h₁ := C_add_one R n
  have h₂ := C_sub_one R (-n)
  linear_combination (norm := ring_nf) (X:R[X]) * ih1 - ih2 + h₁ - h₂

Result:
no goals

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

Tactic:
ring

Result:
no goals