-- Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck
Goal:
𝒮 : Type u_1
inst : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
a b c : (↑(F.obj { as := op S : LocallyDiscrete 𝒮ᵒᵖ }) : Type u_2)
φ : a ⟶ b
ψ : b ⟶ c
hfg₁ :
  Eq.{v_1 + 1} (α := { base := S, fiber := a : ∫ᶜ F }.base ⟶ { base := S, fiber := c : ∫ᶜ F }.base)
    (Hom.base
      { base := 𝟙 S,
        fiber :=
          (φ ≫ ψ) ≫ NatTrans.app (Cat.Hom₂.toNatTrans (Iso.inv (F.mapId { as := op S : LocallyDiscrete 𝒮ᵒᵖ }))) c })
    (Hom.base
      (CategoryStruct.comp (Y := { base := S, fiber := b })
        { base := 𝟙 S,
          fiber := φ ≫ NatTrans.app (Cat.Hom₂.toNatTrans (Iso.inv (F.mapId { as := op S : LocallyDiscrete 𝒮ᵒᵖ }))) b }
        { base := 𝟙 S,
          fiber := ψ ≫ NatTrans.app (Cat.Hom₂.toNatTrans (Iso.inv (F.mapId { as := op S : LocallyDiscrete 𝒮ᵒᵖ }))) c }))
hfg₂ :
  Eq.{u_3 + 1} (α :=
    { base := S, fiber := a : ∫ᶜ F }.fiber ⟶
      obj
        (Cat.Hom.toFunctor
          (F.map
            (Quiver.Hom.toLoc
              (Quiver.Hom.op
                (Hom.base
                  { base := 𝟙 S,
                    fiber :=
                      (φ ≫ ψ) ≫
                        NatTrans.app (Cat.Hom₂.toNatTrans (Iso.inv (F.mapId { as := op S : LocallyDiscrete 𝒮ᵒᵖ }))) c :
                    { base := S, fiber := a : ∫ᶜ F }.Hom { base := S, fiber := c : ∫ᶜ F } })))))
        { base := S, fiber := c : ∫ᶜ F }.fiber)
    (Hom.fiber
      { base := 𝟙 S,
        fiber :=
          (φ ≫ ψ) ≫ NatTrans.app (Cat.Hom₂.toNatTrans (Iso.inv (F.mapId { as := op S : LocallyDiscrete 𝒮ᵒᵖ }))) c })
    (CategoryStruct.comp (Y :=
      obj
        (Cat.Hom.toFunctor
          (F.map
            (Quiver.Hom.toLoc
              (Quiver.Hom.op
                (Hom.base
                  (CategoryStruct.comp (Y := { base := S, fiber := b : ∫ᶜ F })
                    { base := 𝟙 S,
                      fiber :=
                        φ ≫
                          NatTrans.app (Cat.Hom₂.toNatTrans (Iso.inv (F.mapId { as := op S : LocallyDiscrete 𝒮ᵒᵖ })))
                            b :
                      { base := S, fiber := a : ∫ᶜ F }.Hom { base := S, fiber := b : ∫ᶜ F } }
                    { base := 𝟙 S,
                      fiber :=
                        ψ ≫
                          NatTrans.app (Cat.Hom₂.toNatTrans (Iso.inv (F.mapId { as := op S : LocallyDiscrete 𝒮ᵒᵖ })))
                            c :
                      { base := S, fiber := b : ∫ᶜ F }.Hom { base := S, fiber := c : ∫ᶜ F } }))))))
        { base := S, fiber := c : ∫ᶜ F }.fiber)
      (Hom.fiber
        (CategoryStruct.comp (Y := { base := S, fiber := b })
          { base := 𝟙 S,
            fiber := φ ≫ NatTrans.app (Cat.Hom₂.toNatTrans (Iso.inv (F.mapId { as := op S : LocallyDiscrete 𝒮ᵒᵖ }))) b }
          { base := 𝟙 S,
            fiber :=
              ψ ≫ NatTrans.app (Cat.Hom₂.toNatTrans (Iso.inv (F.mapId { as := op S : LocallyDiscrete 𝒮ᵒᵖ }))) c }))
      (eqToHom ⋯))
⊢ Eq (α := { base := S, fiber := a : ∫ᶜ F } ⟶ { base := S, fiber := c })
    { base := 𝟙 S,
      fiber := (φ ≫ ψ) ≫ NatTrans.app (Cat.Hom₂.toNatTrans (Iso.inv (F.mapId { as := op S : LocallyDiscrete 𝒮ᵒᵖ }))) c }
    (CategoryStruct.comp (Y := { base := S, fiber := b })
      { base := 𝟙 S,
        fiber := φ ≫ NatTrans.app (Cat.Hom₂.toNatTrans (Iso.inv (F.mapId { as := op S : LocallyDiscrete 𝒮ᵒᵖ }))) b }
      { base := 𝟙 S,
        fiber := ψ ≫ NatTrans.app (Cat.Hom₂.toNatTrans (Iso.inv (F.mapId { as := op S : LocallyDiscrete 𝒮ᵒᵖ }))) c })

Tactic:
ext