no goals
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : CommRing R
p✝ q✝ : R[X]
inst✝ : CommRing S
f : R →+* S
p q : R[X]
hq : Monic q
x : S
hx : eval₂ f x q = 0
⊢ eval₂ f x (p %ₘ q) = eval₂ f x p
rw [modByMonic_eq_sub_mul_div p hq, eval₂_sub, eval₂_mul, hx, MulZeroClass.zero_mul, sub_zero]