∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} (X_1 : CategoryTheory.Functor J (CategoryTheory.Over X)) (X_2 : CategoryTheory.WithTerminal J),
  (CategoryTheory.WithTerminal.liftFromOver.obj X_1).obj X_2 =
    match X_2 with
    | CategoryTheory.WithTerminal.of x => (X_1.obj x).left
    | CategoryTheory.WithTerminal.star => X