-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem U_eq_X_mul_U_add_T (n : ℤ) : U R (n + 1) = X * U R n + T R (n + 1)

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

Tactic:
simp [two_mul]

Result:
no goals

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

Tactic:
ring

Result:
no goals

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

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

Result:
case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : U R (↑n + 1 + 1) = X * U R (↑n + 1) + T R (↑n + 1 + 1)
ih2 : U R (↑n + 1) = X * U R ↑n + T 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) = X * U R (↑n + 2) + T R (↑n + 2 + 1)

Proof state:
case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : U R (↑n + 1 + 1) = X * U R (↑n + 1) + T R (↑n + 1 + 1)
ih2 : U R (↑n + 1) = X * U R ↑n + T 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) = X * U R (↑n + 2) + T R (↑n + 2 + 1)

Tactic:
have h₂ := U_add_two R n

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

Proof state:
case one
R : Type u_1
inst✝ : CommRing R
⊢ U R (1 + 1) = X * U R 1 + T R (1 + 1)

Tactic:
simp [U_two, T_two]

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

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

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

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

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

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

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

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ U R (n + 1) = X * U R n + T R (n + 1)

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

Result:
no goals

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

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

Result:
no goals

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

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

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

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

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

Result:
no goals

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

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

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