∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} C] {J : Type u_1}
  [inst_1 : CategoryTheory.Category.{u_4, u_1} J] {X : C} {K : CategoryTheory.Functor J (CategoryTheory.Over X)}
  (t : CategoryTheory.Limits.Cone (CategoryTheory.WithTerminal.liftFromOver.obj K)) (j : CategoryTheory.WithTerminal J),
  ((CategoryTheory.WithTerminal.coneBack✝.comp CategoryTheory.WithTerminal.coneLift✝).obj t).π.app j =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Iso.refl
          ((CategoryTheory.WithTerminal.coneBack✝¹.comp CategoryTheory.WithTerminal.coneLift✝¹).obj t).pt).hom
      (((CategoryTheory.Functor.id (CategoryTheory.Limits.Cone (CategoryTheory.WithTerminal.liftFromOver.obj K))).obj
              t).π.app
        j)