case h
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
I J : Ideal R
coprime : I ⊔ J = ⊤
⊢ RingHom.comp (RingHom.comp (RingHom.snd (R ⧸ I) (R ⧸ J)) ↑(quotientInfEquivQuotientProd I J coprime))
      (Quotient.mk (I ⊓ J)) =
    RingHom.comp (Quotient.factor (I ⊓ J) J (_ : I ⊓ J ≤ J)) (Quotient.mk (I ⊓ J))
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
I J : Ideal R
coprime : I ⊔ J = ⊤
⊢ RingHom.comp (RingHom.snd (R ⧸ I) (R ⧸ J)) ↑(quotientInfEquivQuotientProd I J coprime) =
    Quotient.factor (I ⊓ J) J (_ : I ⊓ J ≤ J)
apply Quotient.ringHom_ext
case h.a
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
I J : Ideal R
coprime : I ⊔ J = ⊤
x✝ : R
⊢ ↑(RingHom.comp (RingHom.comp (RingHom.snd (R ⧸ I) (R ⧸ J)) ↑(quotientInfEquivQuotientProd I J coprime))
          (Quotient.mk (I ⊓ J)))
      x✝ =
    ↑(RingHom.comp (Quotient.factor (I ⊓ J) J (_ : I ⊓ J ≤ J)) (Quotient.mk (I ⊓ J))) x✝
case h
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
I J : Ideal R
coprime : I ⊔ J = ⊤
⊢ RingHom.comp (RingHom.comp (RingHom.snd (R ⧸ I) (R ⧸ J)) ↑(quotientInfEquivQuotientProd I J coprime))
      (Quotient.mk (I ⊓ J)) =
    RingHom.comp (Quotient.factor (I ⊓ J) J (_ : I ⊓ J ≤ J)) (Quotient.mk (I ⊓ J))
ext
no goals
case h.a
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
I J : Ideal R
coprime : I ⊔ J = ⊤
x✝ : R
⊢ ↑(RingHom.comp (RingHom.comp (RingHom.snd (R ⧸ I) (R ⧸ J)) ↑(quotientInfEquivQuotientProd I J coprime))
          (Quotient.mk (I ⊓ J)))
      x✝ =
    ↑(RingHom.comp (Quotient.factor (I ⊓ J) J (_ : I ⊓ J ≤ J)) (Quotient.mk (I ⊓ J))) x✝
rfl