-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {A B : CategoryTheory.Mon C} {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_1 : C} {actLeft_1 : CategoryTheory.MonoidalCategoryStruct.tensorObj A.X X_1 ⟶ X_1}
  {one_actLeft_1 :
    autoParam
      (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one X_1) actLeft_1 =
        (CategoryTheory.MonoidalCategoryStruct.leftUnitor X_1).hom)
      Bimod.one_actLeft._autoParam}
  {left_assoc_1 :
    autoParam
      (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul X_1) actLeft_1 =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A.X A.X X_1).hom
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A.X actLeft_1)
            actLeft_1))
      Bimod.left_assoc._autoParam}
  {actRight_1 : CategoryTheory.MonoidalCategoryStruct.tensorObj X_1 B.X ⟶ X_1}
  {actRight_one_1 :
    autoParam
      (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X_1 CategoryTheory.MonObj.one) actRight_1 =
        (CategoryTheory.MonoidalCategoryStruct.rightUnitor X_1).hom)
      Bimod.actRight_one._autoParam}
  {right_assoc_1 :
    autoParam
      (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X_1 CategoryTheory.MonObj.mul) actRight_1 =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X_1 B.X B.X).inv
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight actRight_1 B.X)
            actRight_1))
      Bimod.right_assoc._autoParam}
  {middle_assoc_1 :
    autoParam
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight actLeft_1 B.X)
          actRight_1 =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A.X X_1 B.X).hom
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A.X actRight_1)
            actLeft_1))
      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_1, actLeft := actLeft_1, one_actLeft := one_actLeft_1, left_assoc := left_assoc_1,
        actRight := actRight_1, actRight_one := actRight_one_1, right_assoc := right_assoc_1,
        middle_assoc := middle_assoc_1 } →
    X = X_1 ∧ actLeft ≍ actLeft_1 ∧ actRight ≍ actRight_1