-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A : Functor.{v₁, v₂, u₁, u₂} C ℰ
P_1 : ℰᵒᵖ ⥤ Type (max w v₁ v₂)
inst_2 : Functor.HasPointwiseLeftKanExtension uliftYoneda.{max w v₂, v₁, u₁} A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
inst_3 : L.IsLeftKanExtension α
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
X Y : ℰ
f : L.obj P ⟶ X
g : X ⟶ Y
this :
  ∀ {W W' : ℰ}
    (f :
      Quiver.Hom (V := CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P ⥤ ℰ)
        (CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A)
        (Functor.obj (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)) W))
    (g : W ⟶ W'),
    Eq.{v₂ + 1} (α := L.obj P ⟶ W')
      ((Equiv.symm (IsColimit.homEquiv (Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension L α P)) :
            (a :
                CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A ⟶
                  (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).obj W') →
              L.obj P ⟶ W')
          (f ≫ Functor.map (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)) g) :
        L.obj P ⟶ W')
      ((Equiv.symm (IsColimit.homEquiv (Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension L α P)) :
              (a :
                  CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A ⟶
                    (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).obj W) →
                L.obj P ⟶ W)
            f ≫
          g :
        L.obj P ⟶ W')
a :
  ∀ (j : CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P),
    Eq (α := Functor.obj (CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A) j ⟶ Y)
      (((Functor.LeftExtension.mk L α).coconeAt P).ι.app j ≫
        ((restrictedULiftYonedaHomEquiv.{w, v₁, v₂, u₁, u₂} L α P Y).symm :
            (a : P ⟶ (restrictedULiftYoneda A).obj Y) → L.obj P ⟶ Y)
          ((restrictedULiftYonedaHomEquiv.{w, v₁, v₂, u₁, u₂} L α P Y :
              (a : L.obj P ⟶ Y) → P ⟶ (restrictedULiftYoneda A).obj Y)
            (f ≫ g)))
      (((Functor.LeftExtension.mk L α).coconeAt P).ι.app j ≫
        ((restrictedULiftYonedaHomEquiv.{w, v₁, v₂, u₁, u₂} L α P Y).symm :
            (a : P ⟶ (restrictedULiftYoneda A).obj Y) → L.obj P ⟶ Y)
          ((restrictedULiftYonedaHomEquiv.{w, v₁, v₂, u₁, u₂} L α P X :
                (a : L.obj P ⟶ X) → P ⟶ (restrictedULiftYoneda A).obj X)
              f ≫
            (restrictedULiftYoneda A).map g))
⊢ Eq.{v₂ + 1} (α := L.obj P ⟶ Y)
    (((restrictedULiftYonedaHomEquiv.{w, v₁, v₂, u₁, u₂} L α P Y).symm :
          (a : P ⟶ (restrictedULiftYoneda A).obj Y) → L.obj P ⟶ Y)
        ((restrictedULiftYonedaHomEquiv.{w, v₁, v₂, u₁, u₂} L α P Y :
            (a : L.obj P ⟶ Y) → P ⟶ (restrictedULiftYoneda A).obj Y)
          (f ≫ g)) :
      L.obj P ⟶ Y)
    (((restrictedULiftYonedaHomEquiv.{w, v₁, v₂, u₁, u₂} L α P Y).symm :
          (a : P ⟶ (restrictedULiftYoneda A).obj Y) → L.obj P ⟶ Y)
        ((restrictedULiftYonedaHomEquiv.{w, v₁, v₂, u₁, u₂} L α P X :
              (a : L.obj P ⟶ X) → P ⟶ (restrictedULiftYoneda A).obj X)
            f ≫
          (restrictedULiftYoneda A).map g) :
      L.obj P ⟶ Y)

Tactic:
apply (Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension L α P).hom_ext

Premises used: CategoryTheory.Limits.IsColimit.hom_ext, CategoryTheory.Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension