{C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {inst_1 : CategoryTheory.MonoidalCategory C} →
      {A B : CategoryTheory.Mon C} →
        {P : Sort u} →
          {X : C} →
            {actLeft : CategoryTheory.MonoidalCategoryStruct.tensorObj A.X X ⟶ X} →
              {one_actLeft :
                  autoParam
                    (CategoryTheory.CategoryStruct.comp
                        (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one X) actLeft =
                      (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom)
                    Bimod.one_actLeft._autoParam} →
                {left_assoc :
                    autoParam
                      (CategoryTheory.CategoryStruct.comp
                          (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul X) actLeft =
                        CategoryTheory.CategoryStruct.comp
                          (CategoryTheory.MonoidalCategoryStruct.associator A.X A.X X).hom
                          (CategoryTheory.CategoryStruct.comp
                            (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A.X actLeft) actLeft))
                      Bimod.left_assoc._autoParam} →
                  {actRight : CategoryTheory.MonoidalCategoryStruct.tensorObj X B.X ⟶ X} →
                    {actRight_one :
                        autoParam
                          (CategoryTheory.CategoryStruct.comp
                              (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.MonObj.one) actRight =
                            (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom)
                          Bimod.actRight_one._autoParam} →
                      {right_assoc :
                          autoParam
                            (CategoryTheory.CategoryStruct.comp
                                (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.MonObj.mul)
                                actRight =
                              CategoryTheory.CategoryStruct.comp
                                (CategoryTheory.MonoidalCategoryStruct.associator X B.X B.X).inv
                                (CategoryTheory.CategoryStruct.comp
                                  (CategoryTheory.MonoidalCategoryStruct.whiskerRight actRight B.X) actRight))
                            Bimod.right_assoc._autoParam} →
                        {middle_assoc :
                            autoParam
                              (CategoryTheory.CategoryStruct.comp
                                  (CategoryTheory.MonoidalCategoryStruct.whiskerRight actLeft B.X) actRight =
                                CategoryTheory.CategoryStruct.comp
                                  (CategoryTheory.MonoidalCategoryStruct.associator A.X X B.X).hom
                                  (CategoryTheory.CategoryStruct.comp
                                    (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A.X actRight) actLeft))
                              Bimod.middle_assoc._autoParam} →
                          {X' : C} →
                            {actLeft' : CategoryTheory.MonoidalCategoryStruct.tensorObj A.X X' ⟶ X'} →
                              {one_actLeft' :
                                  autoParam
                                    (CategoryTheory.CategoryStruct.comp
                                        (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one
                                          X')
                                        actLeft' =
                                      (CategoryTheory.MonoidalCategoryStruct.leftUnitor X').hom)
                                    Bimod.one_actLeft._autoParam} →
                                {left_assoc' :
                                    autoParam
                                      (CategoryTheory.CategoryStruct.comp
                                          (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul
                                            X')
                                          actLeft' =
                                        CategoryTheory.CategoryStruct.comp
                                          (CategoryTheory.MonoidalCategoryStruct.associator A.X A.X X').hom
                                          (CategoryTheory.CategoryStruct.comp
                                            (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A.X actLeft') actLeft'))
                                      Bimod.left_assoc._autoParam} →
                                  {actRight' : CategoryTheory.MonoidalCategoryStruct.tensorObj X' B.X ⟶ X'} →
                                    {actRight_one' :
                                        autoParam
                                          (CategoryTheory.CategoryStruct.comp
                                              (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X'
                                                CategoryTheory.MonObj.one)
                                              actRight' =
                                            (CategoryTheory.MonoidalCategoryStruct.rightUnitor X').hom)
                                          Bimod.actRight_one._autoParam} →
                                      {right_assoc' :
                                          autoParam
                                            (CategoryTheory.CategoryStruct.comp
                                                (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X'
                                                  CategoryTheory.MonObj.mul)
                                                actRight' =
                                              CategoryTheory.CategoryStruct.comp
                                                (CategoryTheory.MonoidalCategoryStruct.associator X' B.X B.X).inv
                                                (CategoryTheory.CategoryStruct.comp
                                                  (CategoryTheory.MonoidalCategoryStruct.whiskerRight actRight' B.X)
                                                  actRight'))
                                            Bimod.right_assoc._autoParam} →
                                        {middle_assoc' :
                                            autoParam
                                              (CategoryTheory.CategoryStruct.comp
                                                  (CategoryTheory.MonoidalCategoryStruct.whiskerRight actLeft' B.X)
                                                  actRight' =
                                                CategoryTheory.CategoryStruct.comp
                                                  (CategoryTheory.MonoidalCategoryStruct.associator A.X X' B.X).hom
                                                  (CategoryTheory.CategoryStruct.comp
                                                    (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A.X actRight')
                                                    actLeft'))
                                              Bimod.middle_assoc._autoParam} →
                                          { X := X, actLeft := actLeft, one_actLeft := one_actLeft,
                                                left_assoc := left_assoc, actRight := actRight,
                                                actRight_one := actRight_one, right_assoc := right_assoc,
                                                middle_assoc := middle_assoc } =
                                              { X := X', actLeft := actLeft', one_actLeft := one_actLeft',
                                                left_assoc := left_assoc', actRight := actRight',
                                                actRight_one := actRight_one', right_assoc := right_assoc',
                                                middle_assoc := middle_assoc' } →
                                            (X ≍ X' → actLeft ≍ actLeft' → actRight ≍ actRight' → P) → P