-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Grothendieck (goal)
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))
⊢ (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
have h₁ : Eq (α :=
  (obj fiberInclusion ((Fiber.inducedFunctor sorry).obj X)).fiber ⟶
    obj
      (Cat.Hom.toFunctor
        (F.map
          (Quiver.Hom.toLoc
            (Quiver.Hom.op
              (Hom.base
                (Functor.map fiberInclusion
                  ((Fiber.inducedFunctor sorry).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 sorry).obj Y)).fiber)
                      (Hom.fiber (Functor.map fiberInclusion f))
                      (eqToHom sorry ≫
                        NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (F.mapId { as := op S : LocallyDiscrete 𝒮ᵒᵖ })))
                          Y)))))))))
      (obj fiberInclusion ((Fiber.inducedFunctor sorry).obj Y)).fiber)
  (Hom.fiber
    (Functor.map fiberInclusion
      ((Fiber.inducedFunctor sorry).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 sorry).obj Y)).fiber)
          (Hom.fiber (Functor.map fiberInclusion f))
          (eqToHom sorry ≫
            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 sorry).obj Y)).fiber)
    (Hom.fiber (Functor.map fiberInclusion f)) (eqToHom sorry))
Tactic: ext