no goals
C : Type u
inst✝⁴ : Category C
X Y Z : C
f✝ : X ⟶ Y
inst✝³ : HasImage f✝
inst✝² : HasEqualizers C
X' : C
h : X' ⟶ X
inst✝¹ : IsIso h
f : X ⟶ Y
inst✝ : HasImage f
⊢ inv (image.preComp h f) ≫ image.ι (h ≫ f) = image.ι f
simp