∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C]
  {X X' Y Y' : C} (g : X ⟶ Y) (g' : X' ⟶ Y'),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.coprod.inl)
        (CategoryTheory.CategoryStruct.comp g' CategoryTheory.Limits.coprod.inr))
      (CategoryTheory.Limits.codiag (Y ⨿ Y')) =
    CategoryTheory.Limits.coprod.map g g'