R : Type u
inst✝ : CommRing R
I J : Ideal R
⊢ RingEquiv.symm
      (RingEquiv.trans (RingEquiv.trans (quotQuotEquivQuotSup I J) (quotEquivOfEq (_ : I ⊔ J = J ⊔ I)))
        (RingEquiv.symm (quotQuotEquivQuotSup J I))) =
    RingEquiv.trans (RingEquiv.trans (quotQuotEquivQuotSup J I) (quotEquivOfEq (_ : J ⊔ I = I ⊔ J)))
      (RingEquiv.symm (quotQuotEquivQuotSup I J))
R : Type u
inst✝ : CommRing R
I J : Ideal R
⊢ RingEquiv.symm (quotQuotEquivComm I J) = quotQuotEquivComm J I
change (((quotQuotEquivQuotSup I J).trans (quotEquivOfEq (sup_comm))).trans
  (quotQuotEquivQuotSup J I).symm).symm =
    ((quotQuotEquivQuotSup J I).trans (quotEquivOfEq (sup_comm))).trans
      (quotQuotEquivQuotSup I J).symm
case h
R : Type u
inst✝ : CommRing R
I J : Ideal R
r : (R ⧸ J) ⧸ map (Ideal.Quotient.mk J) I
⊢ ↑(RingEquiv.symm
          (RingEquiv.trans (RingEquiv.trans (quotQuotEquivQuotSup I J) (quotEquivOfEq (_ : I ⊔ J = J ⊔ I)))
            (RingEquiv.symm (quotQuotEquivQuotSup J I))))
      r =
    ↑(RingEquiv.trans (RingEquiv.trans (quotQuotEquivQuotSup J I) (quotEquivOfEq (_ : J ⊔ I = I ⊔ J)))
          (RingEquiv.symm (quotQuotEquivQuotSup I J)))
      r
R : Type u
inst✝ : CommRing R
I J : Ideal R
⊢ RingEquiv.symm
      (RingEquiv.trans (RingEquiv.trans (quotQuotEquivQuotSup I J) (quotEquivOfEq (_ : I ⊔ J = J ⊔ I)))
        (RingEquiv.symm (quotQuotEquivQuotSup J I))) =
    RingEquiv.trans (RingEquiv.trans (quotQuotEquivQuotSup J I) (quotEquivOfEq (_ : J ⊔ I = I ⊔ J)))
      (RingEquiv.symm (quotQuotEquivQuotSup I J))
ext r
case h
R : Type u
inst✝ : CommRing R
I J : Ideal R
r : (R ⧸ J) ⧸ map (Ideal.Quotient.mk J) I
⊢ ↑(RingEquiv.symm (quotQuotEquivQuotSup I J))
      (↑(RingEquiv.symm (quotEquivOfEq (_ : I ⊔ J = J ⊔ I)))
        (↑(RingEquiv.symm (RingEquiv.symm (quotQuotEquivQuotSup J I))) r)) =
    ↑(RingEquiv.symm (quotQuotEquivQuotSup I J)) (↑(quotEquivOfEq (_ : J ⊔ I = I ⊔ J)) (↑(quotQuotEquivQuotSup J I) r))
case h
R : Type u
inst✝ : CommRing R
I J : Ideal R
r : (R ⧸ J) ⧸ map (Ideal.Quotient.mk J) I
⊢ ↑(RingEquiv.symm
          (RingEquiv.trans (RingEquiv.trans (quotQuotEquivQuotSup I J) (quotEquivOfEq (_ : I ⊔ J = J ⊔ I)))
            (RingEquiv.symm (quotQuotEquivQuotSup J I))))
      r =
    ↑(RingEquiv.trans (RingEquiv.trans (quotQuotEquivQuotSup J I) (quotEquivOfEq (_ : J ⊔ I = I ⊔ J)))
          (RingEquiv.symm (quotQuotEquivQuotSup I J)))
      r
dsimp
no goals
case h
R : Type u
inst✝ : CommRing R
I J : Ideal R
r : (R ⧸ J) ⧸ map (Ideal.Quotient.mk J) I
⊢ ↑(RingEquiv.symm (quotQuotEquivQuotSup I J))
      (↑(RingEquiv.symm (quotEquivOfEq (_ : I ⊔ J = J ⊔ I)))
        (↑(RingEquiv.symm (RingEquiv.symm (quotQuotEquivQuotSup J I))) r)) =
    ↑(RingEquiv.symm (quotQuotEquivQuotSup I J)) (↑(quotEquivOfEq (_ : J ⊔ I = I ⊔ J)) (↑(quotQuotEquivQuotSup J I) r))
rfl