{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {M N : C} →
        [inst_2 : CategoryTheory.MonObj M] →
          [inst_3 : CategoryTheory.MonObj N] →
            (e : M ≅ N) → [CategoryTheory.IsMonHom e.hom] → { X := M, mon := inst_2 } ≅ { X := N, mon := inst_3 }