∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {X : C} [inst_1 : CategoryTheory.Limits.HasImages C]
  {X' X_1 : CategoryTheory.Over X} {Y : CategoryTheory.MonoOver X} (f : X' ⟶ X_1)
  (g : X_1 ⟶ (CategoryTheory.MonoOver.forget X).obj Y),
  {
          toFun := fun k =>
            CategoryTheory.Over.homMk
              (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage X'.hom) k.hom.left) ⋯,
          invFun := fun k =>
            CategoryTheory.MonoOver.homMk
              (CategoryTheory.Limits.image.lift { I := Y.obj.left, m := Y.arrow, m_mono := ⋯, e := k.left, fac := ⋯ })
              ⋯,
          left_inv := ⋯, right_inv := ⋯ }.symm
      (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoOver.image.map f)
      ({
            toFun := fun k =>
              CategoryTheory.Over.homMk
                (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage X_1.hom) k.hom.left) ⋯,
            invFun := fun k =>
              CategoryTheory.MonoOver.homMk
                (CategoryTheory.Limits.image.lift { I := Y.obj.left, m := Y.arrow, m_mono := ⋯, e := k.left, fac := ⋯ })
                ⋯,
            left_inv := ⋯, right_inv := ⋯ }.symm
        g)