no goals
R : Type u_2
A : Type u_1
B : Type ?u.734629
S : Type ?u.734632
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
x : { x // x ∈ integralClosure R A }
p : R[X]
hpm : Monic p
hpx : eval₂ (algebraMap R A) (↑x) p = 0
⊢ ↑(eval₂ (algebraMap R { x // x ∈ integralClosure R A }) x p) = ↑0
rwa [← aeval_def, ← Subalgebra.val_apply, aeval_algHom_apply] at hpx