no goals
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
pb : PowerBasis K L
f : K[X]
⊢ ↑(AlgEquiv.symm (equivAdjoinSimple pb)) (↑(aeval pb.gen) f) = ↑(aeval (AdjoinSimple.gen K pb.gen)) f
rw [equivAdjoinSimple, equivOfMinpoly_symm, equivOfMinpoly_aeval, adjoin.powerBasis_gen]