-- 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 :=
          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 =
    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 := (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 := 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 }
have hfg₂ : 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 sorry) :
    { 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: ext