case a
X Y : CommRingCat
i : X ≅ Y
x✝ : ↑Y
⊢ ↑(RingEquiv.toRingHom (RingEquiv.symm (commRingCatIsoToRingEquiv i))) x✝ = ↑i.inv x✝
X Y : CommRingCat
i : X ≅ Y
⊢ RingEquiv.toRingHom (RingEquiv.symm (commRingCatIsoToRingEquiv i)) = i.inv
ext
no goals
case a
X Y : CommRingCat
i : X ≅ Y
x✝ : ↑Y
⊢ ↑(RingEquiv.toRingHom (RingEquiv.symm (commRingCatIsoToRingEquiv i))) x✝ = ↑i.inv x✝
rfl