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