case h
ι : Type ?u.276606
V : Type u
inst✝³ : Category V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w✝ : f ≫ g = 0
inst✝¹ : HasKernels V
inst✝ : HasImages V
w : f ≫ g = 0
⊢ ((imageSubobjectIso f).hom ≫ imageToKernel' f g w) ≫ equalizer.ι g 0 =
    (imageToKernel f g w ≫ (kernelSubobjectIso g).hom) ≫ equalizer.ι g 0
ι : Type ?u.276606
V : Type u
inst✝³ : Category V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w✝ : f ≫ g = 0
inst✝¹ : HasKernels V
inst✝ : HasImages V
w : f ≫ g = 0
⊢ (imageSubobjectIso f).hom ≫ imageToKernel' f g w = imageToKernel f g w ≫ (kernelSubobjectIso g).hom
apply equalizer.hom_ext
no goals
case h
ι : Type ?u.276606
V : Type u
inst✝³ : Category V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w✝ : f ≫ g = 0
inst✝¹ : HasKernels V
inst✝ : HasImages V
w : f ≫ g = 0
⊢ ((imageSubobjectIso f).hom ≫ imageToKernel' f g w) ≫ equalizer.ι g 0 =
    (imageToKernel f g w ≫ (kernelSubobjectIso g).hom) ≫ equalizer.ι g 0
simp [imageToKernel']