no goals
R : Type ?u.210961
S : Type u_2
T : Type ?u.210967
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_1
B : Type ?u.211273
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type ?u.211695
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_3
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : ↑(aeval y) (minpoly A pb.gen) = 0
⊢ ↑(↑(Basis.constr pb.basis A) fun i => y ^ ↑i) pb.gen = y
convert pb.constr_pow_aeval hy X <;> rw [aeval_X]