∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} {X_1 Y : CategoryTheory.Functor J (CategoryTheory.Under X)} (f : X_1 ⟶ Y),
  (CategoryTheory.WithInitial.commaFromUnder.map f).right =
    CategoryTheory.Functor.whiskerRight f (CategoryTheory.Under.forget X)