∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {X Y W : C} {fst : W ⟶ X} {snd : W ⟶ Y}
  (lift : (s : CategoryTheory.Limits.BinaryFan X Y) → s.pt ⟶ W),
  (∀ (s : CategoryTheory.Limits.BinaryFan X Y), CategoryTheory.CategoryStruct.comp (lift s) fst = s.fst) →
    (∀ (s : CategoryTheory.Limits.BinaryFan X Y), CategoryTheory.CategoryStruct.comp (lift s) snd = s.snd) →
      ∀ (s : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair X Y))
        (j : CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair),
        CategoryTheory.CategoryStruct.comp (lift s) ((CategoryTheory.Limits.BinaryFan.mk fst snd).π.app j) = s.π.app j