-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
p q : R[X]
n : ℕ
r : R
ih :
  (derivative : (a : R[X]) → R[X])
      (eval₂ C q (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))) =
    HMul.hMul (β := R[X])
      (eval₂ C q
        ((derivative : (a : R[X]) → R[X])
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
rw :
  (derivative : (a : R[X]) → R[X])
      (eval₂ C q (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n * X))) =
    HMul.hMul (β := R[X])
      (eval₂ C q
        ((derivative : (a : R[X]) → R[X])
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n * X))))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
rw₁ :
  (derivative : (a : R[X]) → R[X])
      (eval₂ C q (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n) * X)) =
    HMul.hMul (β := R[X])
      (eval₂ C q
        ((derivative : (a : R[X]) → R[X])
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n) * X)))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
rw₂ :
  (derivative : (a : R[X]) → R[X])
      (eval₂ C q (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)) * eval₂ C q X) =
    HMul.hMul (β := R[X])
      (eval₂ C q
        ((derivative : (a : R[X]) → R[X])
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n) * X)))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
rw₃ :
  (derivative : (a : R[X]) → R[X])
      (eval₂ C q (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)) * q) =
    HMul.hMul (β := R[X])
      (eval₂ C q
        ((derivative : (a : R[X]) → R[X])
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n) * X)))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
rw₄ :
  HMul.hMul (α := R[X])
        ((derivative : (a : R[X]) → R[X])
            (eval₂ C q (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))) :
          R[X])
        q +
      HMul.hMul (β := R[X])
        (eval₂ C q (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)))
        ((derivative : (a : R[X]) → R[X]) q : R[X]) =
    HMul.hMul (β := R[X])
      (eval₂ C q
        ((derivative : (a : R[X]) → R[X])
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n) * X)))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
rw₅ :
  HMul.hMul (β := R[X])
          (eval₂ C q
            ((derivative : (a : R[X]) → R[X])
              (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))))
          ((derivative : (a : R[X]) → R[X]) q : R[X]) *
        q +
      HMul.hMul (β := R[X])
        (eval₂ C q (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)))
        ((derivative : (a : R[X]) → R[X]) q : R[X]) =
    HMul.hMul (β := R[X])
      (eval₂ C q
        ((derivative : (a : R[X]) → R[X])
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n) * X)))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
rw₆ :
  HMul.hMul (β := R[X])
          (eval₂ C q
            ((derivative : (a : R[X]) → R[X])
              (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))))
          ((derivative : (a : R[X]) → R[X]) q : R[X]) *
        q +
      HMul.hMul (β := R[X])
        (eval₂ C q (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)))
        ((derivative : (a : R[X]) → R[X]) q : R[X]) =
    HMul.hMul (β := R[X])
      (eval₂ C q
        (HMul.hMul (α := R[X]) (β := R[X])
            ((derivative : (a : R[X]) → R[X])
                (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)) :
              R[X])
            X +
          HMul.hMul (β := R[X]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))
            ((derivative : (a : R[X]) → R[X]) X : R[X])))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
rw₇ :
  HMul.hMul (β := R[X])
          (eval₂ C q
            ((derivative : (a : R[X]) → R[X])
              (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))))
          ((derivative : (a : R[X]) → R[X]) q : R[X]) *
        q +
      HMul.hMul (β := R[X])
        (eval₂ C q (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)))
        ((derivative : (a : R[X]) → R[X]) q : R[X]) =
    HMul.hMul (β := R[X])
      (eval₂ C q
        (HMul.hMul (α := R[X]) (β := R[X])
            ((derivative : (a : R[X]) → R[X])
                (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)) :
              R[X])
            X +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n) * 1))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
⊢ (derivative : (a : R[X]) → R[X])
      (eval₂ C q (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))) =
    HMul.hMul (β := R[X])
      (eval₂ C q
        ((derivative : (a : R[X]) → R[X])
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
have rw₈ : HMul.hMul (β := R[X])
        (eval₂ C q
          ((derivative : (a : R[X]) → R[X])
            (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))))
        ((derivative : (a : R[X]) → R[X]) q : R[X]) *
      q +
    HMul.hMul (β := R[X])
      (eval₂ C q (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)))
      ((derivative : (a : R[X]) → R[X]) q : R[X]) =
  HMul.hMul (β := R[X])
    (eval₂ C q
      (HMul.hMul (α := R[X]) (β := R[X])
          ((derivative : (a : R[X]) → R[X])
              (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)) :
            R[X])
          X +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)))
    ((derivative : (a : R[X]) → R[X]) q : R[X])
Tactic: rw [pow_succ, ← mul_assoc, eval₂_mul, eval₂_X, derivative_mul, ih, @derivative_mul _ _ _ X,
      derivative_X, mul_one, eval₂_add, @eval₂_mul _ _ _ _ X, eval₂_X, add_mul, mul_right_comm]