-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (goal)
Goal:
C D : Type u₁
inst : SmallCategory C
inst_1 : SmallCategory D
E : Type u₂
inst_2 : Category.{u₁, u₂} E
F : C ⥤ D
X : D
inst_3 : ∀ (X : D), HasColimitsOfShape.{u₁, u₁, u₁, u₂} (CostructuredArrow F X) E
G₁ G₂ : C ⥤ E
φ : G₁ ⟶ G₂
⊢ Eq (α :=
    Functor.obj (F.lan ⋙ Functor.obj (evaluation D E) X) G₁ ⟶
      Functor.obj
        (Functor.obj (Functor.whiskeringLeft (CostructuredArrow F X) C E) (CostructuredArrow.proj F X) ⋙ colim) G₂)
    (Functor.map (F.lan ⋙ Functor.obj (evaluation D E) X) φ ≫
      Iso.hom
        ((fun (G : C ⥤ E) ↦
            (IsColimit.coconePointUniqueUpToIso (F.isPointwiseLeftKanExtensionLeftKanExtensionUnit G X)
                (colimit.isColimit (CostructuredArrow.proj F X ⋙ G)) :
              ((Functor.LeftExtension.mk (F.leftKanExtension G) (F.leftKanExtensionUnit G)).coconeAt X).pt ≅
                (colimit.cocone
                    (Functor.obj
                      (Functor.obj (Functor.whiskeringLeft (CostructuredArrow F X) C E) (CostructuredArrow.proj F X))
                      G)).pt))
          G₂))
    (Iso.hom
        ((fun (G : C ⥤ E) ↦
            (IsColimit.coconePointUniqueUpToIso (F.isPointwiseLeftKanExtensionLeftKanExtensionUnit G X)
                (colimit.isColimit (CostructuredArrow.proj F X ⋙ G)) :
              ((Functor.LeftExtension.mk (F.leftKanExtension G) (F.leftKanExtensionUnit G)).coconeAt X).pt ≅
                (colimit.cocone
                    (Functor.obj
                      (Functor.obj (Functor.whiskeringLeft (CostructuredArrow F X) C E) (CostructuredArrow.proj F X))
                      G)).pt))
          G₁) ≫
      Functor.map
        (Functor.obj (Functor.whiskeringLeft (CostructuredArrow F X) C E) (CostructuredArrow.proj F X) ⋙ colim) φ)
have apply : ∀ (j : CostructuredArrow F X),
  Eq (α :=
    (CostructuredArrow.proj F X ⋙ G₁).obj j ⟶
      Functor.obj
        (Functor.obj (Functor.whiskeringLeft (CostructuredArrow F X) C E) (CostructuredArrow.proj F X) ⋙ colim) G₂)
    (((Functor.LeftExtension.mk (F.leftKanExtension G₁) (F.leftKanExtensionUnit G₁)).coconeAt X).ι.app j ≫
      Functor.map (F.lan ⋙ Functor.obj (evaluation D E) X) φ ≫
        Iso.hom
          ((fun (G : C ⥤ E) ↦
              (IsColimit.coconePointUniqueUpToIso (F.isPointwiseLeftKanExtensionLeftKanExtensionUnit G X)
                  (colimit.isColimit (CostructuredArrow.proj F X ⋙ G)) :
                ((Functor.LeftExtension.mk (F.leftKanExtension G) (F.leftKanExtensionUnit G)).coconeAt X).pt ≅
                  (colimit.cocone
                      (Functor.obj
                        (Functor.obj (Functor.whiskeringLeft (CostructuredArrow F X) C E) (CostructuredArrow.proj F X))
                        G)).pt))
            G₂))
    (((Functor.LeftExtension.mk (F.leftKanExtension G₁) (F.leftKanExtensionUnit G₁)).coconeAt X).ι.app j ≫
      Iso.hom
          ((fun (G : C ⥤ E) ↦
              (IsColimit.coconePointUniqueUpToIso (F.isPointwiseLeftKanExtensionLeftKanExtensionUnit G X)
                  (colimit.isColimit (CostructuredArrow.proj F X ⋙ G)) :
                ((Functor.LeftExtension.mk (F.leftKanExtension G) (F.leftKanExtensionUnit G)).coconeAt X).pt ≅
                  (colimit.cocone
                      (Functor.obj
                        (Functor.obj (Functor.whiskeringLeft (CostructuredArrow F X) C E) (CostructuredArrow.proj F X))
                        G)).pt))
            G₁) ≫
        Functor.map
          (Functor.obj (Functor.whiskeringLeft (CostructuredArrow F X) C E) (CostructuredArrow.proj F X) ⋙ colim) φ)
Tactic: apply (Functor.isPointwiseLeftKanExtensionLeftKanExtensionUnit F G₁ X).hom_ext