no goals
C : Type u
inst✝³ : Category C
X Y Z : C
inst✝² : HasZeroMorphisms C
f : X ⟶ Y
inst✝¹ : HasKernel f
X' Y' : C
f' : X' ⟶ Y'
inst✝ : HasKernel f'
sq : Arrow.mk f ⟶ Arrow.mk f'
⊢ kernelSubobjectMap sq ≫ arrow (kernelSubobject f') = arrow (kernelSubobject f) ≫ sq.left
simp [kernelSubobjectMap]