no goals
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝² : CommRing R
p✝ q✝ : R[X]
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : R[X]
hq : Monic q
x : S
hx : ↑(aeval x) q = 0
⊢ ↑(aeval x) (p %ₘ q) = ↑(aeval x) p
rw [modByMonic_eq_sub_mul_div p hq, _root_.map_sub, _root_.map_mul, hx, MulZeroClass.zero_mul,
  sub_zero]