∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {M N : C} [inst_3 : CategoryTheory.BimonObj M]
  [inst_4 : CategoryTheory.BimonObj N] {f : M ⟶ N},
  autoParam (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one f = CategoryTheory.MonObj.one)
      CategoryTheory.IsMonHom.one_hom._autoParam →
    autoParam
        (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul f =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f f)
            CategoryTheory.MonObj.mul)
        CategoryTheory.IsMonHom.mul_hom._autoParam →
      autoParam (CategoryTheory.CategoryStruct.comp f CategoryTheory.ComonObj.counit = CategoryTheory.ComonObj.counit)
          CategoryTheory.IsComonHom.hom_counit._autoParam →
        autoParam
            (CategoryTheory.CategoryStruct.comp f CategoryTheory.ComonObj.comul =
              CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul
                (CategoryTheory.MonoidalCategoryStruct.tensorHom f f))
            CategoryTheory.IsComonHom.hom_comul._autoParam →
          CategoryTheory.IsBimonHom f