V : Type u
inst✝⁴ : Category V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
inst✝ : IsIso f
w : Exact (f ≫ g) h
⊢ Exact (inv f ≫ f ≫ g) h
V : Type u
inst✝⁴ : Category V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
inst✝ : IsIso f
w : Exact (f ≫ g) h
⊢ Exact g h
rw [← IsIso.inv_hom_id_assoc f g]
no goals
V : Type u
inst✝⁴ : Category V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
inst✝ : IsIso f
w : Exact (f ≫ g) h
⊢ Exact (inv f ≫ f ≫ g) h
exact exact_epi_comp w