-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem S_eq_X_mul_S_add_C (n : ℤ) : 2 * S R (n + 1) = X * S R n + C R (n + 1)

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

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

Result:
no goals

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

Tactic:
have h₁ := S_add_two R (-n - 1)

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

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

Tactic:
have h₃ := C_add_two R (n + 1)

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

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

Tactic:
ring

Result:
no goals

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

Tactic:
have h₁ := S_add_two R (n + 1)

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

Proof state:
case one
R : Type u_1
inst✝ : CommRing R
⊢ 2 * S R (1 + 1) = X * S R 1 + C R (1 + 1)

Tactic:
simp [S_two, C_two]

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

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

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

Result:
no goals

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

Tactic:
have h₂ := S_add_two R n

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

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

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

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

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ 2 * S R (n + 1) = X * S R n + C R (n + 1)

Tactic:
induction n using Polynomial.Chebyshev.induct with
| zero => simp [two_mul]
| one => simp [S_two, C_two]; ring
| add_two n ih1 ih2 =>
  have h₁ := S_add_two R (n + 1)
  have h₂ := S_add_two R n
  have h₃ := C_add_two R (n + 1)
  linear_combination (norm := ring_nf) -h₃ - (X:R[X]) * h₂ + 2 * h₁ + (X:R[X]) * ih1 - ih2
| neg_add_one n ih1 ih2 =>
  have h₁ := S_add_two R (-n - 1)
  have h₂ := S_add_two R (-n)
  have h₃ := C_add_two R (-n)
  linear_combination (norm := ring_nf) -h₃ + 2 * h₂ - (X:R[X]) * h₁ - ih2 + (X:R[X]) * ih1

Result:
no goals

Proof state:
case zero
R : Type u_1
inst✝ : CommRing R
⊢ 2 * S R (0 + 1) = X * S R 0 + C R (0 + 1)

Tactic:
simp [two_mul]

Result:
no goals

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

Tactic:
have h₃ := C_add_two R (-n)

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