∀ {C : Type u_1} {D : Type u_4} [inst : CategoryTheory.Category.{u_3, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_2, u_4} D] (L : CategoryTheory.Functor C D) {H : Type u_6}
  [inst_2 : CategoryTheory.Category.{u_5, u_6} H] (F : CategoryTheory.Functor C H)
  [inst_3 : L.HasPointwiseLeftKanExtension F] [inst_4 : L.HasLeftKanExtension F] {X Y : D} (f : X ⟶ Y)
  (j : ↑((CategoryTheory.CostructuredArrow.functor L).obj X)),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimit.ι
        ((CategoryTheory.Grothendieck.ι (CategoryTheory.CostructuredArrow.functor L) X).comp
          ((CategoryTheory.CostructuredArrow.grothendieckProj L).comp F))
        j)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Limits.fiberwiseColimit ((CategoryTheory.CostructuredArrow.grothendieckProj L).comp F)).map f)
        ((fun X =>
              CategoryTheory.Limits.HasColimit.isoOfNatIso
                  (CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.CostructuredArrow.ιCompGrothendieckProj L X)
                    F) ≪≫
                (L.leftKanExtensionObjIsoColimit F X).symm)
            Y).hom) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimit.ι
        ((CategoryTheory.Grothendieck.ι (CategoryTheory.CostructuredArrow.functor L) X).comp
          ((CategoryTheory.CostructuredArrow.grothendieckProj L).comp F))
        j)
      (CategoryTheory.CategoryStruct.comp
        ((fun X =>
              CategoryTheory.Limits.HasColimit.isoOfNatIso
                  (CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.CostructuredArrow.ιCompGrothendieckProj L X)
                    F) ≪≫
                (L.leftKanExtensionObjIsoColimit F X).symm)
            X).hom
        ((L.leftKanExtension F).map f))