-- 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
⊢ 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 ⋯)
        { 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)
have hfg₂ : Eq (α :=
  (G.map (f.base.toLoc ≫ g.base.toLoc)).toFunctor.obj
      (obj (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) a.fiber) ⟶
    obj (Cat.Hom.toFunctor (α.app { as := c.base : LocallyDiscrete 𝒮 })) c.fiber)
  (𝟙
      ((G.map (f.base.toLoc ≫ g.base.toLoc)).toFunctor.obj
        (obj (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) a.fiber)) ≫
    (α.naturality (f.base.toLoc ≫ g.base.toLoc)).inv.toNatTrans.app a.fiber ≫
      Functor.map (Cat.Hom.toFunctor (α.app { as := c.base : LocallyDiscrete 𝒮 }))
          ((F.mapComp f.base.toLoc g.base.toLoc).hom.toNatTrans.app a.fiber) ≫
        ((F.map g.base.toLoc).toFunctor ⋙ Cat.Hom.toFunctor (α.app { as := c.base : LocallyDiscrete 𝒮 })).map f.fiber ≫
          Functor.map (Cat.Hom.toFunctor (α.app { as := c.base : LocallyDiscrete 𝒮 })) g.fiber)
  ((G.mapComp f.base.toLoc g.base.toLoc).hom.toNatTrans.app
      (obj (Cat.Hom.toFunctor (α.app { as := a.base : LocallyDiscrete 𝒮 })) a.fiber) ≫
    (G.map g.base.toLoc).toFunctor.map ((α.naturality f.base.toLoc).inv.toNatTrans.app a.fiber) ≫
      (α.naturality g.base.toLoc).inv.toNatTrans.app ((F.map f.base.toLoc).toFunctor.obj a.fiber) ≫
        ((F.map g.base.toLoc).toFunctor ⋙ Cat.Hom.toFunctor (α.app { as := c.base : LocallyDiscrete 𝒮 })).map f.fiber ≫
          Functor.map (Cat.Hom.toFunctor (α.app { as := c.base : LocallyDiscrete 𝒮 })) g.fiber)
Tactic: simp only [Cat.Hom.comp_toFunctor, comp_obj, categoryStruct_comp_base, Quiver.Hom.comp_toLoc,
        categoryStruct_comp_fiber, eqToHom_refl, map_comp, ← Cat.Hom.comp_map, assoc,
        NatTrans.naturality_assoc]