awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
h : T R (n - 1 + 2) = HMul.hMul (α := R[X]) X (U R (n - 1 + 1)) - U R (n - 1)
a :
  HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * (↑n : R[X]) * T R (n + 1) +
        HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * (↑n : R[X]) * (HMul.hMul (α := R[X]) X (U R (n - 1 + 1)) - U R (n - 1)) -
      (HMul.hMul (α := R[X]) (↑n : R[X]) X * (HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * U R (n + 1 - 1)) -
          HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * HMul.hMul (α := R[X]) (↑n : R[X]) (U R (n - 1)) +
        HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * (↑n : R[X]) * T R (n - 1 + 2)) =
    0
⊢ HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * (↑n : R[X]) * T R (n + 1) +
        HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * (↑n : R[X]) * (HMul.hMul (α := R[X]) X (U R (n - 1 + 1)) - U R (n - 1)) -
      (HMul.hMul (α := R[X]) (↑n : R[X]) X * HMul.hMul (α := R[X]) (↑(n + 1) : R[X]) (U R (n + 1 - 1)) -
          HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * HMul.hMul (α := R[X]) (↑n : R[X]) (U R (n - 1)) +
        HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * (↑n : R[X]) * T R (n - 1 + 2)) =
    0

Tactic:
push_cast
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
h : T R (n - 1 + 2) = HMul.hMul (α := R[X]) X (U R (n - 1 + 1)) - U R (n - 1)
⊢ HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * (↑n : R[X]) * T R (n + 1) +
        HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * (↑n : R[X]) * (HMul.hMul (α := R[X]) X (U R (n - 1 + 1)) - U R (n - 1)) -
      (HMul.hMul (α := R[X]) (↑n : R[X]) X * (HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * U R (n + 1 - 1)) -
          HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * HMul.hMul (α := R[X]) (↑n : R[X]) (U R (n - 1)) +
        HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * (↑n : R[X]) * T R (n - 1 + 2)) =
    0

Tactic:
ring_nf
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
h : T R (n - 1 + 2) = HMul.hMul (α := R[X]) X (U R (n - 1 + 1)) - U R (n - 1)
a :
  HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * (↑n : R[X]) * T R (n + 1) +
        HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * (↑n : R[X]) * (HMul.hMul (α := R[X]) X (U R (n - 1 + 1)) - U R (n - 1)) -
      (HMul.hMul (α := R[X]) (↑n : R[X]) X * HMul.hMul (α := R[X]) (↑(n + 1) : R[X]) (U R (n + 1 - 1)) -
          HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * HMul.hMul (α := R[X]) (↑n : R[X]) (U R (n - 1)) +
        HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * (↑n : R[X]) * T R (n - 1 + 2)) =
    0
⊢ HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * (↑n : R[X]) * T R (n + 1) =
    HMul.hMul (α := R[X]) (↑n : R[X]) X * HMul.hMul (α := R[X]) (↑(n + 1) : R[X]) (U R (n + 1 - 1)) -
      HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * HMul.hMul (α := R[X]) (↑n : R[X]) (U R (n - 1))

Tactic:
linear_combination (norm := (push_cast; ring_nf))
    (n + 1) * n * h

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ Eq (α := R[X])
    ((derivative : (a : R[X]) → R[X])
        (HMul.hMul (β := R[X]) (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2)
          ((derivative : (a : R[X]) → R[X]) (T R (n - 1 + 1)) : R[X])) :
      R[X])
    ((derivative : (a : R[X]) → R[X])
        (HAdd.hAdd (α := R[X]) (↑(n - 1) : R[X]) 1 * (T R (n - 1) - HMul.hMul (α := R[X]) X (T R (n - 1 + 1)))) :
      R[X])

