∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S T U V W : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryCoproduct U W] [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct T V]
  (f : U ⟶ S) (g : W ⟶ S) (h : T ⟶ U) (k : V ⟶ W) {Z : C} (h_1 : S ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map h k)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.desc f g) h_1) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.coprod.desc (CategoryTheory.CategoryStruct.comp h f)
        (CategoryTheory.CategoryStruct.comp k g))
      h_1