-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
p q p₁ p₂ : R[X]
ih₁ :
  (derivative : (a : R[X]) → R[X]) (eval₂ C q p₁) =
    HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) p₁)) ((derivative : (a : R[X]) → R[X]) q : R[X])
ih₂ :
  (derivative : (a : R[X]) → R[X]) (eval₂ C q p₂) =
    HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) p₂)) ((derivative : (a : R[X]) → R[X]) q : R[X])
rw :
  (derivative : (a : R[X]) → R[X]) (eval₂ C q p₁ + eval₂ C q p₂) =
    HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) (p₁ + p₂)))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
rw₁ :
  HAdd.hAdd (α := R[X]) (β := R[X]) ((derivative : (a : R[X]) → R[X]) (eval₂ C q p₁) : R[X])
      ((derivative : (a : R[X]) → R[X]) (eval₂ C q p₂) : R[X]) =
    HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) (p₁ + p₂)))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
rw₂ :
  HAdd.hAdd (β := R[X])
      (HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) p₁))
        ((derivative : (a : R[X]) → R[X]) q : R[X]))
      ((derivative : (a : R[X]) → R[X]) (eval₂ C q p₂) : R[X]) =
    HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) (p₁ + p₂)))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
rw₃ :
  HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) p₁)) ((derivative : (a : R[X]) → R[X]) q : R[X]) +
      HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) p₂))
        ((derivative : (a : R[X]) → R[X]) q : R[X]) =
    HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) (p₁ + p₂)))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
rw₄ :
  HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) p₁)) ((derivative : (a : R[X]) → R[X]) q : R[X]) +
      HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) p₂))
        ((derivative : (a : R[X]) → R[X]) q : R[X]) =
    HMul.hMul (β := R[X])
      (eval₂ C q
        (HAdd.hAdd (α := R[X]) (β := R[X]) ((derivative : (a : R[X]) → R[X]) p₁ : R[X])
          ((derivative : (a : R[X]) → R[X]) p₂ : 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]) p₁)) ((derivative : (a : R[X]) → R[X]) q : R[X]) +
      HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) p₂))
        ((derivative : (a : R[X]) → R[X]) q : R[X]) =
    HMul.hMul (β := R[X])
      (eval₂ C q ((derivative : (a : R[X]) → R[X]) p₁) + eval₂ C q ((derivative : (a : R[X]) → R[X]) p₂))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
⊢ (derivative : (a : R[X]) → R[X]) (eval₂ C q (p₁ + p₂)) =
    HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) (p₁ + p₂)))
      ((derivative : (a : R[X]) → R[X]) q : R[X])
have rw₆ : HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) p₁)) ((derivative : (a : R[X]) → R[X]) q : R[X]) +
    HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) p₂))
      ((derivative : (a : R[X]) → R[X]) q : R[X]) =
  HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) p₁)) ((derivative : (a : R[X]) → R[X]) q : R[X]) +
    HMul.hMul (β := R[X]) (eval₂ C q ((derivative : (a : R[X]) → R[X]) p₂)) ((derivative : (a : R[X]) → R[X]) q : R[X])
Tactic: rw [eval₂_add, derivative_add, ih₁, ih₂, derivative_add, eval₂_add, add_mul]