-- Module: Mathlib.CategoryTheory.Functor.Flat
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₂
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) φ)
⊢ 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) φ)

Tactic:
apply (Functor.isPointwiseLeftKanExtensionLeftKanExtensionUnit F G₁ X).hom_ext

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