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
h : Exact 0 g
this : Epi (imageToKernel 0 g (_ : 0 ≫ g = 0))
⊢ Subobject.arrow (kernelSubobject g) = 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
h : Exact 0 g
⊢ Subobject.arrow (kernelSubobject g) = 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
h : Exact 0 g
this : Epi (imageToKernel 0 g (_ : 0 ≫ g = 0))
⊢ factorThruImageSubobject 0 ≫ imageToKernel 0 g (_ : 0 ≫ g = 0) ≫ Subobject.arrow (kernelSubobject g) =
    factorThruImageSubobject 0 ≫ imageToKernel 0 g (_ : 0 ≫ g = 0) ≫ 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
h : Exact 0 g
this : Epi (imageToKernel 0 g (_ : 0 ≫ g = 0))
⊢ Subobject.arrow (kernelSubobject g) = 0
rw [← cancel_epi (imageToKernel (0 : A ⟶ B) g h.w), ←
  cancel_epi (factorThruImageSubobject (0 : A ⟶ B))]
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
h : Exact 0 g
this : Epi (imageToKernel 0 g (_ : 0 ≫ g = 0))
⊢ factorThruImageSubobject 0 ≫ imageToKernel 0 g (_ : 0 ≫ g = 0) ≫ Subobject.arrow (kernelSubobject g) =
    factorThruImageSubobject 0 ≫ imageToKernel 0 g (_ : 0 ≫ g = 0) ≫ 0
simp