no goals
R : Type u_3
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type ?u.47235
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
R' : Type u_2
inst✝ : CommRing R'
g : S →+* R'
p : S[X]
x : R'
hx : eval₂ g x p = 0
b : { x // x ∈ M }
hb : Polynomial.map (algebraMap R S) (integerNormalization M p) = ↑b • p
⊢ eval₂ g x (Polynomial.map (algebraMap R S) (integerNormalization M p)) = 0
rw [hb, ← IsScalarTower.algebraMap_smul S (b : R) p, eval₂_smul, hx, MulZeroClass.mul_zero]