no goals
C : Type u
inst✝² : Category C
X Y Z : C
f✝ : X ⟶ Y
inst✝¹ : HasImage f✝
f : X ⟶ Y
inst✝ : Mono f
⊢ (imageSubobjectIso f ≪≫ imageMonoIsoSource f ≪≫ (underlyingIso f).symm).hom ≫ arrow (Subobject.mk f) =
    arrow (imageSubobject f)
simp