∀ {C : Type u_4} {D : Type u_6} {H : Type u_2} [inst : CategoryTheory.Category.{u_3, u_4} C]
  [inst_1 : CategoryTheory.Category.{u_5, u_6} D] [inst_2 : CategoryTheory.Category.{u_1, u_2} H]
  (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) [inst_3 : L.HasPointwiseRightKanExtension F]
  (Y : D),
  CategoryTheory.Limits.limit.lift ((CategoryTheory.StructuredArrow.proj Y L).comp F)
      { pt := CategoryTheory.Limits.limit ((CategoryTheory.StructuredArrow.proj Y L).comp F),
        π :=
          {
            app := fun g =>
              CategoryTheory.Limits.limit.π ((CategoryTheory.StructuredArrow.proj Y L).comp F)
                ((CategoryTheory.StructuredArrow.map (CategoryTheory.CategoryStruct.id Y)).obj g),
            naturality := ⋯ } } =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.limit ((CategoryTheory.StructuredArrow.proj Y L).comp F))