∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] (X Y : C)
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct X Y] (x : CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair),
  (CategoryTheory.Limits.limit.cone (CategoryTheory.Limits.pair X Y)).π.app x =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Iso.refl (CategoryTheory.Limits.limit.cone (CategoryTheory.Limits.pair X Y)).pt).hom
      ((CategoryTheory.Limits.BinaryFan.mk CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd).π.app x)