∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C]
  (𝒯 : CategoryTheory.Limits.LimitCone (CategoryTheory.Functor.empty C))
  (ℬ : (X Y : C) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y)) (X Y : C) {T : C} (f : T ⟶ X)
  (g : T ⟶ Y)
  (m :
    T ⟶
      (CategoryTheory.Limits.BinaryFan.mk (CategoryTheory.Limits.BinaryFan.fst (ℬ X Y).cone)
          (CategoryTheory.Limits.BinaryFan.snd (ℬ X Y).cone)).pt),
  CategoryTheory.CategoryStruct.comp m
        (CategoryTheory.Limits.BinaryFan.mk (CategoryTheory.Limits.BinaryFan.fst (ℬ X Y).cone)
            (CategoryTheory.Limits.BinaryFan.snd (ℬ X Y).cone)).fst =
      f →
    CategoryTheory.CategoryStruct.comp m (CategoryTheory.Limits.BinaryFan.fst (ℬ X Y).cone) =
      CategoryTheory.CategoryStruct.comp
        ((fun {T} f g => ↑(CategoryTheory.Limits.BinaryFan.IsLimit.lift' (ℬ X Y).isLimit f g)) f g)
        (CategoryTheory.Limits.BinaryFan.fst (ℬ X Y).cone)