∀ {T : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} T] (X : T) ⦃X_1 Y : CategoryTheory.Under X⦄ (f : X_1 ⟶ Y),
  CategoryTheory.CategoryStruct.comp (((CategoryTheory.Functor.const (CategoryTheory.Under X)).obj X).map f) Y.hom =
    CategoryTheory.CategoryStruct.comp X_1.hom ((CategoryTheory.Under.forget X).map f)