∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M N : C}
  [inst_2 : CategoryTheory.MonObj M] [inst_3 : CategoryTheory.MonObj 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 →
      CategoryTheory.IsMonHom f