-- Module: Mathlib.CategoryTheory.Bicategory.Grothendieck
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₂ :
  Functor.map (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ })) f.fiber ≫
      Functor.map (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ }))
          (Functor.map (Cat.Hom.toFunctor (F.map f.base.op.toLoc)) g.fiber) ≫
        Functor.map (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ }))
            (NatTrans.app (Cat.Hom₂.toNatTrans (Iso.inv (F.mapComp g.base.op.toLoc f.base.op.toLoc))) c.fiber) ≫
          Functor.map (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ }))
              (NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (F.mapComp g.base.op.toLoc f.base.op.toLoc))) c.fiber) ≫
            NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (α.naturality f.base.op.toLoc)))
                (obj (Cat.Hom.toFunctor (F.map g.base.op.toLoc)) c.fiber) ≫
              Functor.map (Cat.Hom.toFunctor (G.map f.base.op.toLoc))
                  (NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (α.naturality g.base.op.toLoc))) c.fiber) ≫
                NatTrans.app (Cat.Hom₂.toNatTrans (Iso.inv (G.mapComp g.base.op.toLoc f.base.op.toLoc)))
                  (obj (Cat.Hom.toFunctor (α.app { as := op c.base : LocallyDiscrete 𝒮ᵒᵖ })) c.fiber) =
    Functor.map (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ })) f.fiber ≫
      NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (α.naturality f.base.op.toLoc))) b.fiber ≫
        Functor.map (Cat.Hom.toFunctor (G.map f.base.op.toLoc))
            (Functor.map (Cat.Hom.toFunctor (α.app { as := op b.base : LocallyDiscrete 𝒮ᵒᵖ })) g.fiber) ≫
          Functor.map (Cat.Hom.toFunctor (G.map f.base.op.toLoc))
              (NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (α.naturality g.base.op.toLoc))) c.fiber) ≫
            NatTrans.app (Cat.Hom₂.toNatTrans (Iso.inv (G.mapComp g.base.op.toLoc f.base.op.toLoc)))
              (obj (Cat.Hom.toFunctor (α.app { as := op c.base : LocallyDiscrete 𝒮ᵒᵖ })) c.fiber)
