case h
R✝ : Type u
inst✝¹ : CommRing R✝
I✝ : Ideal R✝
a b : R✝
S : Type v
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
h : I = J
x✝ : R ⧸ J
⊢ ↑(RingEquiv.symm (quotEquivOfEq h)) x✝ = ↑(quotEquivOfEq (_ : J = I)) x✝
R✝ : Type u
inst✝¹ : CommRing R✝
I✝ : Ideal R✝
a b : R✝
S : Type v
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
h : I = J
⊢ RingEquiv.symm (quotEquivOfEq h) = quotEquivOfEq (_ : J = I)
ext
no goals
case h
R✝ : Type u
inst✝¹ : CommRing R✝
I✝ : Ideal R✝
a b : R✝
S : Type v
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
h : I = J
x✝ : R ⧸ J
⊢ ↑(RingEquiv.symm (quotEquivOfEq h)) x✝ = ↑(quotEquivOfEq (_ : J = I)) x✝
rfl