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]
⊢ ↑(quotientEquivQuotientMinpolyMap pb I) (↑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) (↑(aeval pb.gen) g)) =
    ↑(Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)}))
      (Polynomial.map (Ideal.Quotient.mk I) g)
rw [PowerBasis.quotientEquivQuotientMinpolyMap, AlgEquiv.trans_apply, AlgEquiv.ofRingEquiv_apply,
  quotientEquiv_mk, AlgEquiv.coe_ringEquiv', AdjoinRoot.equiv'_symm_apply, PowerBasis.lift_aeval,
  AdjoinRoot.aeval_eq, AdjoinRoot.quotEquivQuotMap_apply_mk]