-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Grothendieck (goal)
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮 ⥤ᵖ Cat
α : F ⟶ G
a b c : ∫ F
f : a ⟶ b
g : b ⟶ c
hfg₁ :
  { base := (f ≫ g).base,
        fiber :=
          (α.naturality (f ≫ g).base.toLoc).inv.toNatTrans.app a.fiber ≫
            Functor.map (Cat.Hom.toFunctor (α.app { as := c.base : LocallyDiscrete 𝒮 })) (f ≫ g).fiber :
        { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) a.fiber :
              ∫ G }.Hom
          { base := c.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := c.base : LocallyDiscrete 𝒮 })) c.fiber :
            ∫ G } }.base =
    Hom.base
      ({ base := f.base,
          fiber :=
            (α.naturality f.base.toLoc).inv.toNatTrans.app a.fiber ≫
              Functor.map (Cat.Hom.toFunctor (α.app { as := b.base : LocallyDiscrete 𝒮 })) f.fiber :
          { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) a.fiber :
                ∫ G }.Hom
            { base := b.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := b.base : LocallyDiscrete 𝒮 })) b.fiber :
              ∫ G } } ≫
        { base := g.base,
          fiber :=
            (α.naturality g.base.toLoc).inv.toNatTrans.app b.fiber ≫
              Functor.map (Cat.Hom.toFunctor (α.app { as := c.base : LocallyDiscrete 𝒮 })) g.fiber })
⊢ { base := (f ≫ g).base,
      fiber :=
        (α.naturality (f ≫ g).base.toLoc).inv.toNatTrans.app a.fiber ≫
          Functor.map (Cat.Hom.toFunctor (α.app { as := c.base : LocallyDiscrete 𝒮 })) (f ≫ g).fiber :
      { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) a.fiber :
            ∫ G }.Hom
        { base := c.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := c.base : LocallyDiscrete 𝒮 })) c.fiber :
          ∫ G } } =
    { base := f.base,
        fiber :=
          (α.naturality f.base.toLoc).inv.toNatTrans.app a.fiber ≫
            Functor.map (Cat.Hom.toFunctor (α.app { as := b.base : LocallyDiscrete 𝒮 })) f.fiber :
        { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) a.fiber :
              ∫ G }.Hom
          { base := b.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := b.base : LocallyDiscrete 𝒮 })) b.fiber :
            ∫ G } } ≫
      { base := g.base,
        fiber :=
          (α.naturality g.base.toLoc).inv.toNatTrans.app b.fiber ≫
            Functor.map (Cat.Hom.toFunctor (α.app { as := c.base : LocallyDiscrete 𝒮 })) g.fiber }
