∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {A B : CategoryTheory.Mon C} {M N : Bimod A B} {hom : M.X ⟶ N.X}
  {left_act_hom :
    autoParam
      (CategoryTheory.CategoryStruct.comp M.actLeft hom =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A.X hom) N.actLeft)
      Bimod.Hom.left_act_hom._autoParam}
  {right_act_hom :
    autoParam
      (CategoryTheory.CategoryStruct.comp M.actRight hom =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight hom B.X) N.actRight)
      Bimod.Hom.right_act_hom._autoParam}
  {hom_1 : M.X ⟶ N.X}
  {left_act_hom_1 :
    autoParam
      (CategoryTheory.CategoryStruct.comp M.actLeft hom_1 =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A.X hom_1) N.actLeft)
      Bimod.Hom.left_act_hom._autoParam}
  {right_act_hom_1 :
    autoParam
      (CategoryTheory.CategoryStruct.comp M.actRight hom_1 =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight hom_1 B.X) N.actRight)
      Bimod.Hom.right_act_hom._autoParam},
  { hom := hom, left_act_hom := left_act_hom, right_act_hom := right_act_hom } =
      { hom := hom_1, left_act_hom := left_act_hom_1, right_act_hom := right_act_hom_1 } →
    hom = hom_1