∀ {C : Type u_2} {inst : CategoryTheory.Category.{u_1, u_2} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {A B : CategoryTheory.Mon C} {M N : Bimod A B} (motive : M.Hom N → Prop) (h : M.Hom N),
  (∀ (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),
      motive { hom := hom, left_act_hom := left_act_hom, right_act_hom := right_act_hom }) →
    motive h