-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.mk.injEq : ∀ {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)