∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
  {F : CategoryTheory.Limits.MonoFactorisation f} [inst_1 : SizeOf C]
  (lift : (F' : CategoryTheory.Limits.MonoFactorisation f) → F.I ⟶ F'.I)
  (lift_fac :
    autoParam
      (∀ (F' : CategoryTheory.Limits.MonoFactorisation f), CategoryTheory.CategoryStruct.comp (lift F') F'.m = F.m)
      CategoryTheory.Limits.IsImage.lift_fac._autoParam),
  sizeOf { lift := lift, lift_fac := lift_fac } = 1