no goals
R : Type u_1
inst✝ : CommRing R
I : Ideal R
f : R[X]
⊢ ↑(RingEquiv.symm (polynomialQuotientEquivQuotientPolynomial I)) (↑(Quotient.mk (map C I)) f) =
    Polynomial.map (Quotient.mk I) f
rw [polynomialQuotientEquivQuotientPolynomial, RingEquiv.symm_mk, RingEquiv.coe_mk,
  Equiv.coe_fn_mk, Quotient.lift_mk, coe_eval₂RingHom, eval₂_eq_eval_map, ← Polynomial.map_map,
  ← eval₂_eq_eval_map, Polynomial.eval₂_C_X]