-- 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) ≫
            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)
⊢ 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)

Tactic:
slice_lhs 2 4 => simp [← Cat.Hom.toNatIso_inv, Cat.Hom.comp_toFunctor,
        ← Cat.Hom.toNatIso_hom, ← map_comp, Iso.inv_hom_id_app, comp_obj, map_id, comp_id]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Cat.Hom.toNatIso_hom, CategoryTheory.Cat.Hom.comp_toFunctor, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, CategoryTheory.Iso.inv_hom_id_app, CategoryTheory.Cat.Hom.toNatIso_inv