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'
⊢ (kernelSubobjectIso f).hom ≫
      kernel.map f f' sq.left sq.right
        (_ : (Arrow.mk f).hom ≫ (𝟭 C).map sq.right = (𝟭 C).map sq.left ≫ (Arrow.mk f').hom) =
    kernelSubobjectMap sq ≫ (kernelSubobjectIso f').hom
simp [← Iso.comp_inv_eq, kernel_map_comp_kernelSubobjectIso_inv]