C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
h : IsLimit (KernelFork.ofι f 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 : IsLimit (KernelFork.ofι f 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 : IsLimit (KernelFork.ofι f w)
this :
  IsLimit.lift h (KernelFork.ofι (kernel.ι g) (_ : kernel.ι g ≫ g = 0)) ≫
      (KernelFork.ofι f w).π.app WalkingParallelPair.zero =
    (KernelFork.ofι (kernel.ι g) (_ : kernel.ι g ≫ g = 0)).π.app WalkingParallelPair.zero
⊢ 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 : IsLimit (KernelFork.ofι f w)
⊢ kernel.ι g ≫ cokernel.π f = 0
have := h.fac (KernelFork.ofι _ (kernel.condition g)) WalkingParallelPair.zero
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
h : IsLimit (KernelFork.ofι f w)
this : IsLimit.lift h (KernelFork.ofι (kernel.ι g) (_ : kernel.ι g ≫ g = 0)) ≫ f = kernel.ι g
⊢ 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 : IsLimit (KernelFork.ofι f w)
this :
  IsLimit.lift h (KernelFork.ofι (kernel.ι g) (_ : kernel.ι g ≫ g = 0)) ≫
      (KernelFork.ofι f w).π.app WalkingParallelPair.zero =
    (KernelFork.ofι (kernel.ι g) (_ : kernel.ι g ≫ g = 0)).π.app WalkingParallelPair.zero
⊢ kernel.ι g ≫ cokernel.π f = 0
simp only [Fork.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 : IsLimit (KernelFork.ofι f w)
this : IsLimit.lift h (KernelFork.ofι (kernel.ι g) (_ : kernel.ι g ≫ g = 0)) ≫ f = kernel.ι g
⊢ kernel.ι g ≫ cokernel.π f = 0
rw [← this, Category.assoc, cokernel.condition, comp_zero]