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