-- Module: Mathlib.CategoryTheory.Bicategory.Grothendieck
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
α : F ⟶ G
a : ∫ᶜ F
⊢ 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 := Hom.base (𝟙 a),
                    fiber :=
                      Functor.map (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ }))
                          (Hom.fiber (𝟙 a)) ≫
                        NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (α.naturality (Hom.base (𝟙 a)).op.toLoc))) a.fiber :
                    { base := a.base,
                          fiber := obj (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ })) a.fiber :
                          ∫ᶜ G }.Hom
                      { base := a.base,
                        fiber := obj (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ })) a.fiber :
                        ∫ᶜ G } }.base.op.toLoc))
        { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ })) a.fiber :
            ∫ᶜ G }.fiber)
    ({ base := Hom.base (𝟙 a),
          fiber :=
            Functor.map (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ })) (Hom.fiber (𝟙 a)) ≫
              NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (α.naturality (Hom.base (𝟙 a)).op.toLoc))) a.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 := Hom.base (𝟙 a),
                      fiber :=
                        Functor.map (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ }))
                            (Hom.fiber (𝟙 a)) ≫
                          NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (α.naturality (Hom.base (𝟙 a)).op.toLoc)))
                            a.fiber :
                      { base := a.base,
                            fiber := obj (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ })) a.fiber :
                            ∫ᶜ G }.Hom
                        { base := a.base,
                          fiber := obj (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ })) a.fiber :
                          ∫ᶜ G } }.base.op.toLoc))
          { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ })) a.fiber :
              ∫ᶜ G }.fiber)
    (Hom.fiber
          (𝟙
            { base := a.base,
              fiber := obj (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ })) a.fiber : ∫ᶜ G }) ≫
        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 := Hom.base (𝟙 a),
                      fiber :=
                        Functor.map (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ }))
                            (Hom.fiber (𝟙 a)) ≫
                          NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (α.naturality (Hom.base (𝟙 a)).op.toLoc)))
                            a.fiber :
                      { base := a.base,
                            fiber := obj (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ })) a.fiber :
                            ∫ᶜ G }.Hom
                        { base := a.base,
                          fiber := obj (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ })) a.fiber :
                          ∫ᶜ G } }.base.op.toLoc))
          { base := a.base, fiber := obj (Cat.Hom.toFunctor (α.app { as := op a.base : LocallyDiscrete 𝒮ᵒᵖ })) a.fiber :
              ∫ᶜ G }.fiber)

Tactic:
simp [Cat.Hom.comp_toFunctor, naturality_id_hom_app, Cat.Hom.id_toFunctor, ← Category.assoc,
        ← Functor.map_comp, ← Cat.Hom₂.comp_app]

Premises used: CategoryTheory.Cat.Hom₂.comp_app, CategoryTheory.Category.assoc, CategoryTheory.Cat.Hom.comp_toFunctor, CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_hom_app, CategoryTheory.Functor.map_comp, CategoryTheory.Cat.Hom.id_toFunctor