∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] (D : Type u_4)
  [inst_1 : CategoryTheory.Category.{u_3, u_4} D]
  [inst_2 : ∀ (a b : C), CategoryTheory.Limits.HasProductsOfShape (a ⟶ b) D] (c : C) {X Y : D} (f : X ⟶ Y) ⦃X_1 Y_1 : C⦄
  (f_1 : X_1 ⟶ Y_1),
  CategoryTheory.CategoryStruct.comp
      ({ obj := fun t => ∏ᶜ fun x => X,
            map := fun {X_2 Y} f =>
              CategoryTheory.Limits.Pi.lift fun g =>
                CategoryTheory.Limits.Pi.π (fun x => X) (CategoryTheory.CategoryStruct.comp f g),
            map_id := ⋯, map_comp := ⋯ }.map
        f_1)
      (CategoryTheory.Limits.Pi.lift fun g =>
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun x => X) g) f) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.Pi.lift fun g =>
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun x => X) g) f)
      ({ obj := fun t => ∏ᶜ fun x => Y,
            map := fun {X Y_2} f =>
              CategoryTheory.Limits.Pi.lift fun g =>
                CategoryTheory.Limits.Pi.π (fun x => Y) (CategoryTheory.CategoryStruct.comp f g),
            map_id := ⋯, map_comp := ⋯ }.map
        f_1)