⊢ Eq (α :=
    { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ })) a.fiber :
          ∫ᶜ G }.fiber ⟶
      obj
        (Cat.Hom.toFunctor
          (G.map
            { base := (f ≫ g).base,
                    fiber :=
                      Functor.map (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ })) (f ≫ g).fiber ≫
                        NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (α.naturality (f ≫ g).base.op.toLoc))) c.fiber :
                    { base := a.base,
                          fiber := obj (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ })) a.fiber :
                          ∫ᶜ G }.Hom
                      { base := c.base,
                        fiber := obj (Cat.Hom.toFunctor (α.app { as := op c.base : LocallyDiscrete 𝒮ᵒᵖ })) c.fiber :
                        ∫ᶜ G } }.base.op.toLoc))
        { base := c.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := op c.base : LocallyDiscrete 𝒮ᵒᵖ })) c.fiber :
            ∫ᶜ G }.fiber)
    ({ base := (f ≫ g).base,
          fiber :=
            Functor.map (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ })) (f ≫ g).fiber ≫
              NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (α.naturality (f ≫ g).base.op.toLoc))) c.fiber }.fiber :
      { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ })) a.fiber :
            ∫ᶜ G }.fiber ⟶
        obj
          (Cat.Hom.toFunctor
            (G.map
              { base := (f ≫ g).base,
                      fiber :=
                        Functor.map (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ }))
                            (f ≫ g).fiber ≫
                          NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (α.naturality (f ≫ g).base.op.toLoc))) c.fiber :
                      { base := a.base,
                            fiber := obj (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ })) a.fiber :
                            ∫ᶜ G }.Hom
                        { base := c.base,
                          fiber := obj (Cat.Hom.toFunctor (α.app { as := op c.base : LocallyDiscrete 𝒮ᵒᵖ })) c.fiber :
                          ∫ᶜ G } }.base.op.toLoc))
          { base := c.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := op c.base : LocallyDiscrete 𝒮ᵒᵖ })) c.fiber :
              ∫ᶜ G }.fiber)
    (CategoryStruct.comp (Y :=
        obj
          (Cat.Hom.toFunctor
            (G.map
              (Quiver.Hom.toLoc
                (Quiver.Hom.op
                  (Hom.base
                    ({ base := f.base,
                        fiber :=
                          Functor.map (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ })) f.fiber ≫
                            NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (α.naturality f.base.op.toLoc))) b.fiber :
                        { base := a.base,
                              fiber :=
                                obj (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ })) a.fiber :
                              ∫ᶜ G }.Hom
                          { base := b.base,
                            fiber := obj (Cat.Hom.toFunctor (α.app { as := op b.base : LocallyDiscrete 𝒮ᵒᵖ })) b.fiber :
                            ∫ᶜ G } } ≫
                      { base := g.base,
                        fiber :=
                          Functor.map (Cat.Hom.toFunctor (α.app { as := op b.base : LocallyDiscrete 𝒮ᵒᵖ })) g.fiber ≫
                            NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (α.naturality g.base.op.toLoc))) c.fiber :
                        { base := b.base,
                              fiber :=
                                obj (Cat.Hom.toFunctor (α.app { as := op b.base : LocallyDiscrete 𝒮ᵒᵖ })) b.fiber :
                              ∫ᶜ G }.Hom
                          { base := c.base,
                            fiber := obj (Cat.Hom.toFunctor (α.app { as := op c.base : LocallyDiscrete 𝒮ᵒᵖ })) c.fiber :
                            ∫ᶜ G } }))))))
          { base := c.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := op c.base : LocallyDiscrete 𝒮ᵒᵖ })) c.fiber :
              ∫ᶜ G }.fiber)
        (Hom.fiber
          ({ base := f.base,
              fiber :=
                Functor.map (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ })) f.fiber ≫
                  NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (α.naturality f.base.op.toLoc))) b.fiber :
              { base := a.base,
                    fiber := obj (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ })) a.fiber :
                    ∫ᶜ G }.Hom
                { base := b.base,
                  fiber := obj (Cat.Hom.toFunctor (α.app { as := op b.base : LocallyDiscrete 𝒮ᵒᵖ })) b.fiber :
                  ∫ᶜ G } } ≫
            { base := g.base,
              fiber :=
                Functor.map (Cat.Hom.toFunctor (α.app { as := op b.base : LocallyDiscrete 𝒮ᵒᵖ })) g.fiber ≫
                  NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (α.naturality g.base.op.toLoc))) c.fiber }))
        (eqToHom ⋯) :
      { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ })) a.fiber :
            ∫ᶜ G }.fiber ⟶
        obj
          (Cat.Hom.toFunctor
            (G.map
              { base := (f ≫ g).base,
                      fiber :=
                        Functor.map (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ }))
                            (f ≫ g).fiber ≫
                          NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (α.naturality (f ≫ g).base.op.toLoc))) c.fiber :
                      { base := a.base,
                            fiber := obj (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ })) a.fiber :
                            ∫ᶜ G }.Hom
                        { base := c.base,
                          fiber := obj (Cat.Hom.toFunctor (α.app { as := op c.base : LocallyDiscrete 𝒮ᵒᵖ })) c.fiber :
                          ∫ᶜ G } }.base.op.toLoc))
          { base := c.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := op c.base : LocallyDiscrete 𝒮ᵒᵖ })) c.fiber :
              ∫ᶜ G }.fiber)

Tactic:
simp only [categoryStruct_comp_base, op_comp, Quiver.Hom.comp_toLoc,
        categoryStruct_comp_fiber, Cat.Hom.comp_toFunctor, map_comp, naturality_comp_hom_app, assoc,
        eqToHom_refl, comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.op_comp, CategoryTheory.Cat.Hom.comp_toFunctor, Quiver.Hom.comp_toLoc, CategoryTheory.Pseudofunctor.CoGrothendieck.categoryStruct_comp_base, CategoryTheory.eqToHom_refl, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_comp, CategoryTheory.Pseudofunctor.CoGrothendieck.categoryStruct_comp_fiber, CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_hom_app