{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} →
      {f g : CategoryTheory.MonoOver X} →
        (h : f.obj.left ≅ g.obj.left) →
          autoParam (CategoryTheory.CategoryStruct.comp h.hom g.arrow = f.arrow) CategoryTheory.MonoOver.isoMk._auto_1 →
            (f ≅ g)