Tactic:
have h₁ := congr_arg derivative <| one_sub_X_sq_mul_derivative_T_eq_poly_in_T (R := R) (n - 1)
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
h₁ :
  Eq (α := R[X])
    ((derivative : (a : R[X]) → R[X])
        (HMul.hMul (β := R[X]) (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2)
          ((derivative : (a : R[X]) → R[X]) (T R (n - 1 + 1)) : R[X])) :
      R[X])
    ((derivative : (a : R[X]) → R[X])
        (HAdd.hAdd (α := R[X]) (↑(n - 1) : R[X]) 1 * (T R (n - 1) - HMul.hMul (α := R[X]) X (T R (n - 1 + 1)))) :
      R[X])
⊢ HMul.hMul (β := R[X]) (0 - (↑2 : R[X]) * HPow.hPow (α := R[X]) X (HSub.hSub (α := ℕ) 2 1))
        ((derivative : (a : R[X]) → R[X]) (T R n) : R[X]) +
      HMul.hMul (β := R[X]) (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2)
        ((derivative : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) (T R n)) : R[X]) =
    0 * (T R (n - 1) - HMul.hMul (α := R[X]) X (T R n)) +
      (↑n : R[X]) *
        HSub.hSub (α := R[X]) ((derivative : (a : R[X]) → R[X]) (T R (n - 1)) : R[X])
          (HMul.hMul (α := R[X]) 1 (T R n) +
            HMul.hMul (α := R[X]) (β := R[X]) X ((derivative : (a : R[X]) → R[X]) (T R n) : R[X]))

Tactic:
simp only [derivative_sub, derivative_mul, derivative_X, derivative_one, derivative_X_pow,
    C_eq_natCast, sub_add_cancel, Int.cast_sub, Int.cast_one, derivative_intCast] at h₁

Premises used: Polynomial.derivative_mul, Polynomial.derivative_X, Int.cast_sub, Polynomial.C_eq_natCast, Polynomial.derivative_X_pow, Polynomial.derivative_sub, sub_add_cancel, Polynomial.derivative_one, Int.cast_one, Polynomial.derivative_intCast
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
h₁ :
  HMul.hMul (β := R[X]) (0 - (↑2 : R[X]) * HPow.hPow (α := R[X]) X (HSub.hSub (α := ℕ) 2 1))
        ((derivative : (a : R[X]) → R[X]) (T R n) : R[X]) +
      HMul.hMul (β := R[X]) (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2)
        ((derivative : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) (T R n)) : R[X]) =
    0 * (T R (n - 1) - HMul.hMul (α := R[X]) X (T R n)) +
      (↑n : R[X]) *
        HSub.hSub (α := R[X]) ((derivative : (a : R[X]) → R[X]) (T R (n - 1)) : R[X])
          (HMul.hMul (α := R[X]) 1 (T R n) +
            HMul.hMul (α := R[X]) (β := R[X]) X ((derivative : (a : R[X]) → R[X]) (T R n) : R[X]))
⊢ HAdd.hAdd (α := R[X]) (↑(n - 1) : R[X]) 1 * (↑(n - 1) : R[X]) * T R (n - 1 + 1) =
    HMul.hMul (β := R[X]) (HMul.hMul (α := R[X]) (↑(n - 1) : R[X]) X)
        ((derivative : (a : R[X]) → R[X]) (T R (n - 1 + 1)) : R[X]) -
      HMul.hMul (β := R[X]) (HAdd.hAdd (α := R[X]) (↑(n - 1) : R[X]) 1)
        ((derivative : (a : R[X]) → R[X]) (T R (n - 1)) : R[X])

Tactic:
have h₂ := add_one_mul_self_mul_T_eq_poly_in_T (R := R) (n - 1)
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
h₁ :
  HMul.hMul (β := R[X]) (0 - (↑2 : R[X]) * HPow.hPow (α := R[X]) X (HSub.hSub (α := ℕ) 2 1))
        ((derivative : (a : R[X]) → R[X]) (T R n) : R[X]) +
      HMul.hMul (β := R[X]) (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2)
        ((derivative : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) (T R n)) : R[X]) =
    0 * (T R (n - 1) - HMul.hMul (α := R[X]) X (T R n)) +
      (↑n : R[X]) *
        HSub.hSub (α := R[X]) ((derivative : (a : R[X]) → R[X]) (T R (n - 1)) : R[X])
          (HMul.hMul (α := R[X]) 1 (T R n) +
            HMul.hMul (α := R[X]) (β := R[X]) X ((derivative : (a : R[X]) → R[X]) (T R n) : R[X]))
