-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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]) (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
have 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]) (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: push_cast