∀ {R : Type u_1} [inst : CommRing R] (A : ModuleCat R) [inst_1 : CategoryTheory.MonObj A]
  (x y : ↑(CategoryTheory.MonoidalCategoryStruct.tensorUnit (ModuleCat R))),
  (ModuleCat.Hom.hom CategoryTheory.MonObj.one).toFun (x + y) =
    (ModuleCat.Hom.hom CategoryTheory.MonObj.one).toFun x + (ModuleCat.Hom.hom CategoryTheory.MonObj.one).toFun y