no goals
R✝ : Type u
S : Type v
T : Type w
ι : Type y
a b : R✝
m n : ℕ
inst✝² : CommSemiring R✝
inst✝¹ : CommSemiring S
f✝ : R✝ →+* S
R : Type u_1
inst✝ : CommRing R
f : R →+* S
x : R
p : R[X]
h : IsRoot (Polynomial.map f p) (↑f x)
hf : Function.Injective ↑f
⊢ IsRoot p x
rwa [IsRoot, ← (injective_iff_map_eq_zero' f).mp hf, ← eval₂_hom, ← eval_map]