∀ {I : Type u_2} (C : I → Type u_3) [inst : (i : I) → CategoryTheory.Category.{u_1, u_3} (C i)] {J : Type u_2}
  {D : J → Type u_3} [inst_1 : (j : J) → CategoryTheory.Category.{u_1, u_3} (D j)] {X X' : (i : I) → C i} (f : X ⟶ X')
  ⦃X_1 Y : (j : J) → D j⦄ (f_1 : X_1 ⟶ Y),
  (CategoryTheory.CategoryStruct.comp
      ({
            obj := fun Y s =>
              match s with
              | Sum.inl i => X i
              | Sum.inr j => Y j,
            map := fun {x x_1} f s =>
              match s with
              | Sum.inl i => CategoryTheory.CategoryStruct.id (X i)
              | Sum.inr j => f j,
            map_id := ⋯, map_comp := ⋯ }.map
        f_1)
      fun s =>
      match s with
      | Sum.inl i => f i
      | Sum.inr j => CategoryTheory.CategoryStruct.id (Y j)) =
    CategoryTheory.CategoryStruct.comp
      (fun s =>
        match s with
        | Sum.inl i => f i
        | Sum.inr j => CategoryTheory.CategoryStruct.id (X_1 j))
      ({
            obj := fun Y s =>
              match s with
              | Sum.inl i => X' i
              | Sum.inr j => Y j,
            map := fun {x x_1} f s =>
              match s with
              | Sum.inl i => CategoryTheory.CategoryStruct.id (X' i)
              | Sum.inr j => f j,
            map_id := ⋯, map_comp := ⋯ }.map
        f_1)