∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M' N' : C}
  [inst_2 : CategoryTheory.AddMonObj M'] [inst_3 : CategoryTheory.AddMonObj N'] {f : M' ⟶ N'},
  autoParam (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.zero f = CategoryTheory.AddMonObj.zero)
      CategoryTheory.IsAddMonHom.zero_hom._autoParam →
    autoParam
        (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add f =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f f)
            CategoryTheory.AddMonObj.add)
        CategoryTheory.IsAddMonHom.add_hom._autoParam →
      CategoryTheory.IsAddMonHom f