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