no goals
C : Type u
inst✝² : Category C
X✝ Y Z : C
f✝ : X✝ ⟶ Y
inst✝¹ : HasImage f✝
A B : C
X : Subobject B
f : A ⟶ B
inst✝ : HasImage f
h : A ⟶ underlying.obj X
w : h ≫ arrow X = f
⊢ ((imageSubobjectIso f).hom ≫ image.lift (MonoFactorisation.mk (underlying.obj X) (arrow X) h)) ≫ arrow X =
    arrow (imageSubobject f)
rw [assoc, image.lift_fac, imageSubobject_arrow]