case h
ι : Type ?u.7186
V : Type u
inst✝³ : Category V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹ : HasImage f
g : B ⟶ C
inst✝ : HasKernel g
w : f ≫ g = 0
⊢ (factorThruImageSubobject f ≫ imageToKernel f g w) ≫ Subobject.arrow (kernelSubobject g) =
    factorThruKernelSubobject g f w ≫ Subobject.arrow (kernelSubobject g)
ι : Type ?u.7186
V : Type u
inst✝³ : Category V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹ : HasImage f
g : B ⟶ C
inst✝ : HasKernel g
w : f ≫ g = 0
⊢ factorThruImageSubobject f ≫ imageToKernel f g w = factorThruKernelSubobject g f w
ext
no goals
case h
ι : Type ?u.7186
V : Type u
inst✝³ : Category V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹ : HasImage f
g : B ⟶ C
inst✝ : HasKernel g
w : f ≫ g = 0
⊢ (factorThruImageSubobject f ≫ imageToKernel f g w) ≫ Subobject.arrow (kernelSubobject g) =
    factorThruKernelSubobject g f w ≫ Subobject.arrow (kernelSubobject g)
simp