{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      {f : X ⟶ Y} →
        (I : C) →
          (m : I ⟶ Y) →
            [m_mono : CategoryTheory.Mono m] →
              (e : X ⟶ I) →
                autoParam (CategoryTheory.CategoryStruct.comp e m = f)
                    CategoryTheory.Limits.MonoFactorisation.fac._autoParam →
                  CategoryTheory.Limits.MonoFactorisation f