no goals
Δ Δ'' : SimplexCategory
φ : Δ ⟶ Δ''
e : Δ ⟶ image φ
inst✝¹ : Epi e
i : image φ ⟶ Δ''
inst✝ : Mono i
fac : e ≫ i = φ
⊢ factorThruImage φ = e
rw [← cancel_mono i, fac, ← image_ι_eq fac, image.fac]