fix: remove redundant @[simp] on backwardDiff_X/C

With @[expose], simp can already prove these from the definition,
making the @[simp] tags redundant (linter error).

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: RaggedR

Mathlib/RingTheory/HopfAlgebra/AscPochhammer.lean

@@ -54,11 +54,9 @@ theorem backwardDiff_apply (p : R[X]) :
     backwardDiff p = p - taylor (-1 : R) p := by
   simp [backwardDiff]
 
-@[simp]
 theorem backwardDiff_X : backwardDiff (X : R[X]) = (1 : R[X]) := by
   simp [taylor_X]
 
-@[simp]
 theorem backwardDiff_C (r : R) : backwardDiff (C r : R[X]) = 0 := by
   simp [taylor_C]