case h
ι : Type ?u.9377
V : Type u
inst✝² : Category V
inst✝¹ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝ : HasImages V
w : f ≫ 0 = 0
⊢ imageToKernel f 0 w ≫ Subobject.arrow (kernelSubobject 0) =
    (Subobject.arrow (imageSubobject f) ≫ inv (Subobject.arrow (kernelSubobject 0))) ≫
      Subobject.arrow (kernelSubobject 0)
ι : Type ?u.9377
V : Type u
inst✝² : Category V
inst✝¹ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝ : HasImages V
w : f ≫ 0 = 0
⊢ imageToKernel f 0 w = Subobject.arrow (imageSubobject f) ≫ inv (Subobject.arrow (kernelSubobject 0))
ext
no goals
case h
ι : Type ?u.9377
V : Type u
inst✝² : Category V
inst✝¹ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝ : HasImages V
w : f ≫ 0 = 0
⊢ imageToKernel f 0 w ≫ Subobject.arrow (kernelSubobject 0) =
    (Subobject.arrow (imageSubobject f) ≫ inv (Subobject.arrow (kernelSubobject 0))) ≫
      Subobject.arrow (kernelSubobject 0)
simp