-- 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₂
T : CostructuredArrow F X
h₂ :
  Eq (α := G₁.obj T.left ⟶ (Functor.obj F.lan G₂).obj (F.obj T.left))
    (φ.app T.left ≫ NatTrans.app (NatTrans.app F.lanUnit G₂) T.left)
    (NatTrans.app (NatTrans.app F.lanUnit G₁) T.left ≫ NatTrans.app (Functor.map F.lan φ) (F.obj T.left))
h₁ :
  ∀ (G : C ⥤ E),
    Eq (α := G.obj T.left ⟶ colimit (CostructuredArrow.proj F X ⋙ G))
      (NatTrans.app (F.leftKanExtensionUnit G) T.left ≫
        (F.leftKanExtension G).map T.hom ≫
          Iso.hom
            (IsColimit.coconePointUniqueUpToIso (F.isPointwiseLeftKanExtensionLeftKanExtensionUnit G X)
              (colimit.isColimit (CostructuredArrow.proj F X ⋙ G))))
      (colimit.ι (CostructuredArrow.proj F X ⋙ G) T)
simp :
  Eq (α := G₁.obj T.left ⟶ colimit (CostructuredArrow.proj F X ⋙ G₂))
    (NatTrans.app (F.leftKanExtensionUnit G₁) T.left ≫
      (F.leftKanExtension G₁).map T.hom ≫
        CategoryStruct.comp (Y := (F.leftKanExtension G₂).obj X)
          (NatTrans.app
              ((F.leftKanExtension G₁).descOfIsLeftKanExtension (F.leftKanExtensionUnit G₁) (F.leftKanExtension G₂)
                (φ ≫ F.leftKanExtensionUnit G₂))
              X :
            (F.leftKanExtension G₁).obj X ⟶ (F.leftKanExtension G₂).obj X)
          (Iso.hom
              (IsColimit.coconePointUniqueUpToIso (F.isPointwiseLeftKanExtensionLeftKanExtensionUnit G₂ X)
                (colimit.isColimit (CostructuredArrow.proj F X ⋙ G₂))) :
            (F.leftKanExtension G₂).obj X ⟶ colimit (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 φ)))
⊢ 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:
simp only [Functor.lan, Functor.lanUnit] at h₂ ⊢

Premises used: CategoryTheory.Functor.lan, CategoryTheory.Functor.lanUnit