h₂ :
  HAdd.hAdd (α := R[X]) (↑(n - 1) : R[X]) 1 * (↑(n - 1) : R[X]) * T R (n - 1 + 1) =
    HMul.hMul (β := R[X]) (HMul.hMul (α := R[X]) (↑(n - 1) : R[X]) X)
        ((derivative : (a : R[X]) → R[X]) (T R (n - 1 + 1)) : R[X]) -
      HMul.hMul (β := R[X]) (HAdd.hAdd (α := R[X]) (↑(n - 1) : R[X]) 1)
        ((derivative : (a : R[X]) → R[X]) (T R (n - 1)) : R[X])
⊢ HMul.hMul (β := R[X]) (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2)
          ((derivative : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) (T R n)) : R[X]) +
        (0 * (T R (n - 1) - HMul.hMul (α := R[X]) X (T R n)) +
            (↑n : R[X]) *
              HSub.hSub (α := R[X]) ((derivative : (a : R[X]) → R[X]) (T R (n - 1)) : R[X])
                (HMul.hMul (α := R[X]) 1 (T R n) +
                  HMul.hMul (α := R[X]) (β := R[X]) X ((derivative : (a : R[X]) → R[X]) (T R n) : R[X])) +
          (HMul.hMul (β := R[X]) (HSub.hSub (α := R[X]) (↑n : R[X]) 1 * X)
              ((derivative : (a : R[X]) → R[X]) (T R (n - 1 + 1)) : R[X]) -
            HMul.hMul (β := R[X]) (HSub.hSub (α := R[X]) (↑n : R[X]) 1 + 1)
              ((derivative : (a : R[X]) → R[X]) (T R (n - 1)) : R[X]))) -
      (HMul.hMul (α := R[X]) (β := R[X]) X ((derivative : (a : R[X]) → R[X]) (T R n) : R[X]) -
          HPow.hPow (α := R[X]) (β := ℕ) (↑n : R[X]) 2 * T R n +
        (HMul.hMul (β := R[X]) (0 - 2 * HPow.hPow (α := R[X]) (β := ℕ) X 1)
              ((derivative : (a : R[X]) → R[X]) (T R n) : R[X]) +
            HMul.hMul (β := R[X]) (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2)
              ((derivative : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) (T R n)) : R[X]) +
          (HSub.hSub (α := R[X]) (↑n : R[X]) 1 + 1) * HSub.hSub (α := R[X]) (↑n : R[X]) 1 * T R (n - 1 + 1))) =
    0

Tactic:
ring_nf
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
h₁ :
  HMul.hMul (β := R[X]) (0 - (↑2 : R[X]) * HPow.hPow (α := R[X]) X (HSub.hSub (α := ℕ) 2 1))
        ((derivative : (a : R[X]) → R[X]) (T R n) : R[X]) +
      HMul.hMul (β := R[X]) (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2)
        ((derivative : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) (T R n)) : R[X]) =
    0 * (T R (n - 1) - HMul.hMul (α := R[X]) X (T R n)) +
      (↑n : R[X]) *
        HSub.hSub (α := R[X]) ((derivative : (a : R[X]) → R[X]) (T R (n - 1)) : R[X])
          (HMul.hMul (α := R[X]) 1 (T R n) +
            HMul.hMul (α := R[X]) (β := R[X]) X ((derivative : (a : R[X]) → R[X]) (T R n) : R[X]))
h₂ :
  HAdd.hAdd (α := R[X]) (↑(n - 1) : R[X]) 1 * (↑(n - 1) : R[X]) * T R (n - 1 + 1) =
    HMul.hMul (β := R[X]) (HMul.hMul (α := R[X]) (↑(n - 1) : R[X]) X)
        ((derivative : (a : R[X]) → R[X]) (T R (n - 1 + 1)) : R[X]) -
      HMul.hMul (β := R[X]) (HAdd.hAdd (α := R[X]) (↑(n - 1) : R[X]) 1)
        ((derivative : (a : R[X]) → R[X]) (T R (n - 1)) : R[X])
