∀ {X Y : Type u_1} (x : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Types.binaryProductFunctor.map x)
      (CategoryTheory.NatIso.ofComponents
          (fun Y_1 =>
            ((CategoryTheory.Limits.limit.isLimit (CategoryTheory.Limits.pair Y Y_1)).conePointUniqueUpToIso
                (CategoryTheory.Limits.Types.binaryProductLimit Y Y_1)).symm)
          ⋯).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.NatIso.ofComponents
          (fun Y =>
            ((CategoryTheory.Limits.limit.isLimit (CategoryTheory.Limits.pair X Y)).conePointUniqueUpToIso
                (CategoryTheory.Limits.Types.binaryProductLimit X Y)).symm)
          ⋯).hom
      (CategoryTheory.Limits.prod.functor.map x)