-- Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst_1 : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst_2 : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
d : (↑(F.obj X) : Type u_1)
w :
  Eq (α := (Grothendieck.ι F X).obj d ⟶ (Grothendieck.ι F Z).obj ((F.map (f ≫ g)).toFunctor.obj d))
    { base := f ≫ g, fiber := 𝟙 ((F.map (f ≫ g)).toFunctor.obj ((Grothendieck.ι F X).obj d).fiber) }
    (CategoryStruct.comp (Y := (Grothendieck.ι F Z).obj ((F.map g).toFunctor.obj ((F.map f).toFunctor.obj d)))
      (CategoryStruct.comp (Y := (Grothendieck.ι F Y).obj ((F.map f).toFunctor.obj d))
        { base := f, fiber := 𝟙 ((F.map f).toFunctor.obj ((Grothendieck.ι F X).obj d).fiber) }
        { base := g,
          fiber := 𝟙 ((F.map g).toFunctor.obj ((Grothendieck.ι F Y).obj ((F.map f).toFunctor.obj d)).fiber) })
      { base := eqToHom ⋯,
        fiber :=
          (eqToHom ⋯ :
            obj
                (Cat.Hom.toFunctor (F.map (eqToHom ⋯)) :
                  Functor.{u_2, u_2, u_1, u_1}
                    (↑(F.obj ((Grothendieck.ι F Z).obj ((F.map g).toFunctor.obj ((F.map f).toFunctor.obj d))).base) :
                      Type u_1)
                    (↑(F.obj ((Grothendieck.ι F Z).obj ((F.map (f ≫ g)).toFunctor.obj d)).base) : Type u_1))
                ((Grothendieck.ι F Z).obj ((F.map g).toFunctor.obj ((F.map f).toFunctor.obj d))).fiber ⟶
              ((Grothendieck.ι F Z).obj ((F.map (f ≫ g)).toFunctor.obj d)).fiber) })
⊢ Eq (α := G.obj ((Grothendieck.ι F X).obj d) ⟶ colimit (Grothendieck.ι F Z ⋙ G))
    (CategoryStruct.comp (Y := G.obj ((Grothendieck.ι F Z).obj ((F.map (f ≫ g)).toFunctor.obj d)))
      (G.map { base := f ≫ g, fiber := 𝟙 ((F.map (f ≫ g)).toFunctor.obj ((Grothendieck.ι F X).obj d).fiber) })
      (colimit.ι (Grothendieck.ι F Z ⋙ G) ((F.map (f ≫ g)).toFunctor.obj d)))
    (CategoryStruct.comp (Y := (Grothendieck.ι F Z ⋙ G).obj ((F.map (f ≫ g)).toFunctor.obj d))
      (G.map
        (CategoryStruct.comp (Y := (Grothendieck.ι F Z).obj ((F.map g).toFunctor.obj ((F.map f).toFunctor.obj d)))
          (CategoryStruct.comp (Y := (Grothendieck.ι F Y).obj ((F.map f).toFunctor.obj d))
            { base := f, fiber := 𝟙 ((F.map f).toFunctor.obj ((Grothendieck.ι F X).obj d).fiber) }
            { base := g,
              fiber := 𝟙 ((F.map g).toFunctor.obj ((Grothendieck.ι F Y).obj ((F.map f).toFunctor.obj d)).fiber) })
          { base := eqToHom ⋯,
            fiber :=
              (eqToHom ⋯ :
                obj
                    (Cat.Hom.toFunctor (F.map (eqToHom ⋯)) :
                      Functor.{u_2, u_2, u_1, u_1}
                        (↑(F.obj
                              ((Grothendieck.ι F Z).obj ((F.map g).toFunctor.obj ((F.map f).toFunctor.obj d))).base) :
                          Type u_1)
                        (↑(F.obj ((Grothendieck.ι F Z).obj ((F.map (f ≫ g)).toFunctor.obj d)).base) : Type u_1))
                    ((Grothendieck.ι F Z).obj ((F.map g).toFunctor.obj ((F.map f).toFunctor.obj d))).fiber ⟶
                  ((Grothendieck.ι F Z).obj ((F.map (f ≫ g)).toFunctor.obj d)).fiber) }))
      (colimit.ι (Grothendieck.ι F Z ⋙ G) ((F.map (f ≫ g)).toFunctor.obj d)))

Tactic:
congr 2