-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (hypothesis)
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 (α := Functor.obj (CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A) p ⟶ X)
    (((Functor.LeftExtension.mk L α).coconeAt P).ι.app p ≫
      ((restrictedULiftYonedaHomEquiv.{w, v₁, v₂, u₁, u₂} L α P X).symm :
          (a : P ⟶ (restrictedULiftYoneda A).obj X) → L.obj P ⟶ X)
        (f ≫ g))
    (((Functor.LeftExtension.mk L α).coconeAt P).ι.app p ≫
      L.map f ≫
        ((restrictedULiftYonedaHomEquiv.{w, v₁, v₂, u₁, u₂} L α Q X).symm :
            (a : Q ⟶ (restrictedULiftYoneda A).obj X) → L.obj Q ⟶ X)
          g)
have hg : 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)