case a
R : Type u_1
inst✝ : CommRing R
I : Ideal R
f : R[X]
⊢ ↑(RingEquiv.symm (polynomialQuotientEquivQuotientPolynomial I))
      (↑(polynomialQuotientEquivQuotientPolynomial I) (Polynomial.map (Quotient.mk I) f)) =
    ↑(RingEquiv.symm (polynomialQuotientEquivQuotientPolynomial I)) (↑(Quotient.mk (map C I)) f)
R : Type u_1
inst✝ : CommRing R
I : Ideal R
f : R[X]
⊢ ↑(polynomialQuotientEquivQuotientPolynomial I) (Polynomial.map (Quotient.mk I) f) = ↑(Quotient.mk (map C I)) f
apply (polynomialQuotientEquivQuotientPolynomial I).symm.injective
no goals
case a
R : Type u_1
inst✝ : CommRing R
I : Ideal R
f : R[X]
⊢ ↑(RingEquiv.symm (polynomialQuotientEquivQuotientPolynomial I))
      (↑(polynomialQuotientEquivQuotientPolynomial I) (Polynomial.map (Quotient.mk I) f)) =
    ↑(RingEquiv.symm (polynomialQuotientEquivQuotientPolynomial I)) (↑(Quotient.mk (map C I)) f)
rw [RingEquiv.symm_apply_apply, polynomialQuotientEquivQuotientPolynomial_symm_mk]