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

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

Tactic:
simp

Result:
no goals

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

Tactic:
induction n using Polynomial.Chebyshev.induct with
| zero => simp
| one => simp
| add_two n ih1 ih2 =>
  have h₁ := S_add_one R n
  have h₂ := S_sub_two R (-n - 1)
  linear_combination (norm := ring_nf) (X:R[X]) * ih1 - ih2 + h₁ + h₂
| neg_add_one n ih1 ih2 =>
  have h₁ := S_eq R n
  have h₂ := S_sub_two R (-n)
  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 : S R (-(↑n + 1) - 1) = -S R (↑n + 1 - 1)
ih2 : S R (-↑n - 1) = -S R (↑n - 1)
⊢ S R (-(↑n + 2) - 1) = -S R (↑n + 2 - 1)

Tactic:
have h₁ := S_add_one R n

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

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

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

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

Proof state:
case neg_add_one
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : S R (- -↑n - 1) = -S R (-↑n - 1)
ih2 : S R (-(-↑n + 1) - 1) = -S R (-↑n + 1 - 1)
h₁ : S R ↑n = X * S R (↑n - 1) - S R (↑n - 2)
h₂ : S R (-↑n - 2) = X * S R (-↑n - 1) - S R (-↑n)
⊢ S R (-(-↑n - 1) - 1) = -S R (-↑n - 1 - 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 : S R (-(↑n + 1) - 1) = -S R (↑n + 1 - 1)
ih2 : S R (-↑n - 1) = -S R (↑n - 1)
h₁ : S R (↑n + 1) = X * S R ↑n - S R (↑n - 1)
h₂ : S R (-↑n - 1 - 2) = X * S R (-↑n - 1 - 1) - S R (-↑n - 1)
⊢ S R (-(↑n + 2) - 1) = -S R (↑n + 2 - 1)

Tactic:
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
⊢ S R (-1 - 1) = -S R (1 - 1)

Tactic:
simp

Result:
no goals

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

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

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

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

Tactic:
have h₁ := S_eq R n

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