-- Module: Mathlib.CategoryTheory.Filtered.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
F : C ⥤ Cat
inst_1 : IsFilteredOrEmpty.{v, u} C
inst_2 : ∀ (c : C), IsFilteredOrEmpty.{u_1, u_2} (↑(F.obj c) : Type u_2)
c : C
f : (↑(F.obj c) : Type u_2)
d : C
g : (↑(F.obj d) : Type u_2)
u : { base := c, fiber := f : Grothendieck F }.base ⟶ { base := d, fiber := g : Grothendieck F }.base
x : (F.map u).toFunctor.obj { base := c, fiber := f : Grothendieck F }.fiber ⟶ { base := d, fiber := g }.fiber
v : { base := c, fiber := f : Grothendieck F }.base ⟶ { base := d, fiber := g : Grothendieck F }.base
y : (F.map v).toFunctor.obj { base := c, fiber := f : Grothendieck F }.fiber ⟶ { base := d, fiber := g }.fiber
refine_2 :
  Eq.{u_1 + 1} (α :=
    Functor.obj
        (Cat.Hom.toFunctor
          (F.map
            (Grothendieck.Hom.base
              ({ base := v, fiber := y :
                  { base := c, fiber := f : Grothendieck F }.Hom { base := d, fiber := g : Grothendieck F } } ≫
                { base := coeqHom u v,
                  fiber :=
                    coeqHom (eqToHom ⋯ ≫ Functor.map (Cat.Hom.toFunctor (F.map (coeqHom u v))) x)
                      (Functor.map (Cat.Hom.toFunctor (F.map (coeqHom u v))) y) :
                  { base := d, fiber := g : Grothendieck F }.Hom
                    { base := coeq u v,
                      fiber :=
                        coeq (j :=
                          Functor.obj (Cat.Hom.toFunctor (F.map (coeqHom u v)))
                            ((F.map v).toFunctor.obj { base := c, fiber := f : Grothendieck F }.fiber))
                          (eqToHom ⋯ ≫ Functor.map (Cat.Hom.toFunctor (F.map (coeqHom u v))) x)
                          (Functor.map (Cat.Hom.toFunctor (F.map (coeqHom u v))) y) :
                      Grothendieck F } }))))
        { base := c, fiber := f : Grothendieck F }.fiber ⟶
      { base := coeq u v,
          fiber :=
            coeq (j :=
              Functor.obj (Cat.Hom.toFunctor (F.map (coeqHom u v)))
                ((F.map v).toFunctor.obj { base := c, fiber := f : Grothendieck F }.fiber))
              (eqToHom ⋯ ≫ Functor.map (Cat.Hom.toFunctor (F.map (coeqHom u v))) x)
              (Functor.map (Cat.Hom.toFunctor (F.map (coeqHom u v))) y) :
          Grothendieck F }.fiber)
    (CategoryStruct.comp (Y :=
      Functor.obj
        (Cat.Hom.toFunctor
          (F.map
            (Grothendieck.Hom.base
              ({ base := u, fiber := x :
                  { base := c, fiber := f : Grothendieck F }.Hom { base := d, fiber := g : Grothendieck F } } ≫
                { base := coeqHom u v,
                  fiber :=
                    coeqHom (eqToHom ⋯ ≫ Functor.map (Cat.Hom.toFunctor (F.map (coeqHom u v))) x)
                      (Functor.map (Cat.Hom.toFunctor (F.map (coeqHom u v))) y) :
                  { base := d, fiber := g : Grothendieck F }.Hom
                    { base := coeq u v,
                      fiber :=
                        coeq (j :=
                          Functor.obj (Cat.Hom.toFunctor (F.map (coeqHom u v)))
                            ((F.map v).toFunctor.obj { base := c, fiber := f : Grothendieck F }.fiber))
                          (eqToHom ⋯ ≫ Functor.map (Cat.Hom.toFunctor (F.map (coeqHom u v))) x)
                          (Functor.map (Cat.Hom.toFunctor (F.map (coeqHom u v))) y) :
                      Grothendieck F } }))))
        { base := c, fiber := f : Grothendieck F }.fiber)
      (eqToHom ⋯)
      (Grothendieck.Hom.fiber
        ({ base := u, fiber := x :
            { base := c, fiber := f : Grothendieck F }.Hom { base := d, fiber := g : Grothendieck F } } ≫
          { base := coeqHom u v,
            fiber :=
              coeqHom (eqToHom ⋯ ≫ Functor.map (Cat.Hom.toFunctor (F.map (coeqHom u v))) x)
                (Functor.map (Cat.Hom.toFunctor (F.map (coeqHom u v))) y) })))
    (eqToHom ⋯ ≫
      (eqToHom ⋯ ≫ Functor.map (Cat.Hom.toFunctor (F.map (coeqHom u v))) x) ≫
        coeqHom (eqToHom ⋯ ≫ Functor.map (Cat.Hom.toFunctor (F.map (coeqHom u v))) x)
          (Functor.map (Cat.Hom.toFunctor (F.map (coeqHom u v))) y))
