-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Grothendieck (goal)
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 }))
⊢ 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 })
have 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 sorry))
Tactic: ext