{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      {f : X ⟶ Y} →
        (F : CategoryTheory.Limits.MonoFactorisation f) →
          (m : F.I ⟶ Y) →
            (e : X ⟶ F.I) →
              autoParam (m = F.m) CategoryTheory.Limits.MonoFactorisation.copy._auto_1 →
                autoParam (e = F.e) CategoryTheory.Limits.MonoFactorisation.copy._auto_3 →
                  CategoryTheory.Limits.MonoFactorisation f