C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
h : IsColimit (CokernelCofork.ofπ g w)
⊢ kernel.ι g ≫ cokernel.π f = 0
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
h : IsColimit (CokernelCofork.ofπ g w)
⊢ Exact f g
refine' (exact_iff _ _).2 ⟨w, _⟩
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
h : IsColimit (CokernelCofork.ofπ g w)
this :
  (CokernelCofork.ofπ g w).ι.app WalkingParallelPair.one ≫
      IsColimit.desc h (CokernelCofork.ofπ (cokernel.π f) (_ : f ≫ cokernel.π f = 0)) =
    (CokernelCofork.ofπ (cokernel.π f) (_ : f ≫ cokernel.π f = 0)).ι.app WalkingParallelPair.one
⊢ kernel.ι g ≫ cokernel.π f = 0
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
h : IsColimit (CokernelCofork.ofπ g w)
⊢ kernel.ι g ≫ cokernel.π f = 0
have := h.fac (CokernelCofork.ofπ _ (cokernel.condition f)) WalkingParallelPair.one
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
h : IsColimit (CokernelCofork.ofπ g w)
this : g ≫ IsColimit.desc h (CokernelCofork.ofπ (cokernel.π f) (_ : f ≫ cokernel.π f = 0)) = cokernel.π f
⊢ kernel.ι g ≫ cokernel.π f = 0
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
h : IsColimit (CokernelCofork.ofπ g w)
this :
  (CokernelCofork.ofπ g w).ι.app WalkingParallelPair.one ≫
      IsColimit.desc h (CokernelCofork.ofπ (cokernel.π f) (_ : f ≫ cokernel.π f = 0)) =
    (CokernelCofork.ofπ (cokernel.π f) (_ : f ≫ cokernel.π f = 0)).ι.app WalkingParallelPair.one
⊢ kernel.ι g ≫ cokernel.π f = 0
simp only [Cofork.ofπ_ι_app] at this
no goals
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
h : IsColimit (CokernelCofork.ofπ g w)
this : g ≫ IsColimit.desc h (CokernelCofork.ofπ (cokernel.π f) (_ : f ≫ cokernel.π f = 0)) = cokernel.π f
⊢ kernel.ι g ≫ cokernel.π f = 0
rw [← this, ← Category.assoc, kernel.condition, zero_comp]