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