-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
G : Functor.{v, w, u, w + 1} C (Type w)
E : Type u_1
inst_2 : Category.{v_1, u_1} E
c : C
X Y Z : (↑(F.obj c) : Type u₂)
f : X ⟶ Y
g : Y ⟶ Z
apply :
  Eq (α :=
    obj
        (Cat.Hom.toFunctor
          (F.map
            (Hom.base
              ({ base := 𝟙 { base := c, fiber := X : Grothendieck F }.base, fiber := eqToHom ⋯ ≫ f :
                  { base := c, fiber := X : Grothendieck F }.Hom { base := c, fiber := Y : Grothendieck F } } ≫
                { base := 𝟙 { base := c, fiber := Y : Grothendieck F }.base, fiber := eqToHom ⋯ ≫ g :
                  { base := c, fiber := Y : Grothendieck F }.Hom { base := c, fiber := Z : Grothendieck F } }))))
        { base := c, fiber := X : Grothendieck F }.fiber ⟶
      { base := c, fiber := Z : Grothendieck F }.fiber)
    (CategoryStruct.comp (Y :=
        (F.map
                { base := 𝟙 { base := c, fiber := X : Grothendieck F }.base, fiber := eqToHom ⋯ ≫ f ≫ g :
                    { base := c, fiber := X : Grothendieck F }.Hom
                      { base := c, fiber := Z : Grothendieck F } }.base).toFunctor.obj
          { base := c, fiber := X }.fiber)
        (eqToHom ⋯) { base := 𝟙 { base := c, fiber := X : Grothendieck F }.base, fiber := eqToHom ⋯ ≫ f ≫ g }.fiber :
      obj
          (Cat.Hom.toFunctor
            (F.map
              (Hom.base
                ({ base := 𝟙 { base := c, fiber := X : Grothendieck F }.base, fiber := eqToHom ⋯ ≫ f :
                    { base := c, fiber := X : Grothendieck F }.Hom { base := c, fiber := Y : Grothendieck F } } ≫
                  { base := 𝟙 { base := c, fiber := Y : Grothendieck F }.base, fiber := eqToHom ⋯ ≫ g :
                    { base := c, fiber := Y : Grothendieck F }.Hom { base := c, fiber := Z : Grothendieck F } }))))
          { base := c, fiber := X : Grothendieck F }.fiber ⟶
        { base := c, fiber := Z : Grothendieck F }.fiber)
    (Hom.fiber
        ({ base := 𝟙 { base := c, fiber := X : Grothendieck F }.base, fiber := eqToHom ⋯ ≫ f :
            { base := c, fiber := X : Grothendieck F }.Hom { base := c, fiber := Y : Grothendieck F } } ≫
          { base := 𝟙 { base := c, fiber := Y : Grothendieck F }.base, fiber := eqToHom ⋯ ≫ g }) :
      obj
          (Cat.Hom.toFunctor
            (F.map
              (Hom.base
                ({ base := 𝟙 { base := c, fiber := X : Grothendieck F }.base, fiber := eqToHom ⋯ ≫ f :
                    { base := c, fiber := X : Grothendieck F }.Hom { base := c, fiber := Y : Grothendieck F } } ≫
                  { base := 𝟙 { base := c, fiber := Y : Grothendieck F }.base, fiber := eqToHom ⋯ ≫ g :
                    { base := c, fiber := Y : Grothendieck F }.Hom { base := c, fiber := Z : Grothendieck F } }))))
          { base := c, fiber := X : Grothendieck F }.fiber ⟶
        { base := c, fiber := Z : Grothendieck F }.fiber)
⊢ { base := 𝟙 { base := c, fiber := X : Grothendieck F }.base, fiber := eqToHom ⋯ ≫ f ≫ g :
      { base := c, fiber := X : Grothendieck F }.Hom { base := c, fiber := Z : Grothendieck F } } =
    { base := 𝟙 { base := c, fiber := X : Grothendieck F }.base, fiber := eqToHom ⋯ ≫ f :
        { base := c, fiber := X : Grothendieck F }.Hom { base := c, fiber := Y : Grothendieck F } } ≫
      { base := 𝟙 { base := c, fiber := Y : Grothendieck F }.base, fiber := eqToHom ⋯ ≫ g }

Tactic:
apply Grothendieck.ext _ _ (by simp)

Premises used: CategoryTheory.Grothendieck.ext