∀ (G H : AddCommGrpCat) {T : AddCommGrpCat} (x : T ⟶ G) (x_1 : T ⟶ H),
  CategoryTheory.CategoryStruct.comp (AddCommGrpCat.ofHom ((AddCommGrpCat.Hom.hom x).prod (AddCommGrpCat.Hom.hom x_1)))
      (CategoryTheory.Limits.BinaryFan.mk (AddCommGrpCat.ofHom (AddMonoidHom.fst ↑G ↑H))
          (AddCommGrpCat.ofHom (AddMonoidHom.snd ↑G ↑H))).fst =
    CategoryTheory.CategoryStruct.comp
      (AddCommGrpCat.ofHom ((AddCommGrpCat.Hom.hom x).prod (AddCommGrpCat.Hom.hom x_1)))
      (CategoryTheory.Limits.BinaryFan.mk (AddCommGrpCat.ofHom (AddMonoidHom.fst ↑G ↑H))
          (AddCommGrpCat.ofHom (AddMonoidHom.snd ↑G ↑H))).fst