case hom_inv_id
C : Type u
inst✝¹ : Category C
X Y Z : C
f g : X ⟶ Y
h : Y ⟶ Z
inst✝ : IsIso f
⊢ inv f ≫ f = 𝟙 Y
C : Type u
inst✝¹ : Category C
X Y Z : C
f g : X ⟶ Y
h : Y ⟶ Z
inst✝ : IsIso f
⊢ inv (inv f) = f
apply inv_eq_of_hom_inv_id
no goals
case hom_inv_id
C : Type u
inst✝¹ : Category C
X Y Z : C
f g : X ⟶ Y
h : Y ⟶ Z
inst✝ : IsIso f
⊢ inv f ≫ f = 𝟙 Y
simp