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