∀ {C : Type u_6} [inst : CategoryTheory.Category.{u_5, u_6} C] {F : CategoryTheory.Functor C CategoryTheory.Cat}
  {H : Type u_2} [inst_1 : CategoryTheory.Category.{u_1, u_2} 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))]
  {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimMap
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Functor.whiskerRight
            (CategoryTheory.Grothendieck.ιNatTrans (CategoryTheory.CategoryStruct.comp f g)) G)
          ((F.map (CategoryTheory.CategoryStruct.comp f g)).toFunctor.associator (CategoryTheory.Grothendieck.ι F Z)
              G).hom))
      (CategoryTheory.Limits.colimit.pre ((CategoryTheory.Grothendieck.ι F Z).comp G)
        (F.map (CategoryTheory.CategoryStruct.comp f g)).toFunctor) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.colimMap
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Functor.whiskerRight (CategoryTheory.Grothendieck.ιNatTrans f) G)
            ((F.map f).toFunctor.associator (CategoryTheory.Grothendieck.ι F Y) G).hom))
        (CategoryTheory.Limits.colimit.pre ((CategoryTheory.Grothendieck.ι F Y).comp G) (F.map f).toFunctor))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.colimMap
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Functor.whiskerRight (CategoryTheory.Grothendieck.ιNatTrans g) G)
            ((F.map g).toFunctor.associator (CategoryTheory.Grothendieck.ι F Z) G).hom))
        (CategoryTheory.Limits.colimit.pre ((CategoryTheory.Grothendieck.ι F Z).comp G) (F.map g).toFunctor))