no goals
R : Type u
S : Type v
K : Type w
inst✝ : CommRing R
I : Ideal R
f p : R[X]
⊢ ↑(quotQuotEquivComm I f)
      (↑(Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) f})) (Polynomial.map (Ideal.Quotient.mk I) p)) =
    ↑(Ideal.Quotient.mk (span {↑(Ideal.Quotient.mk (Ideal.map C I)) f})) (↑(Ideal.Quotient.mk (Ideal.map C I)) p)
simp only [Polynomial.quotQuotEquivComm, quotientEquiv_mk,
  polynomialQuotientEquivQuotientPolynomial_map_mk]