∀ {C : Type u_4} [inst : CategoryTheory.Category.{u_1, u_4} C] {F : CategoryTheory.Functor C CategoryTheory.Cat}
  {H : Type u_6} [inst_1 : CategoryTheory.Category.{u_3, u_6} H]
  {G : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H}
  [inst_2 :
    ∀ {X Y : C} (f : X ⟶ Y),
      CategoryTheory.Limits.HasColimit ((F.map f).toFunctor.comp ((CategoryTheory.Grothendieck.ι F Y).comp G))]
  {c : CategoryTheory.Limits.Cocone (CategoryTheory.Limits.fiberwiseColimit G)} (hc : CategoryTheory.Limits.IsColimit c)
  (s : CategoryTheory.Limits.Cocone G) (j : CategoryTheory.Grothendieck F),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.coconeOfCoconeFiberwiseColimit c).ι.app j)
      (hc.desc
        { pt := s.pt,
          ι :=
            {
              app := fun X =>
                CategoryTheory.Limits.colimit.desc ((CategoryTheory.Grothendieck.ι F X).comp G)
                  (CategoryTheory.Limits.Cocone.whisker (CategoryTheory.Grothendieck.ι F X) s),
              naturality := ⋯ } }) =
    s.ι.app j