∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {D : Type u_5}
  [inst_1 : CategoryTheory.Category.{u_3, u_5} D] {F : CategoryTheory.Functor C D}
  [inst_2 : ∀ (P : CategoryTheory.Functor Cᵒᵖ (Type (max u_4 u_1 u_3))), F.op.HasLeftKanExtension P]
  (P : CategoryTheory.Functor Cᵒᵖ (Type (max u_4 u_1 u_3))), (F.op.lan.obj P).IsLeftKanExtension (F.op.lanUnit.app P)