∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C]
  {X Y : C} (f : X ⟶ Y) ⦃X_1 Y_1 : C⦄ (f_1 : X_1 ⟶ Y_1),
  CategoryTheory.CategoryStruct.comp
      ({ obj := fun Y => X ⨿ Y,
            map := fun {x x_1} => CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id X), map_id := ⋯,
            map_comp := ⋯ }.map
        f_1)
      (CategoryTheory.Limits.coprod.map f (CategoryTheory.CategoryStruct.id Y_1)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map f (CategoryTheory.CategoryStruct.id X_1))
      ({ obj := fun Y_2 => Y ⨿ Y_2,
            map := fun {x x_1} => CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id Y), map_id := ⋯,
            map_comp := ⋯ }.map
        f_1)