case h
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_2
R₂ : Type ?u.1696123
A : Type u_1
B : Type ?u.1696129
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
I J : Ideal A
h : I = J
a✝ : A ⧸ J
⊢ ↑(AlgEquiv.symm (quotientEquivAlgOfEq R₁ h)) a✝ = ↑(quotientEquivAlgOfEq R₁ (_ : J = I)) a✝
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_2
R₂ : Type ?u.1696123
A : Type u_1
B : Type ?u.1696129
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
I J : Ideal A
h : I = J
⊢ AlgEquiv.symm (quotientEquivAlgOfEq R₁ h) = quotientEquivAlgOfEq R₁ (_ : J = I)
ext
no goals
case h
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_2
R₂ : Type ?u.1696123
A : Type u_1
B : Type ?u.1696129
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
I J : Ideal A
h : I = J
a✝ : A ⧸ J
⊢ ↑(AlgEquiv.symm (quotientEquivAlgOfEq R₁ h)) a✝ = ↑(quotientEquivAlgOfEq R₁ (_ : J = I)) a✝
rfl