{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          (X Y : C) →
            [inst_2 : CategoryTheory.Limits.HasBinaryProduct X Y] →
              [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair X Y) G] →
                CategoryTheory.Limits.IsLimit
                  (CategoryTheory.Limits.BinaryFan.mk (G.map CategoryTheory.Limits.prod.fst)
                    (G.map CategoryTheory.Limits.prod.snd))