no goals
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
I✝ : Ideal R
f✝ f g : R[X]
I : Ideal R
⊢ ↑(AlgEquiv.symm (quotEquivQuotMap f I))
      (↑(Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) f})) (Polynomial.map (Ideal.Quotient.mk I) g)) =
    ↑(Ideal.Quotient.mk (Ideal.map (of f) I)) (↑(mk f) g)
rw [AdjoinRoot.quotEquivQuotMap_symm_apply,
  AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot_symm_mk_mk]