case hom_inv_id
α : Type u
inst✝ : Group α
x y : SingleObj α
f : x ⟶ y
⊢ f ≫ f⁻¹ = 𝟙 x
α : Type u
inst✝ : Group α
x y : SingleObj α
f : x ⟶ y
⊢ inv f = f⁻¹
apply IsIso.inv_eq_of_hom_inv_id
no goals
case hom_inv_id
α : Type u
inst✝ : Group α
x y : SingleObj α
f : x ⟶ y
⊢ f ≫ f⁻¹ = 𝟙 x
rw [comp_as_mul, inv_mul_self, id_as_one]