case h
C : Type u
inst✝¹ : Category C
X Y Z : C
f : X ⟶ Y
inst✝ : HasImage f
W : C
k : W ⟶ X
h : Factors (imageSubobject f) (k ≫ f)
⊢ factorThru (imageSubobject f) (k ≫ f) h ≫ arrow (imageSubobject f) =
    (k ≫ factorThruImageSubobject f) ≫ arrow (imageSubobject f)
C : Type u
inst✝¹ : Category C
X Y Z : C
f : X ⟶ Y
inst✝ : HasImage f
W : C
k : W ⟶ X
h : Factors (imageSubobject f) (k ≫ f)
⊢ factorThru (imageSubobject f) (k ≫ f) h = k ≫ factorThruImageSubobject f
ext
no goals
case h
C : Type u
inst✝¹ : Category C
X Y Z : C
f : X ⟶ Y
inst✝ : HasImage f
W : C
k : W ⟶ X
h : Factors (imageSubobject f) (k ≫ f)
⊢ factorThru (imageSubobject f) (k ≫ f) h ≫ arrow (imageSubobject f) =
    (k ≫ factorThruImageSubobject f) ≫ arrow (imageSubobject f)
simp