-- 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.{v₁ + 1} (α :=
    ((Grothendieck.ι F X).obj d).base ⟶ ((Grothendieck.ι F Z).obj ((F.map (f ≫ g)).toFunctor.obj d)).base)
    (Grothendieck.Hom.base
      { base := f ≫ g, fiber := 𝟙 ((F.map (f ≫ g)).toFunctor.obj ((Grothendieck.ι F X).obj d).fiber) })
    (Grothendieck.Hom.base
      (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) }))
w₁ :
  Eq.{u_2 + 1} (α :=
    obj
        (Cat.Hom.toFunctor
          (F.map
            (Grothendieck.Hom.base
              (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) :
                    ((Grothendieck.ι F X).obj d).Hom ((Grothendieck.ι F Y).obj ((F.map f).toFunctor.obj d)) }
                  { base := g,
                    fiber := 𝟙 ((F.map g).toFunctor.obj ((Grothendieck.ι F Y).obj ((F.map f).toFunctor.obj d)).fiber) :
                    ((Grothendieck.ι F Y).obj ((F.map f).toFunctor.obj d)).Hom
                      ((Grothendieck.ι F Z).obj ((F.map g).toFunctor.obj ((F.map f).toFunctor.obj d))) })
                { 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) :
                  ((Grothendieck.ι F Z).obj ((F.map g).toFunctor.obj ((F.map f).toFunctor.obj d))).Hom
                    ((Grothendieck.ι F Z).obj ((F.map (f ≫ g)).toFunctor.obj d)) }))))
        ((Grothendieck.ι F X).obj d).fiber ⟶
      ((Grothendieck.ι F Z).obj ((F.map (f ≫ g)).toFunctor.obj d)).fiber)
    (CategoryStruct.comp (Y :=
      obj
        (Cat.Hom.toFunctor
          (F.map
            (Grothendieck.Hom.base
              { base := f ≫ g, fiber := 𝟙 ((F.map (f ≫ g)).toFunctor.obj ((Grothendieck.ι F X).obj d).fiber) :
                ((Grothendieck.ι F X).obj d).Hom ((Grothendieck.ι F Z).obj ((F.map (f ≫ g)).toFunctor.obj d)) })))
        ((Grothendieck.ι F X).obj d).fiber)
      (eqToHom ⋯)
      (Grothendieck.Hom.fiber
        { base := f ≫ g, fiber := 𝟙 ((F.map (f ≫ g)).toFunctor.obj ((Grothendieck.ι F X).obj d).fiber) }))
    (Grothendieck.Hom.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 (α := (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) })

Tactic:
fapply Grothendieck.ext

Premises used: CategoryTheory.Grothendieck.ext