∀ {T : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} T] {X : T} (f : CategoryTheory.Over X)
  {X_1 Y : CategoryTheory.Over f.left} (α : X_1 ⟶ Y),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.homMk α.left ⋯)
      (CategoryTheory.Over.mk (CategoryTheory.Over.homMk Y.hom ⋯)).hom =
    (CategoryTheory.Over.mk (CategoryTheory.Over.homMk X_1.hom ⋯)).hom