-- 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 Q : Cᵒᵖ ⥤ Type (max w v₁ v₂)
X : ℰ
f : P ⟶ Q
g : Q ⟶ (restrictedULiftYoneda A).obj X
p : CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P
hfg :
  Eq (α := A.obj p.left ⟶ X)
    (α.app p.left ≫
      L.map p.hom ≫
        (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 X) →
              L.obj P ⟶ X)
          (((restrictedULiftYonedaHomEquiv'.{w, v₁, v₂, u₁, u₂} A P X).symm :
              (a : P ⟶ (restrictedULiftYoneda A).obj X) →
                CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A ⟶
                  (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).obj X)
            (f ≫ g)))
    (NatTrans.app
      (((restrictedULiftYonedaHomEquiv'.{w, v₁, v₂, u₁, u₂} A P X).symm :
          (a : P ⟶ (restrictedULiftYoneda A).obj X) →
            CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A ⟶
              (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).obj X)
        (f ≫ g))
      p)
hg :
  Eq (α := A.obj p.left ⟶ X)
    (α.app p.left ≫
      L.map (p.hom ≫ f) ≫
        (Equiv.symm (IsColimit.homEquiv (Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension L α Q)) :
            (a :
                CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} Q ⋙ A ⟶
                  (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} Q)).obj X) →
              L.obj Q ⟶ X)
          (((restrictedULiftYonedaHomEquiv'.{w, v₁, v₂, u₁, u₂} A Q X).symm :
              (a : Q ⟶ (restrictedULiftYoneda A).obj X) →
                CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} Q ⋙ A ⟶
                  (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} Q)).obj X)
            g))
    (NatTrans.app
      (((restrictedULiftYonedaHomEquiv'.{w, v₁, v₂, u₁, u₂} A Q X).symm :
          (a : Q ⟶ (restrictedULiftYoneda A).obj X) →
            CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} Q ⋙ A ⟶
              (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} Q)).obj X)
        g)
      (Functor.obj (CostructuredArrow.map f) p))
⊢ Eq (α := A.obj p.left ⟶ X)
    ((α.app p.left ≫ L.map p.hom) ≫
      (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 X) →
            L.obj P ⟶ X)
        (((restrictedULiftYonedaHomEquiv'.{w, v₁, v₂, u₁, u₂} A P X).symm :
            (a : P ⟶ (restrictedULiftYoneda A).obj X) →
              CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A ⟶
                (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).obj X)
          (f ≫ g)))
    ((α.app p.left ≫ L.map p.hom) ≫
      L.map f ≫
        (Equiv.symm (IsColimit.homEquiv (Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension L α Q)) :
            (a :
                CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} Q ⋙ A ⟶
                  (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} Q)).obj X) →
              L.obj Q ⟶ X)
          (((restrictedULiftYonedaHomEquiv'.{w, v₁, v₂, u₁, u₂} A Q X).symm :
              (a : Q ⟶ (restrictedULiftYoneda A).obj X) →
                CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} Q ⋙ A ⟶
                  (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} Q)).obj X)
            g))

Tactic:
simp only [assoc, hfg, ← L.map_comp_assoc, hg,
          restrictedULiftYonedaHomEquiv'_symm_app_naturality_left]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Presheaf.restrictedULiftYonedaHomEquiv'_symm_app_naturality_left