a :
  HMul.hMul (β := R[X]) (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2)
          ((derivative : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) (T R n)) : R[X]) +
        (0 * (T R (n - 1) - HMul.hMul (α := R[X]) X (T R n)) +
            (↑n : R[X]) *
              HSub.hSub (α := R[X]) ((derivative : (a : R[X]) → R[X]) (T R (n - 1)) : R[X])
                (HMul.hMul (α := R[X]) 1 (T R n) +
                  HMul.hMul (α := R[X]) (β := R[X]) X ((derivative : (a : R[X]) → R[X]) (T R n) : R[X])) +
          (HMul.hMul (β := R[X]) (HMul.hMul (α := R[X]) (↑(n - 1) : R[X]) X)
              ((derivative : (a : R[X]) → R[X]) (T R (n - 1 + 1)) : R[X]) -
            HMul.hMul (β := R[X]) (HAdd.hAdd (α := R[X]) (↑(n - 1) : R[X]) 1)
              ((derivative : (a : R[X]) → R[X]) (T R (n - 1)) : R[X]))) -
      (HMul.hMul (α := R[X]) (β := R[X]) X ((derivative : (a : R[X]) → R[X]) (T R n) : R[X]) -
          HPow.hPow (α := R[X]) (β := ℕ) (↑n : R[X]) 2 * T R n +
        (HMul.hMul (β := R[X]) (0 - (↑2 : R[X]) * HPow.hPow (α := R[X]) X (HSub.hSub (α := ℕ) 2 1))
              ((derivative : (a : R[X]) → R[X]) (T R n) : R[X]) +
            HMul.hMul (β := R[X]) (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2)
              ((derivative : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) (T R n)) : R[X]) +
          HAdd.hAdd (α := R[X]) (↑(n - 1) : R[X]) 1 * (↑(n - 1) : R[X]) * T R (n - 1 + 1))) =
    0
⊢ HMul.hMul (β := R[X]) (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2)
      ((derivative : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) (T R n)) : R[X]) =
    HMul.hMul (α := R[X]) (β := R[X]) X ((derivative : (a : R[X]) → R[X]) (T R n) : R[X]) -
      HPow.hPow (α := R[X]) (β := ℕ) (↑n : R[X]) 2 * T R n

Tactic:
linear_combination (norm := (push_cast; ring_nf))
    h₁ + h₂
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) (HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * T R (n + 1)) : R[X])
    ((derivative : (a : R[X]) → R[X])
        (HMul.hMul (α := R[X]) X (U R n) -
          HMul.hMul (β := R[X]) (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2)
            ((derivative : (a : R[X]) → R[X]) (U R n) : R[X])) :
      R[X])

Tactic:
have h := congr_arg derivative <| add_one_mul_T_eq_poly_in_U (R := R) n
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
h :
  Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) (HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * T R (n + 1)) : R[X])
    ((derivative : (a : R[X]) → R[X])
        (HMul.hMul (α := R[X]) X (U R n) -
          HMul.hMul (β := R[X]) (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2)
            ((derivative : (a : R[X]) → R[X]) (U R n) : R[X])) :
      R[X])
⊢ HAdd.hAdd (α := R[X]) 0 0 * T R (n + 1) +
      HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * HMul.hMul (α := R[X]) (↑(n + 1) : R[X]) (U R (n + 1 - 1)) =
    HMul.hMul (α := R[X]) 1 (U R n) +
        HMul.hMul (α := R[X]) (β := R[X]) X ((derivative : (a : R[X]) → R[X]) (U R n) : R[X]) -
      (HMul.hMul (β := R[X]) (0 - (↑2 : R[X]) * HPow.hPow (α := R[X]) X (HSub.hSub (α := ℕ) 2 1))
          ((derivative : (a : R[X]) → R[X]) (U R n) : R[X]) +
        HMul.hMul (β := R[X]) (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2)
          ((derivative : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) (U R n)) : R[X]))

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

