no goals
R : Type u
S : Type v
K : Type w
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pb : PowerBasis R S
I : Ideal R
g : R[X]
⊢ ↑(AlgEquiv.symm (quotientEquivQuotientMinpolyMap pb I))
      (↑(Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)}))
        (Polynomial.map (Ideal.Quotient.mk I) g)) =
    ↑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) (↑(aeval pb.gen) g)
simp only [quotientEquivQuotientMinpolyMap, toRingEquiv_eq_coe, symm_trans_apply,
  quotEquivQuotMap_symm_apply_mk, ofRingEquiv_symm_apply, quotientEquiv_symm_mk,
  toRingEquiv_symm, RingEquiv.symm_symm, AdjoinRoot.equiv'_apply, coe_ringEquiv, liftHom_mk,
  symm_toRingEquiv]