no goals
A : Type ?u.279774
K : Type ?u.279777
R : Type u_2
S : Type u_1
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : CommRing R
inst✝ : CommRing S
M : Submonoid A
p : S[X]
f : S →+* R
r : R
s : S
hr : eval₂ f r p = 0
⊢ eval₂ f (↑f s * r) (scaleRoots p s) = 0
rw [scaleRoots_eval₂_mul, hr, mul_zero]