Premises used: Polynomial.derivative_mul, Polynomial.derivative_X, Polynomial.Chebyshev.T_derivative_eq_U, Polynomial.C_eq_natCast, Polynomial.derivative_X_pow, Polynomial.derivative_sub, Polynomial.derivative_one, Polynomial.derivative_intCast, Polynomial.derivative_add
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
h :
  HAdd.hAdd (α := R[X]) 0 0 * T R (n + 1) +
      HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * HMul.hMul (α := R[X]) (↑(n + 1) : R[X]) (U R (n + 1 - 1)) =
    HMul.hMul (α := R[X]) 1 (U R n) +
        HMul.hMul (α := R[X]) (β := R[X]) X ((derivative : (a : R[X]) → R[X]) (U R n) : R[X]) -
      (HMul.hMul (β := R[X]) (0 - (↑2 : R[X]) * HPow.hPow (α := R[X]) X (HSub.hSub (α := ℕ) 2 1))
          ((derivative : (a : R[X]) → R[X]) (U R n) : R[X]) +
        HMul.hMul (β := R[X]) (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2)
          ((derivative : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) (U R n)) : R[X]))
a :
  HMul.hMul (β := R[X]) (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2)
          ((derivative : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) (U R n)) : R[X]) +
        (HMul.hMul (α := R[X]) 1 (U R n) +
            HMul.hMul (α := R[X]) (β := R[X]) X ((derivative : (a : R[X]) → R[X]) (U R n) : R[X]) -
          (HMul.hMul (β := R[X]) (0 - 2 * HPow.hPow (α := R[X]) (β := ℕ) X 1)
              ((derivative : (a : R[X]) → R[X]) (U R n) : R[X]) +
            HMul.hMul (β := R[X]) (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2)
              ((derivative : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) (U R n)) : R[X]))) -
      (HMul.hMul (β := R[X]) (HMul.hMul (α := R[X]) 3 X) ((derivative : (a : R[X]) → R[X]) (U R n) : R[X]) -
          HAdd.hAdd (α := R[X]) (↑n : R[X]) 2 * (↑n : R[X]) * U R n +
        (HAdd.hAdd (α := R[X]) 0 0 * T R (n + 1) +
          HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * (HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * U R (n + 1 - 1)))) =
    0
⊢ HMul.hMul (β := R[X]) (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2)
          ((derivative : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) (U R n)) : R[X]) +
        (HMul.hMul (α := R[X]) 1 (U R n) +
            HMul.hMul (α := R[X]) (β := R[X]) X ((derivative : (a : R[X]) → R[X]) (U R n) : R[X]) -
          (HMul.hMul (β := R[X]) (0 - (↑2 : R[X]) * HPow.hPow (α := R[X]) X (HSub.hSub (α := ℕ) 2 1))
              ((derivative : (a : R[X]) → R[X]) (U R n) : R[X]) +
            HMul.hMul (β := R[X]) (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2)
              ((derivative : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) (U R n)) : R[X]))) -
      (HMul.hMul (β := R[X]) (HMul.hMul (α := R[X]) 3 X) ((derivative : (a : R[X]) → R[X]) (U R n) : R[X]) -
          HAdd.hAdd (α := R[X]) (↑n : R[X]) 2 * (↑n : R[X]) * U R n +
        (HAdd.hAdd (α := R[X]) 0 0 * T R (n + 1) +
          HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * HMul.hMul (α := R[X]) (↑(n + 1) : R[X]) (U R (n + 1 - 1)))) =
    0

Tactic:
push_cast
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
h :
  HAdd.hAdd (α := R[X]) 0 0 * T R (n + 1) +
      HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * HMul.hMul (α := R[X]) (↑(n + 1) : R[X]) (U R (n + 1 - 1)) =
    HMul.hMul (α := R[X]) 1 (U R n) +
        HMul.hMul (α := R[X]) (β := R[X]) X ((derivative : (a : R[X]) → R[X]) (U R n) : R[X]) -
      (HMul.hMul (β := R[X]) (0 - (↑2 : R[X]) * HPow.hPow (α := R[X]) X (HSub.hSub (α := ℕ) 2 1))
          ((derivative : (a : R[X]) → R[X]) (U R n) : R[X]) +
        HMul.hMul (β := R[X]) (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2)
          ((derivative : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) (U R n)) : R[X]))
