no goals
A : Type ?u.197411
B : Type ?u.197414
inst✝⁹ : Field A
inst✝⁸ : Ring B
inst✝⁷ : Algebra A B
x✝ : B
K : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : Field K
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra K S
inst✝² : Algebra K T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower K S T
hST : Injective ↑(algebraMap S T)
x : S
y : T
hx : IsIntegral K x
h : y = ↑(algebraMap S T) x
⊢ ↑(Polynomial.aeval y) (minpoly K x) = 0
rw [h, aeval_algebraMap_apply, minpoly.aeval, RingHom.map_zero]