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

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

Tactic:
simp only [derivative_sub, derivative_mul, derivative_X, derivative_one, derivative_X_pow,
  T_derivative_eq_U, C_eq_natCast] at h₁

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

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

Tactic:
have h₁ := congr_arg derivative <| T_eq_X_mul_T_sub_pol_U R n

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

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

Tactic:
push_cast

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

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

Tactic:
linear_combination (norm := (push_cast; ring_nf))
  h₁ + (n + 2) * h₂

Result:
no goals

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

Tactic:
ring_nf

Result:
no goals

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

Tactic:
have h₂ := T_eq_U_sub_X_mul_U R (n + 1)

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