-- 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₂
T : CostructuredArrow F X
h₁ :
  ∀ (G : C ⥤ E),
    ((Functor.LeftExtension.mk (F.leftKanExtension G) (F.leftKanExtensionUnit G)).coconeAt X).ι.app T ≫
        Iso.hom
          (IsColimit.coconePointUniqueUpToIso (F.isPointwiseLeftKanExtensionLeftKanExtensionUnit G X)
            (colimit.isColimit (CostructuredArrow.proj F X ⋙ G))) =
      (colimit.cocone (CostructuredArrow.proj F X ⋙ G)).ι.app T
h₂ :
  Eq (α :=
    (Functor.obj (𝟭 (C ⥤ E)) G₁).obj T.left ⟶
      (Functor.obj (F.lan ⋙ Functor.obj (Functor.whiskeringLeft C D E) F) G₂).obj T.left)
    (NatTrans.app (Functor.map (𝟭 (C ⥤ E)) φ ≫ NatTrans.app F.lanUnit G₂) T.left)
    (NatTrans.app (NatTrans.app F.lanUnit G₁ ≫ Functor.map (F.lan ⋙ Functor.obj (Functor.whiskeringLeft C D E) F) φ)
      T.left)
⊢ Eq (α :=
    (CostructuredArrow.proj F X ⋙ G₁).obj T ⟶
      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 T ≫
      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 T ≫
      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 dsimp : Eq (α := G₁.obj T.left ⟶ colimit (CostructuredArrow.proj F X ⋙ G₂))
  ((NatTrans.app (F.leftKanExtensionUnit G₁) T.left ≫ (F.leftKanExtension G₁).map T.hom) ≫
    NatTrans.app (Functor.map F.lan φ) X ≫
      Iso.hom
        (IsColimit.coconePointUniqueUpToIso (F.isPointwiseLeftKanExtensionLeftKanExtensionUnit G₂ X)
          (colimit.isColimit (CostructuredArrow.proj F X ⋙ G₂))))
  ((NatTrans.app (F.leftKanExtensionUnit G₁) T.left ≫ (F.leftKanExtension G₁).map T.hom) ≫
    CategoryStruct.comp (Y := colimit (CostructuredArrow.proj F X ⋙ G₁))
      (Iso.hom
        (IsColimit.coconePointUniqueUpToIso (F.isPointwiseLeftKanExtensionLeftKanExtensionUnit G₁ X)
          (colimit.isColimit (CostructuredArrow.proj F X ⋙ G₁))))
      (colimMap ((CostructuredArrow.proj F X).whiskerLeft φ)))
Tactic: dsimp at h₁ h₂ ⊢