case h
R : Type u
A : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommRing A
inst✝ : Algebra R A
I J : Ideal A
a✝ : (A ⧸ J) ⧸ map (Quotient.mkₐ R J) I
⊢ ↑(AlgEquiv.symm (quotQuotEquivCommₐ R I J)) a✝ = ↑(quotQuotEquivCommₐ R J I) a✝
R : Type u
A : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommRing A
inst✝ : Algebra R A
I J : Ideal A
⊢ AlgEquiv.symm (quotQuotEquivCommₐ R I J) = quotQuotEquivCommₐ R J I
ext
case h
R : Type u
A : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommRing A
inst✝ : Algebra R A
I J : Ideal A
a✝ : (A ⧸ J) ⧸ map (Quotient.mkₐ R J) I
⊢ ↑(AlgEquiv.symm
          (AlgEquiv.ofRingEquiv
            (_ :
              ∀ (x : R),
                ↑(quotQuotEquivComm I J) (↑(algebraMap R ((A ⧸ I) ⧸ map (Quotient.mkₐ R I) J)) x) =
                  ↑(quotQuotEquivComm I J) (↑(algebraMap R ((A ⧸ I) ⧸ map (Quotient.mkₐ R I) J)) x))))
      a✝ =
    ↑(AlgEquiv.ofRingEquiv
          (_ :
            ∀ (x : R),
              ↑(quotQuotEquivComm J I) (↑(algebraMap R ((A ⧸ J) ⧸ map (Quotient.mkₐ R J) I)) x) =
                ↑(quotQuotEquivComm J I) (↑(algebraMap R ((A ⧸ J) ⧸ map (Quotient.mkₐ R J) I)) x)))
      a✝
case h
R : Type u
A : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommRing A
inst✝ : Algebra R A
I J : Ideal A
a✝ : (A ⧸ J) ⧸ map (Quotient.mkₐ R J) I
⊢ ↑(AlgEquiv.symm (quotQuotEquivCommₐ R I J)) a✝ = ↑(quotQuotEquivCommₐ R J I) a✝
unfold quotQuotEquivCommₐ
no goals
case h
R : Type u
A : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommRing A
inst✝ : Algebra R A
I J : Ideal A
a✝ : (A ⧸ J) ⧸ map (Quotient.mkₐ R J) I
⊢ ↑(AlgEquiv.symm
          (AlgEquiv.ofRingEquiv
            (_ :
              ∀ (x : R),
                ↑(quotQuotEquivComm I J) (↑(algebraMap R ((A ⧸ I) ⧸ map (Quotient.mkₐ R I) J)) x) =
                  ↑(quotQuotEquivComm I J) (↑(algebraMap R ((A ⧸ I) ⧸ map (Quotient.mkₐ R I) J)) x))))
      a✝ =
    ↑(AlgEquiv.ofRingEquiv
          (_ :
            ∀ (x : R),
              ↑(quotQuotEquivComm J I) (↑(algebraMap R ((A ⧸ J) ⧸ map (Quotient.mkₐ R J) I)) x) =
                ↑(quotQuotEquivComm J I) (↑(algebraMap R ((A ⧸ J) ⧸ map (Quotient.mkₐ R J) I)) x)))
      a✝
congr