⊢ Eq.{u_1 + 1} (α :=
    Functor.obj
        (Cat.Hom.toFunctor
          (F.map
            (Grothendieck.Hom.base
              ({ base := v, fiber := y :
                  { base := c, fiber := f : Grothendieck F }.Hom { base := d, fiber := g : Grothendieck F } } ≫
                { base := coeqHom u v,
                  fiber :=
                    coeqHom (eqToHom ⋯ ≫ Functor.map (Cat.Hom.toFunctor (F.map (coeqHom u v))) x)
                      (Functor.map (Cat.Hom.toFunctor (F.map (coeqHom u v))) y) :
                  { base := d, fiber := g : Grothendieck F }.Hom
                    { base := coeq u v,
                      fiber :=
                        coeq (j :=
                          Functor.obj (Cat.Hom.toFunctor (F.map (coeqHom u v)))
                            ((F.map v).toFunctor.obj { base := c, fiber := f : Grothendieck F }.fiber))
                          (eqToHom ⋯ ≫ Functor.map (Cat.Hom.toFunctor (F.map (coeqHom u v))) x)
                          (Functor.map (Cat.Hom.toFunctor (F.map (coeqHom u v))) y) :
                      Grothendieck F } }))))
        { base := c, fiber := f : Grothendieck F }.fiber ⟶
      { base := coeq u v,
          fiber :=
            coeq (j :=
              Functor.obj (Cat.Hom.toFunctor (F.map (coeqHom u v)))
                ((F.map v).toFunctor.obj { base := c, fiber := f : Grothendieck F }.fiber))
              (eqToHom ⋯ ≫ Functor.map (Cat.Hom.toFunctor (F.map (coeqHom u v))) x)
              (Functor.map (Cat.Hom.toFunctor (F.map (coeqHom u v))) y) :
          Grothendieck F }.fiber)
    (CategoryStruct.comp (Y :=
      Functor.obj
        (Cat.Hom.toFunctor
          (F.map
            (Grothendieck.Hom.base
              ({ base := u, fiber := x :
                  { base := c, fiber := f : Grothendieck F }.Hom { base := d, fiber := g : Grothendieck F } } ≫
                { base := coeqHom u v,
                  fiber :=
                    coeqHom (eqToHom ⋯ ≫ Functor.map (Cat.Hom.toFunctor (F.map (coeqHom u v))) x)
                      (Functor.map (Cat.Hom.toFunctor (F.map (coeqHom u v))) y) :
                  { base := d, fiber := g : Grothendieck F }.Hom
                    { base := coeq u v,
                      fiber :=
                        coeq (j :=
                          Functor.obj (Cat.Hom.toFunctor (F.map (coeqHom u v)))
                            ((F.map v).toFunctor.obj { base := c, fiber := f : Grothendieck F }.fiber))
                          (eqToHom ⋯ ≫ Functor.map (Cat.Hom.toFunctor (F.map (coeqHom u v))) x)
                          (Functor.map (Cat.Hom.toFunctor (F.map (coeqHom u v))) y) :
                      Grothendieck F } }))))
        { base := c, fiber := f : Grothendieck F }.fiber)
      (eqToHom ⋯)
      (Grothendieck.Hom.fiber
        ({ base := u, fiber := x :
            { base := c, fiber := f : Grothendieck F }.Hom { base := d, fiber := g : Grothendieck F } } ≫
          { base := coeqHom u v,
            fiber :=
              coeqHom (eqToHom ⋯ ≫ Functor.map (Cat.Hom.toFunctor (F.map (coeqHom u v))) x)
                (Functor.map (Cat.Hom.toFunctor (F.map (coeqHom u v))) y) })))
    (Grothendieck.Hom.fiber
      ({ base := v, fiber := y :
          { base := c, fiber := f : Grothendieck F }.Hom { base := d, fiber := g : Grothendieck F } } ≫
        { base := coeqHom u v,
          fiber :=
            coeqHom (eqToHom ⋯ ≫ Functor.map (Cat.Hom.toFunctor (F.map (coeqHom u v))) x)
              (Functor.map (Cat.Hom.toFunctor (F.map (coeqHom u v))) y) }))

Tactic:
refine Eq.trans ?_ (eqToHom _ ≫= coeq_condition _ _)

Premises used: CategoryTheory.eqToHom, CategoryTheory.IsFiltered.coeq_condition, CategoryTheory.whisker_eq, Eq.trans