no goals
C : Type u
inst✝³ : Category C
X✝ Y Z : C
f✝ : X✝ ⟶ Y
inst✝² : HasImage f✝
A B X : C
g : X ⟶ B
inst✝¹ : Mono g
f : A ⟶ B
inst✝ : HasImage f
h : A ⟶ X
w : h ≫ g = f
⊢ (h ≫ (underlyingIso g).inv) ≫ arrow (Subobject.mk g) = f
simp [w]