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✝ : HasCokernels V
h : Exact f g
⊢ Subobject.arrow (kernelSubobject g) ≫ cokernel.π f = 0
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✝ : HasCokernels V
h : Exact f g
⊢ kernel.ι g ≫ cokernel.π f = 0
suffices Subobject.arrow (kernelSubobject g) ≫ cokernel.π f = 0 by
  rw [← kernelSubobject_arrow', Category.assoc, this, comp_zero]
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✝ : HasCokernels V
h : Exact f g
this : Epi (imageToKernel f g (_ : f ≫ g = 0))
⊢ Subobject.arrow (kernelSubobject g) ≫ cokernel.π f = 0
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✝ : HasCokernels V
h : Exact f g
⊢ Subobject.arrow (kernelSubobject g) ≫ cokernel.π f = 0
haveI := h.epi
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✝ : HasCokernels V
h : Exact f g
this : Epi (imageToKernel f g (_ : f ≫ g = 0))
⊢ imageToKernel f g (_ : f ≫ g = 0) ≫ Subobject.arrow (kernelSubobject g) ≫ cokernel.π f = 0
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✝ : HasCokernels V
h : Exact f g
this : Epi (imageToKernel f g (_ : f ≫ g = 0))
⊢ Subobject.arrow (kernelSubobject g) ≫ cokernel.π f = 0
apply zero_of_epi_comp (imageToKernel f g h.w) _
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✝ : HasCokernels V
h : Exact f g
this : Epi (imageToKernel f g (_ : f ≫ g = 0))
⊢ image.ι f ≫ cokernel.π f = (imageSubobjectIso f).inv ≫ 0
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✝ : HasCokernels V
h : Exact f g
this : Epi (imageToKernel f g (_ : f ≫ g = 0))
⊢ imageToKernel f g (_ : f ≫ g = 0) ≫ Subobject.arrow (kernelSubobject g) ≫ cokernel.π f = 0
rw [imageToKernel_arrow_assoc, ← imageSubobject_arrow, Category.assoc, ← Iso.eq_inv_comp]
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✝ : HasCokernels V
h : Exact f g
this : Epi (imageToKernel f g (_ : f ≫ g = 0))
⊢ image.ι f ≫ cokernel.π f = (imageSubobjectIso f).inv ≫ 0
aesop_cat
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✝ : HasCokernels V
h : Exact f g
this : Subobject.arrow (kernelSubobject g) ≫ cokernel.π f = 0
⊢ kernel.ι g ≫ cokernel.π f = 0
rw [← kernelSubobject_arrow', Category.assoc, this, comp_zero]