∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} C] [inst_1 : CategoryTheory.Limits.HasProducts C] {X Y : C}
  (f : X ⟶ Y) ⦃X_1 Y_1 : Type u_1ᵒᵖ⦄ (f_1 : X_1 ⟶ Y_1),
  CategoryTheory.CategoryStruct.comp
      ({ obj := fun n => ∏ᶜ fun x => X,
            map := fun {X_2 Y} f => CategoryTheory.Limits.Pi.map' f.unop fun x => CategoryTheory.CategoryStruct.id X,
            map_id := ⋯, map_comp := ⋯ }.map
        f_1)
      (CategoryTheory.Limits.Pi.map fun x => f) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.map fun x => f)
      ({ obj := fun n => ∏ᶜ fun x => Y,
            map := fun {X Y_2} f => CategoryTheory.Limits.Pi.map' f.unop fun x => CategoryTheory.CategoryStruct.id Y,
            map_id := ⋯, map_comp := ⋯ }.map
        f_1)