no goals
C : Type u
inst✝⁴ : Category C
X Y Z : C
inst✝³ : HasZeroMorphisms C
f✝ : X ⟶ Y
inst✝² : HasKernel f✝
X' : C
f : X' ⟶ X
inst✝¹ : IsIso f
g : X ⟶ Y
inst✝ : HasKernel g
⊢ (kernelSubobjectIsoComp f g).inv ≫ arrow (kernelSubobject (f ≫ g)) = arrow (kernelSubobject g) ≫ inv f
simp [kernelSubobjectIsoComp]