C : Type u₁
inst✝² : Category C
inst✝¹ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
W : C
h : W ⟶ X
inst✝ : Epi h
hfg : Exact (h ≫ f) g
⊢ Exact f g
C : Type u₁
inst✝² : Category C
inst✝¹ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
W : C
h : W ⟶ X
inst✝ : Epi h
⊢ Exact (h ≫ f) g ↔ Exact f g
refine' ⟨fun hfg => _, fun h => exact_epi_comp h⟩
C : Type u₁
inst✝² : Category C
inst✝¹ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
W : C
h : W ⟶ X
inst✝ : Epi h
hfg : Exact (h ≫ f) g
hc : IsColimit
  (CokernelCofork.ofπ (Cofork.π (colimit.cocone (parallelPair (h ≫ f) 0)))
    (_ : f ≫ Cofork.π (colimit.cocone (parallelPair (h ≫ f) 0)) = 0)) :=
  isCokernelOfComp h (h ≫ f) (colimit.isColimit (parallelPair (h ≫ f) 0))
    (_ : f ≫ Cofork.π (colimit.cocone (parallelPair (h ≫ f) 0)) = 0) (_ : h ≫ f = h ≫ f)
⊢ Exact f g
C : Type u₁
inst✝² : Category C
inst✝¹ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
W : C
h : W ⟶ X
inst✝ : Epi h
hfg : Exact (h ≫ f) g
⊢ Exact f g
let hc := isCokernelOfComp _ _ (colimit.isColimit (parallelPair (h ≫ f) 0))
  (by rw [← cancel_epi h, ← Category.assoc, CokernelCofork.condition, comp_zero]) rfl
C : Type u₁
inst✝² : Category C
inst✝¹ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
W : C
h : W ⟶ X
inst✝ : Epi h
hfg : Exact (h ≫ f) g
hc : IsColimit
  (CokernelCofork.ofπ (Cofork.π (colimit.cocone (parallelPair (h ≫ f) 0)))
    (_ : f ≫ Cofork.π (colimit.cocone (parallelPair (h ≫ f) 0)) = 0)) :=
  isCokernelOfComp h (h ≫ f) (colimit.isColimit (parallelPair (h ≫ f) 0))
    (_ : f ≫ Cofork.π (colimit.cocone (parallelPair (h ≫ f) 0)) = 0) (_ : h ≫ f = h ≫ f)
⊢ f ≫ g = 0
C : Type u₁
inst✝² : Category C
inst✝¹ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
W : C
h : W ⟶ X
inst✝ : Epi h
hfg : Exact (h ≫ f) g
hc : IsColimit
  (CokernelCofork.ofπ (Cofork.π (colimit.cocone (parallelPair (h ≫ f) 0)))
    (_ : f ≫ Cofork.π (colimit.cocone (parallelPair (h ≫ f) 0)) = 0)) :=
  isCokernelOfComp h (h ≫ f) (colimit.isColimit (parallelPair (h ≫ f) 0))
    (_ : f ≫ Cofork.π (colimit.cocone (parallelPair (h ≫ f) 0)) = 0) (_ : h ≫ f = h ≫ f)
⊢ Exact f g
refine' (exact_iff' _ _ (limit.isLimit _) hc).2 ⟨_, ((exact_iff _ _).1 hfg).2⟩
no goals
C : Type u₁
inst✝² : Category C
inst✝¹ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
W : C
h : W ⟶ X
inst✝ : Epi h
hfg : Exact (h ≫ f) g
hc : IsColimit
  (CokernelCofork.ofπ (Cofork.π (colimit.cocone (parallelPair (h ≫ f) 0)))
    (_ : f ≫ Cofork.π (colimit.cocone (parallelPair (h ≫ f) 0)) = 0)) :=
  isCokernelOfComp h (h ≫ f) (colimit.isColimit (parallelPair (h ≫ f) 0))
    (_ : f ≫ Cofork.π (colimit.cocone (parallelPair (h ≫ f) 0)) = 0) (_ : h ≫ f = h ≫ f)
⊢ f ≫ g = 0
exact zero_of_epi_comp h (by rw [← hfg.1, Category.assoc])
no goals
C : Type u₁
inst✝² : Category C
inst✝¹ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
W : C
h : W ⟶ X
inst✝ : Epi h
hfg : Exact (h ≫ f) g
⊢ f ≫ Cofork.π (colimit.cocone (parallelPair (h ≫ f) 0)) = 0
rw [← cancel_epi h, ← Category.assoc, CokernelCofork.condition, comp_zero]
no goals
C : Type u₁
inst✝² : Category C
inst✝¹ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
W : C
h : W ⟶ X
inst✝ : Epi h
hfg : Exact (h ≫ f) g
hc : IsColimit
  (CokernelCofork.ofπ (Cofork.π (colimit.cocone (parallelPair (h ≫ f) 0)))
    (_ : f ≫ Cofork.π (colimit.cocone (parallelPair (h ≫ f) 0)) = 0)) :=
  isCokernelOfComp h (h ≫ f) (colimit.isColimit (parallelPair (h ≫ f) 0))
    (_ : f ≫ Cofork.π (colimit.cocone (parallelPair (h ≫ f) 0)) = 0) (_ : h ≫ f = h ≫ f)
⊢ h ≫ f ≫ g = 0
rw [← hfg.1, Category.assoc]