-- 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)
    ((StructuredArrow.hom (Functor.LeftExtension.mk L α)).app p.left ≫
      (StructuredArrow.right (Functor.LeftExtension.mk 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) →
              ((Functor.LeftExtension.mk L α).coconeAt P).pt ⟶ 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)
⊢ Eq (α := A.obj (Functor.obj (CostructuredArrow.map f) p).left ⟶ X)
    ((StructuredArrow.hom (Functor.LeftExtension.mk L α)).app (Functor.obj (CostructuredArrow.map f) p).left ≫
      (StructuredArrow.right (Functor.LeftExtension.mk L α)).map (Functor.obj (CostructuredArrow.map f) p).hom ≫
        (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) →
              ((Functor.LeftExtension.mk L α).coconeAt Q).pt ⟶ 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))

Tactic:
have hg := (Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension
          L α Q).comp_homEquiv_symm ((restrictedULiftYonedaHomEquiv' A Q X).symm g)
            ((CostructuredArrow.map f).obj p)