-- 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 (α :=
    { base := c, fiber := f : Grothendieck F } ⟶
      { 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) })
    ({ 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 := 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) })))
  (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 sorry ≫ Functor.map (Cat.Hom.toFunctor (F.map (coeqHom u v))) x)
            (Functor.map (Cat.Hom.toFunctor (F.map (coeqHom u v))) y) }))
Tactic: apply Grothendieck.ext _ _ (coeq_condition u v)