∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {X : C} (Y Z : CategoryTheory.Over X)
  [inst_1 : CategoryTheory.ChosenPullbacksAlong Z.hom] {T : CategoryTheory.Over X} (f : T ⟶ Y) (g : T ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      ((fun {T} u v => CategoryTheory.Over.homMk (CategoryTheory.ChosenPullbacksAlong.lift u.left v.left ⋯) ⋯) f g)
      (CategoryTheory.ChosenPullbacksAlong.binaryFan Y Z).fst =
    f