-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Grothendieck (goal)
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
⊢ 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) }))
have 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 sorry ≫ 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 sorry ≫ 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 sorry ≫ 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 sorry ≫ 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 sorry ≫ 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 sorry)
    (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 sorry ≫ Functor.map (Cat.Hom.toFunctor (F.map (coeqHom u v))) x)
              (Functor.map (Cat.Hom.toFunctor (F.map (coeqHom u v))) y) })))
  (eqToHom sorry ≫
    (eqToHom sorry ≫ Functor.map (Cat.Hom.toFunctor (F.map (coeqHom u v))) x) ≫
      coeqHom (eqToHom sorry ≫ 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 _ _)