∀ {C : Type u_6} [inst : CategoryTheory.Category.{u_5, u_6} C] {D : Type u_4}
  [inst_1 : CategoryTheory.Category.{u_3, u_4} D] {J : Type u_1} [inst_2 : CategoryTheory.Category.{u_2, u_1} J] {X : C}
  {K : CategoryTheory.Functor J (CategoryTheory.Under X)} {F : CategoryTheory.Functor C D}
  ⦃X_1 Y : CategoryTheory.WithInitial J⦄ (f : X_1 ⟶ Y),
  CategoryTheory.CategoryStruct.comp (((CategoryTheory.WithInitial.liftFromUnder.obj K).comp F).map f)
      (match Y with
      | CategoryTheory.WithInitial.star =>
        CategoryTheory.CategoryStruct.id
          (((CategoryTheory.WithInitial.liftFromUnder.obj K).comp F).obj CategoryTheory.WithInitial.star)
      | CategoryTheory.WithInitial.of a =>
        CategoryTheory.CategoryStruct.id
          (((CategoryTheory.WithInitial.liftFromUnder.obj K).comp F).obj (CategoryTheory.WithInitial.of a))) =
    CategoryTheory.CategoryStruct.comp
      (match X_1 with
      | CategoryTheory.WithInitial.star =>
        CategoryTheory.CategoryStruct.id
          (((CategoryTheory.WithInitial.liftFromUnder.obj K).comp F).obj CategoryTheory.WithInitial.star)
      | CategoryTheory.WithInitial.of a =>
        CategoryTheory.CategoryStruct.id
          (((CategoryTheory.WithInitial.liftFromUnder.obj K).comp F).obj (CategoryTheory.WithInitial.of a)))
      ((CategoryTheory.WithInitial.liftFromUnder.obj (K.comp (CategoryTheory.Under.post F))).map f)