∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] (F G : CategoryTheory.Functor C (Type u_2))
  (x : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair F G))
  (x_1 : CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.FunctorToTypes.prod.lift (CategoryTheory.Limits.BinaryFan.fst x)
        (CategoryTheory.Limits.BinaryFan.snd x))
      ((CategoryTheory.FunctorToTypes.binaryProductCone F G).π.app x_1) =
    x.π.app x_1