∀ {J : Type u_4} {C : Type u_2} [inst : CategoryTheory.Category.{u_3, u_4} J]
  [inst_1 : CategoryTheory.Category.{u_1, u_2} C] {D : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone D)
  (j : J) (k : CategoryTheory.Under j),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Under.post D).obj k).hom (c.ι.app k.right) =
    (((CategoryTheory.Functor.const (CategoryTheory.Under j)).obj (CategoryTheory.Under.mk (c.ι.app j))).obj k).hom