{A : Type u_1} →
  {B : Type u_2} →
    {C : Type u_3} →
      {D : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} A] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} B] →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} D] →
                {G : CategoryTheory.Functor B D} →
                  {F : CategoryTheory.Functor A B} →
                    {L : CategoryTheory.Functor A C} →
                      {c : C} →
                        {motive : G.PreservesPointwiseLeftKanExtensionAt F L c → Sort u} →
                          ((preserves :
                                ∀ (E : L.LeftExtension F) (a : E.IsPointwiseLeftKanExtensionAt c),
                                  Nonempty
                                    (((CategoryTheory.Functor.LeftExtension.postcompose₂ L F G).obj
                                          E).IsPointwiseLeftKanExtensionAt
                                      c)) →
                              motive ⋯) →
                            (t : G.PreservesPointwiseLeftKanExtensionAt F L c) → motive t