∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {J : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J] (D : CategoryTheory.Functor J T) {X : T}
  (s : D ⟶ (CategoryTheory.Functor.const J).obj X) (j : J),
  (CategoryTheory.Over.lift D s).obj j = CategoryTheory.Over.mk (s.app j)