⊢ HMul.hMul (β := R[X]) (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2)
          ((derivative : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) (U R n)) : R[X]) +
        (HMul.hMul (α := R[X]) 1 (U R n) +
            HMul.hMul (α := R[X]) (β := R[X]) X ((derivative : (a : R[X]) → R[X]) (U R n) : R[X]) -
          (HMul.hMul (β := R[X]) (0 - 2 * HPow.hPow (α := R[X]) (β := ℕ) X 1)
              ((derivative : (a : R[X]) → R[X]) (U R n) : R[X]) +
            HMul.hMul (β := R[X]) (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2)
              ((derivative : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) (U R n)) : R[X]))) -
      (HMul.hMul (β := R[X]) (HMul.hMul (α := R[X]) 3 X) ((derivative : (a : R[X]) → R[X]) (U R n) : R[X]) -
          HAdd.hAdd (α := R[X]) (↑n : R[X]) 2 * (↑n : R[X]) * U R n +
        (HAdd.hAdd (α := R[X]) 0 0 * T R (n + 1) +
          HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * (HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * U R (n + 1 - 1)))) =
    0

Tactic:
ring_nf
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
h :
  HAdd.hAdd (α := R[X]) 0 0 * T R (n + 1) +
      HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * HMul.hMul (α := R[X]) (↑(n + 1) : R[X]) (U R (n + 1 - 1)) =
    HMul.hMul (α := R[X]) 1 (U R n) +
        HMul.hMul (α := R[X]) (β := R[X]) X ((derivative : (a : R[X]) → R[X]) (U R n) : R[X]) -
      (HMul.hMul (β := R[X]) (0 - (↑2 : R[X]) * HPow.hPow (α := R[X]) X (HSub.hSub (α := ℕ) 2 1))
          ((derivative : (a : R[X]) → R[X]) (U R n) : R[X]) +
        HMul.hMul (β := R[X]) (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2)
          ((derivative : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) (U R n)) : R[X]))
a :
  HMul.hMul (β := R[X]) (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2)
          ((derivative : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) (U R n)) : R[X]) +
        (HMul.hMul (α := R[X]) 1 (U R n) +
            HMul.hMul (α := R[X]) (β := R[X]) X ((derivative : (a : R[X]) → R[X]) (U R n) : R[X]) -
          (HMul.hMul (β := R[X]) (0 - (↑2 : R[X]) * HPow.hPow (α := R[X]) X (HSub.hSub (α := ℕ) 2 1))
              ((derivative : (a : R[X]) → R[X]) (U R n) : R[X]) +
            HMul.hMul (β := R[X]) (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2)
              ((derivative : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) (U R n)) : R[X]))) -
      (HMul.hMul (β := R[X]) (HMul.hMul (α := R[X]) 3 X) ((derivative : (a : R[X]) → R[X]) (U R n) : R[X]) -
          HAdd.hAdd (α := R[X]) (↑n : R[X]) 2 * (↑n : R[X]) * U R n +
        (HAdd.hAdd (α := R[X]) 0 0 * T R (n + 1) +
          HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * HMul.hMul (α := R[X]) (↑(n + 1) : R[X]) (U R (n + 1 - 1)))) =
    0
⊢ HMul.hMul (β := R[X]) (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2)
      ((derivative : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) (U R n)) : R[X]) =
    HMul.hMul (β := R[X]) (HMul.hMul (α := R[X]) 3 X) ((derivative : (a : R[X]) → R[X]) (U R n) : R[X]) -
      HAdd.hAdd (α := R[X]) (↑n : R[X]) 2 * (↑n : R[X]) * U R n

