no goals
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
I : Ideal R
f p : R[X]
⊢ ↑(RingEquiv.symm (quotAdjoinRootEquivQuotPolynomialQuot I f))
      (↑(Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) f})) (Polynomial.map (Ideal.Quotient.mk I) p)) =
    ↑(Ideal.Quotient.mk (Ideal.map (of f) I)) (↑(mk f) p)
rw [quotAdjoinRootEquivQuotPolynomialQuot, RingEquiv.symm_trans_apply,
  RingEquiv.symm_trans_apply, RingEquiv.symm_trans_apply, RingEquiv.symm_symm,
  Polynomial.quotQuotEquivComm_mk, Ideal.quotEquivOfEq_symm, Ideal.quotEquivOfEq_mk, ←
  RingHom.comp_apply, ← DoubleQuot.quotQuotMk,
  quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk_symm_quotQuotMk,
  quotMapOfEquivQuotMapCMapSpanMk_symm_mk]