have hfg₂ : Eq (α :=
  obj
      (Cat.Hom.toFunctor
        (G.map
          (Quiver.Hom.toLoc
            (Hom.base
              ({ base := f.base,
                  fiber :=
                    (α.naturality f.base.toLoc).inv.toNatTrans.app a.fiber ≫
                      Functor.map (Cat.Hom.toFunctor (α.app { as := b.base : LocallyDiscrete 𝒮 })) f.fiber :
                  { base := a.base,
                        fiber := obj (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) a.fiber :
                        ∫ G }.Hom
                    { base := b.base,
                      fiber := obj (Cat.Hom.toFunctor (α.app { as := b.base : LocallyDiscrete 𝒮 })) b.fiber : ∫ G } } ≫
                { base := g.base,
                  fiber :=
                    (α.naturality g.base.toLoc).inv.toNatTrans.app b.fiber ≫
                      Functor.map (Cat.Hom.toFunctor (α.app { as := c.base : LocallyDiscrete 𝒮 })) g.fiber :
                  { base := b.base,
                        fiber := obj (Cat.Hom.toFunctor (α.app { as := b.base : LocallyDiscrete 𝒮 })) b.fiber :
                        ∫ G }.Hom
                    { base := c.base,
                      fiber := obj (Cat.Hom.toFunctor (α.app { as := c.base : LocallyDiscrete 𝒮 })) c.fiber :
                      ∫ G } })))))
      { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) a.fiber :
          ∫ G }.fiber ⟶
    { base := c.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := c.base : LocallyDiscrete 𝒮 })) c.fiber :
        ∫ G }.fiber)
  (CategoryStruct.comp (Y :=
      (G.map
              { base := (f ≫ g).base,
                    fiber :=
                      (α.naturality (f ≫ g).base.toLoc).inv.toNatTrans.app a.fiber ≫
                        Functor.map (Cat.Hom.toFunctor (α.app { as := c.base : LocallyDiscrete 𝒮 })) (f ≫ g).fiber :
                    { base := a.base,
                          fiber := obj (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) a.fiber :
                          ∫ G }.Hom
                      { base := c.base,
                        fiber := obj (Cat.Hom.toFunctor (α.app { as := c.base : LocallyDiscrete 𝒮 })) c.fiber :
                        ∫ G } }.base.toLoc).toFunctor.obj
        { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) a.fiber }.fiber)
      (eqToHom sorry)
      { base := (f ≫ g).base,
          fiber :=
            (α.naturality (f ≫ g).base.toLoc).inv.toNatTrans.app a.fiber ≫
              Functor.map (Cat.Hom.toFunctor (α.app { as := c.base : LocallyDiscrete 𝒮 })) (f ≫ g).fiber }.fiber :
    obj
        (Cat.Hom.toFunctor
          (G.map
            (Quiver.Hom.toLoc
              (Hom.base
                ({ base := f.base,
                    fiber :=
                      (α.naturality f.base.toLoc).inv.toNatTrans.app a.fiber ≫
                        Functor.map (Cat.Hom.toFunctor (α.app { as := b.base : LocallyDiscrete 𝒮 })) f.fiber :
                    { base := a.base,
                          fiber := obj (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) a.fiber :
                          ∫ G }.Hom
                      { base := b.base,
                        fiber := obj (Cat.Hom.toFunctor (α.app { as := b.base : LocallyDiscrete 𝒮 })) b.fiber :
                        ∫ G } } ≫
                  { base := g.base,
                    fiber :=
                      (α.naturality g.base.toLoc).inv.toNatTrans.app b.fiber ≫
                        Functor.map (Cat.Hom.toFunctor (α.app { as := c.base : LocallyDiscrete 𝒮 })) g.fiber :
                    { base := b.base,
                          fiber := obj (Cat.Hom.toFunctor (α.app { as := b.base : LocallyDiscrete 𝒮 })) b.fiber :
                          ∫ G }.Hom
                      { base := c.base,
                        fiber := obj (Cat.Hom.toFunctor (α.app { as := c.base : LocallyDiscrete 𝒮 })) c.fiber :
                        ∫ G } })))))
        { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) a.fiber :
            ∫ G }.fiber ⟶
      { base := c.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := c.base : LocallyDiscrete 𝒮 })) c.fiber :
          ∫ G }.fiber)
  (Hom.fiber
      ({ base := f.base,
          fiber :=
            (α.naturality f.base.toLoc).inv.toNatTrans.app a.fiber ≫
              Functor.map (Cat.Hom.toFunctor (α.app { as := b.base : LocallyDiscrete 𝒮 })) f.fiber :
          { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) a.fiber :
                ∫ G }.Hom
            { base := b.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := b.base : LocallyDiscrete 𝒮 })) b.fiber :
              ∫ G } } ≫
        { base := g.base,
          fiber :=
            (α.naturality g.base.toLoc).inv.toNatTrans.app b.fiber ≫
              Functor.map (Cat.Hom.toFunctor (α.app { as := c.base : LocallyDiscrete 𝒮 })) g.fiber }) :
    obj
        (Cat.Hom.toFunctor
          (G.map
            (Quiver.Hom.toLoc
              (Hom.base
                ({ base := f.base,
                    fiber :=
                      (α.naturality f.base.toLoc).inv.toNatTrans.app a.fiber ≫
                        Functor.map (Cat.Hom.toFunctor (α.app { as := b.base : LocallyDiscrete 𝒮 })) f.fiber :
                    { base := a.base,
                          fiber := obj (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) a.fiber :
                          ∫ G }.Hom
                      { base := b.base,
                        fiber := obj (Cat.Hom.toFunctor (α.app { as := b.base : LocallyDiscrete 𝒮 })) b.fiber :
                        ∫ G } } ≫
                  { base := g.base,
                    fiber :=
                      (α.naturality g.base.toLoc).inv.toNatTrans.app b.fiber ≫
                        Functor.map (Cat.Hom.toFunctor (α.app { as := c.base : LocallyDiscrete 𝒮 })) g.fiber :
                    { base := b.base,
                          fiber := obj (Cat.Hom.toFunctor (α.app { as := b.base : LocallyDiscrete 𝒮 })) b.fiber :
                          ∫ G }.Hom
                      { base := c.base,
                        fiber := obj (Cat.Hom.toFunctor (α.app { as := c.base : LocallyDiscrete 𝒮 })) c.fiber :
                        ∫ G } })))))
        { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) a.fiber :
            ∫ G }.fiber ⟶
      { base := c.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := c.base : LocallyDiscrete 𝒮 })) c.fiber :
          ∫ G }.fiber)
Tactic: ext