{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        {M : C} →
          [toMonObj : CategoryTheory.MonObj M] →
            [toComonObj : CategoryTheory.ComonObj M] →
              autoParam
                  (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul CategoryTheory.ComonObj.comul =
                    CategoryTheory.CategoryStruct.comp
                      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.ComonObj.comul
                        CategoryTheory.ComonObj.comul)
                      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M M M M)
                        (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.mul
                          CategoryTheory.MonObj.mul)))
                  CategoryTheory.BimonObj.mul_comul._autoParam →
                autoParam
                    (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one CategoryTheory.ComonObj.comul =
                      CategoryTheory.MonObj.one)
                    CategoryTheory.BimonObj.one_comul._autoParam →
                  autoParam
                      (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul CategoryTheory.ComonObj.counit =
                        CategoryTheory.ComonObj.counit)
                      CategoryTheory.BimonObj.mul_counit._autoParam →
                    autoParam
                        (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one CategoryTheory.ComonObj.counit =
                          CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
                        CategoryTheory.BimonObj.one_counit._autoParam →
                      CategoryTheory.BimonObj M