-- Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck
Goal:
𝒮 : Type u_1
inst : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
X Y : (↑(F.obj { as := op S : LocallyDiscrete 𝒮ᵒᵖ }) : Type u_3)
f : (Fiber.inducedFunctor ⋯).obj X ⟶ (Fiber.inducedFunctor ⋯).obj Y
hf :
  Eq (α :=
    (obj fiberInclusion ((Fiber.inducedFunctor ⋯).obj X)).base ⟶
      (obj fiberInclusion ((Fiber.inducedFunctor ⋯).obj Y)).base)
    (Hom.base (Functor.map fiberInclusion f)) (𝟙 S)
h :
  Eq (α :=
    (obj fiberInclusion ((Fiber.inducedFunctor ⋯).obj X)).base ⟶
      (obj fiberInclusion ((Fiber.inducedFunctor ⋯).obj Y)).base)
    (Hom.base
      (Functor.map fiberInclusion
        ((Fiber.inducedFunctor ⋯).map
          (CategoryStruct.comp (Y :=
            obj (Cat.Hom.toFunctor (F.map (Quiver.Hom.toLoc (Quiver.Hom.op (Hom.base (Functor.map fiberInclusion f))))))
              (obj fiberInclusion ((Fiber.inducedFunctor ⋯).obj Y)).fiber)
            (Hom.fiber (Functor.map fiberInclusion f))
            (eqToHom ⋯ ≫
              NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (F.mapId { as := op S : LocallyDiscrete 𝒮ᵒᵖ }))) Y)))))
    (Hom.base (Functor.map fiberInclusion f))
h₁ :
  Eq (α :=
    (obj fiberInclusion ((Fiber.inducedFunctor ⋯).obj X)).fiber ⟶
      obj
        (Cat.Hom.toFunctor
          (F.map
            (Quiver.Hom.toLoc
              (Quiver.Hom.op
                (Hom.base
                  (Functor.map fiberInclusion
                    ((Fiber.inducedFunctor ⋯).map
                      (CategoryStruct.comp (Y :=
                        obj
                          (Cat.Hom.toFunctor
                            (F.map (Quiver.Hom.toLoc (Quiver.Hom.op (Hom.base (Functor.map fiberInclusion f))))))
                          (obj fiberInclusion ((Fiber.inducedFunctor ⋯).obj Y)).fiber)
                        (Hom.fiber (Functor.map fiberInclusion f))
                        (eqToHom ⋯ ≫
                          NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (F.mapId { as := op S : LocallyDiscrete 𝒮ᵒᵖ })))
                            Y)))))))))
        (obj fiberInclusion ((Fiber.inducedFunctor ⋯).obj Y)).fiber)
    (Hom.fiber
      (Functor.map fiberInclusion
        ((Fiber.inducedFunctor ⋯).map
          (CategoryStruct.comp (Y :=
            obj (Cat.Hom.toFunctor (F.map (Quiver.Hom.toLoc (Quiver.Hom.op (Hom.base (Functor.map fiberInclusion f))))))
              (obj fiberInclusion ((Fiber.inducedFunctor ⋯).obj Y)).fiber)
            (Hom.fiber (Functor.map fiberInclusion f))
            (eqToHom ⋯ ≫
              NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (F.mapId { as := op S : LocallyDiscrete 𝒮ᵒᵖ }))) Y)))))
    (CategoryStruct.comp (Y :=
      obj (Cat.Hom.toFunctor (F.map (Quiver.Hom.toLoc (Quiver.Hom.op (Hom.base (Functor.map fiberInclusion f))))))
        (obj fiberInclusion ((Fiber.inducedFunctor ⋯).obj Y)).fiber)
      (Hom.fiber (Functor.map fiberInclusion f)) (eqToHom ⋯))
⊢ (Fiber.inducedFunctor ⋯).map
      (CategoryStruct.comp (Y :=
        obj (Cat.Hom.toFunctor (F.map (Quiver.Hom.toLoc (Quiver.Hom.op (Hom.base (Functor.map fiberInclusion f))))))
          (obj fiberInclusion ((Fiber.inducedFunctor ⋯).obj Y)).fiber)
        (Hom.fiber (Functor.map fiberInclusion f))
        (eqToHom ⋯ ≫ NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (F.mapId { as := op S : LocallyDiscrete 𝒮ᵒᵖ }))) Y)) =
    f

Tactic:
ext