no goals
C : Type u_2
inst✝¹ : Category C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ (imageUnopOp g).hom ≫ image.ι g = (factorThruImage g.unop).op
simp only [← cancel_epi (image.ι g.unop).op, ← Category.assoc, image_ι_op_comp_imageUnopOp_hom,
  ← op_comp, image.fac, Quiver.Hom.op_unop]