∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {X : C} {J : Type u_3}
  [inst_1 : CategoryTheory.SmallCategory J] {Y : CategoryTheory.Functor J C} {j₀ : J} (y : X ⟶ Y.obj j₀)
  (t₁ t₂ : CategoryTheory.Under j₀) (f : t₁ ⟶ t₂),
  CategoryTheory.CategoryStruct.comp (((CategoryTheory.Functor.const (CategoryTheory.Under j₀)).obj X).map f)
      (CategoryTheory.CategoryStruct.comp y (Y.map t₂.hom)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp y (Y.map t₁.hom))
      (((CategoryTheory.Under.forget j₀).comp Y).map f)