∀ {R : Type u_1} [inst : CommRing R] (n : ℤ) (k : ℕ) (x : R),
  (1 - x ^ 2) * Polynomial.eval x ((⇑Polynomial.derivative)^[k + 2] (Polynomial.Chebyshev.T R n)) =
    (2 * ↑k + 1) * x * Polynomial.eval x ((⇑Polynomial.derivative)^[k + 1] (Polynomial.Chebyshev.T R n)) -
      (↑n ^ 2 - ↑k ^ 2) * Polynomial.eval x ((⇑Polynomial.derivative)^[k] (Polynomial.Chebyshev.T R n))