case h.e'_3
R S : CommRingCat
f : R ≅ S
a : ↑R
ha : IsUnit (↑f.hom a)
⊢ a = ↑f.inv (↑f.hom a)
R S : CommRingCat
f : R ≅ S
a : ↑R
ha : IsUnit (↑f.hom a)
⊢ IsUnit a
convert f.inv.isUnit_map ha
no goals
case h.e'_3
R S : CommRingCat
f : R ≅ S
a : ↑R
ha : IsUnit (↑f.hom a)
⊢ a = ↑f.inv (↑f.hom a)
exact (RingHom.congr_fun f.hom_inv_id _).symm