C : Type u
inst✝¹ : Category C
X Y Z : C
g : X ⟶ Y
inst✝ : IsIso g
f : Y ⟶ X
h : f ≫ g = 𝟙 Y
⊢ IsIso (inv g)
C : Type u
inst✝¹ : Category C
X Y Z : C
g : X ⟶ Y
inst✝ : IsIso g
f : Y ⟶ X
h : f ≫ g = 𝟙 Y
⊢ IsIso f
rw [(comp_hom_eq_id _).mp h]
no goals
C : Type u
inst✝¹ : Category C
X Y Z : C
g : X ⟶ Y
inst✝ : IsIso g
f : Y ⟶ X
h : f ≫ g = 𝟙 Y
⊢ IsIso (inv g)
infer_instance