-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem one_sub_X_sq_mul_derivative_T_eq_poly_in_T (n : ℤ) :
    (1 - X ^ 2) * derivative (T R (n + 1)) = (n + 1 : R[X]) * (T R n - X * T R (n + 1))

Proof state:
case a.a
R : Type u_1
inst✝ : CommRing R
n : ℤ
H₁ : (1 - X ^ 2) * U R n = X * T R (n + 1) - T R (n + 2)
H₂ : derivative (T R (n + 1)) = ↑(n + 1) * U R (n + 1 - 1)
h₁ : T R (n + 2) = 2 * X * T R (n + 1) - T R n
⊢ (1 - X ^ 2) * derivative (T R (n + 1)) +
        ((-↑n - 1) * (2 * X * T R (n + 1) - T R n) + (-X ^ 2 + 1) * (↑(n + 1) * U R (n + 1 - 1)) +
          (↑n + 1) * (X * T R (n + 1) - T R (n + 2))) -
      ((↑n + 1) * (T R n - X * T R (n + 1)) +
        ((-↑n - 1) * T R (n + 2) + (-X ^ 2 + 1) * derivative (T R (n + 1)) + (↑n + 1) * ((1 - X ^ 2) * U R n))) =
    0

Tactic:
push_cast

Result:
case a.a
R : Type u_1
inst✝ : CommRing R
n : ℤ
H₁ : (1 - X ^ 2) * U R n = X * T R (n + 1) - T R (n + 2)
H₂ : derivative (T R (n + 1)) = ↑(n + 1) * U R (n + 1 - 1)
h₁ : T R (n + 2) = 2 * X * T R (n + 1) - T R n
⊢ (1 - X ^ 2) * derivative (T R (n + 1)) +
        ((-↑n - 1) * (2 * X * T R (n + 1) - T R n) + (-X ^ 2 + 1) * ((↑n + 1) * U R (n + 1 - 1)) +
          (↑n + 1) * (X * T R (n + 1) - T R (n + 2))) -
      ((↑n + 1) * (T R n - X * T R (n + 1)) +
        ((-↑n - 1) * T R (n + 2) + (-X ^ 2 + 1) * derivative (T R (n + 1)) + (↑n + 1) * ((1 - X ^ 2) * U R n))) =
    0

Proof state:
case a.a
R : Type u_1
inst✝ : CommRing R
n : ℤ
H₁ : (1 - X ^ 2) * U R n = X * T R (n + 1) - T R (n + 2)
H₂ : derivative (T R (n + 1)) = ↑(n + 1) * U R (n + 1 - 1)
h₁ : T R (n + 2) = 2 * X * T R (n + 1) - T R n
⊢ (1 - X ^ 2) * derivative (T R (n + 1)) +
        ((-↑n - 1) * (2 * X * T R (n + 1) - T R n) + (-X ^ 2 + 1) * ((↑n + 1) * U R (n + 1 - 1)) +
          (↑n + 1) * (X * T R (n + 1) - T R (n + 2))) -
      ((↑n + 1) * (T R n - X * T R (n + 1)) +
        ((-↑n - 1) * T R (n + 2) + (-X ^ 2 + 1) * derivative (T R (n + 1)) + (↑n + 1) * ((1 - X ^ 2) * U R n))) =
    0

Tactic:
ring_nf

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ (1 - X ^ 2) * derivative (T R (n + 1)) = (↑n + 1) * (T R n - X * T R (n + 1))

Tactic:
have H₁ := one_sub_X_sq_mul_U_eq_pol_in_T R n

Result:
R : Type u_1
inst✝ : CommRing R
n : ℤ
H₁ : (1 - X ^ 2) * U R n = X * T R (n + 1) - T R (n + 2)
⊢ (1 - X ^ 2) * derivative (T R (n + 1)) = (↑n + 1) * (T R n - X * T R (n + 1))

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℤ
H₁ : (1 - X ^ 2) * U R n = X * T R (n + 1) - T R (n + 2)
H₂ : derivative (T R (n + 1)) = ↑(n + 1) * U R (n + 1 - 1)
h₁ : T R (n + 2) = 2 * X * T R (n + 1) - T R n
⊢ (1 - X ^ 2) * derivative (T R (n + 1)) = (↑n + 1) * (T R n - X * T R (n + 1))

Tactic:
linear_combination (norm := (push_cast; ring_nf))
  (-n - 1) * h₁ + (-(X : R[X]) ^ 2 + 1) * H₂ + (n + 1) * H₁

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℤ
H₁ : (1 - X ^ 2) * U R n = X * T R (n + 1) - T R (n + 2)
H₂ : derivative (T R (n + 1)) = ↑(n + 1) * U R (n + 1 - 1)
⊢ (1 - X ^ 2) * derivative (T R (n + 1)) = (↑n + 1) * (T R n - X * T R (n + 1))

Tactic:
have h₁ := T_add_two R n

Result:
R : Type u_1
inst✝ : CommRing R
n : ℤ
H₁ : (1 - X ^ 2) * U R n = X * T R (n + 1) - T R (n + 2)
H₂ : derivative (T R (n + 1)) = ↑(n + 1) * U R (n + 1 - 1)
h₁ : T R (n + 2) = 2 * X * T R (n + 1) - T R n
⊢ (1 - X ^ 2) * derivative (T R (n + 1)) = (↑n + 1) * (T R n - X * T R (n + 1))

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℤ
H₁ : (1 - X ^ 2) * U R n = X * T R (n + 1) - T R (n + 2)
⊢ (1 - X ^ 2) * derivative (T R (n + 1)) = (↑n + 1) * (T R n - X * T R (n + 1))

Tactic:
have H₂ := T_derivative_eq_U (R := R) (n + 1)

Result:
R : Type u_1
inst✝ : CommRing R
n : ℤ
H₁ : (1 - X ^ 2) * U R n = X * T R (n + 1) - T R (n + 2)
H₂ : derivative (T R (n + 1)) = ↑(n + 1) * U R (n + 1 - 1)
⊢ (1 - X ^ 2) * derivative (T R (n + 1)) = (↑n + 1) * (T R n - X * T R (n + 1))