case a
R : Type u
inst✝ : CommRing R
I J : Ideal R
h : I ≤ J
x✝ : R
⊢ ↑(RingHom.comp (↑(RingEquiv.symm (quotQuotEquivQuotOfLE h))) (Ideal.Quotient.mk J)) x✝ = ↑(quotQuotMk I J) x✝
R : Type u
inst✝ : CommRing R
I J : Ideal R
h : I ≤ J
⊢ RingHom.comp (↑(RingEquiv.symm (quotQuotEquivQuotOfLE h))) (Ideal.Quotient.mk J) = quotQuotMk I J
ext
no goals
case a
R : Type u
inst✝ : CommRing R
I J : Ideal R
h : I ≤ J
x✝ : R
⊢ ↑(RingHom.comp (↑(RingEquiv.symm (quotQuotEquivQuotOfLE h))) (Ideal.Quotient.mk J)) x✝ = ↑(quotQuotMk I J) x✝
rfl