Tactic:
linear_combination (norm := (push_cast; ring_nf)) h
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
k : ℕ
⊢ (⇑derivative : (a : R[X]) → R[X])^[k]
      ((1 - HPow.hPow (α := R[X]) (β := ℕ) X 2) * (⇑derivative : (a : R[X]) → R[X])^[2] (T R n)) =
    (⇑derivative : (a : R[X]) → R[X])^[k]
      (HMul.hMul (α := R[X]) (β := R[X]) X ((derivative : (a : R[X]) → R[X]) (T R n) : R[X]) -
        HPow.hPow (α := R[X]) (β := ℕ) (↑n : R[X]) 2 * T R n)

Tactic:
have h := congr_arg derivative^[k] <| one_sub_X_sq_mul_derivative_derivative_T_eq_poly_in_T
    (R := R) n
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
k : ℕ
h :
  (⇑derivative : (a : R[X]) → R[X])^[k]
      ((1 - HPow.hPow (α := R[X]) (β := ℕ) X 2) * (⇑derivative : (a : R[X]) → R[X])^[2] (T R n)) =
    (⇑derivative : (a : R[X]) → R[X])^[k]
      (HMul.hMul (α := R[X]) (β := R[X]) X ((derivative : (a : R[X]) → R[X]) (T R n) : R[X]) -
        HPow.hPow (α := R[X]) (β := ℕ) (↑n : R[X]) 2 * T R n)
⊢ (⇑derivative : (a : R[X]) → R[X])^[k]
      ((1 - HPow.hPow (α := R[X]) (β := ℕ) X 2) * (⇑derivative : (a : R[X]) → R[X])^[2] (T R n)) =
    (⇑derivative : (a : R[X]) → R[X])^[k]
      (HMul.hMul (α := R[X]) (β := R[X]) X ((derivative : (a : R[X]) → R[X]) (T R n) : R[X]) -
        HMul.hMul (α := R[X]) (↑(HPow.hPow (β := ℕ) n 2) : R[X]) (T R n))

Tactic:
norm_cast at h
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
k : ℕ
h :
  (⇑derivative : (a : R[X]) → R[X])^[k]
      ((1 - HPow.hPow (α := R[X]) (β := ℕ) X 2) * (⇑derivative : (a : R[X]) → R[X])^[2] (T R n)) =
    (⇑derivative : (a : R[X]) → R[X])^[k]
      (HMul.hMul (α := R[X]) (β := R[X]) X ((derivative : (a : R[X]) → R[X]) (T R n) : R[X]) -
        HMul.hMul (α := R[X]) (↑(HPow.hPow (β := ℕ) n 2) : R[X]) (T R n))
⊢ (⇑derivative : (a : R[X]) → R[X])^[k + 2] (T R n) -
      ((⇑derivative : (a : R[X]) → R[X])^[k + 2] (T R n) * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
          HSMul.hSMul (β := R[X]) (2 * k) ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (T R n)) * X +
        HSMul.hSMul (β := R[X]) (k * (k - 1)) ((⇑derivative : (a : R[X]) → R[X])^[k] (T R n))) =
    HMul.hMul (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (T R n)) X +
        HSMul.hSMul (β := R[X]) k ((⇑derivative : (a : R[X]) → R[X])^[k] (T R n)) -
      HMul.hMul (α := R[X]) (↑(HPow.hPow (β := ℕ) n 2) : R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k] (T R n))

Tactic:
rw [sub_mul, iterate_derivative_sub, one_mul, ← Function.iterate_add_apply, mul_comm (X ^ 2),
    iterate_derivative_sub, mul_comm X, iterate_derivative_intCast_mul,
    iterate_derivative_derivative_mul_X_sq, iterate_derivative_derivative_mul_X] at h

Premises used: Function.iterate_add_apply, Polynomial.iterate_derivative_derivative_mul_X_sq, Polynomial.iterate_derivative_derivative_mul_X, sub_mul, HPow.hPow, Polynomial.iterate_derivative_sub, mul_comm, Polynomial.iterate_derivative_intCast_mul, OfNat.ofNat, Polynomial.X, one_mul