C : Type u
inst✝² : Category C
X✝ Y✝ Z✝ : C
f✝ g✝ : X✝ ⟶ Y✝
h : Y✝ ⟶ Z✝
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsIso f
inst✝ : IsIso (f ≫ g)
⊢ IsIso (inv f ≫ f ≫ g)
C : Type u
inst✝² : Category C
X✝ Y✝ Z✝ : C
f✝ g✝ : X✝ ⟶ Y✝
h : Y✝ ⟶ Z✝
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsIso f
inst✝ : IsIso (f ≫ g)
⊢ IsIso g
rw [← id_comp g, ← inv_hom_id f, assoc]
no goals
C : Type u
inst✝² : Category C
X✝ Y✝ Z✝ : C
f✝ g✝ : X✝ ⟶ Y✝
h : Y✝ ⟶ Z✝
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsIso f
inst✝ : IsIso (f ≫ g)
⊢ IsIso (inv f ≫ f ≫ g)
infer_instance