-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
f_1 : Y ⟶ X
S R : Sieve.{v₁, u₁} X
U V : Cᵒᵖ
f : U ⟶ V
x :
  { x : Functor.obj (Functor.obj shrinkYoneda.{v₁, v₁, u₁} X) U //
    S.arrows (Y := Opposite.unop U)
      ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{v₁, v₁, u₁}.obj X).obj U) → Opposite.unop U ⟶ X) x) }
⊢ Eq (α := Opposite.unop V ⟶ X)
    (↑(TypeCat.Fun.toFun
          (hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y :=
              { x : Functor.obj (Functor.obj shrinkYoneda.{v₁, v₁, u₁} X) V //
                S.arrows (Y := Opposite.unop V)
                  ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{v₁, v₁, u₁}.obj X).obj V) → Opposite.unop V ⟶ X) x) })
              (↾fun
                  (x :
                    { x : Functor.obj (Functor.obj shrinkYoneda.{v₁, v₁, u₁} X) U //
                      S.arrows (Y := Opposite.unop U)
                        ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{v₁, v₁, u₁}.obj X).obj U) → Opposite.unop U ⟶ X)
                          x) }) ↦
                Subtype.mk (p := fun (x : Functor.obj (Functor.obj shrinkYoneda.{v₁, v₁, u₁} X) V) ↦
                  S.arrows (Y := Opposite.unop V)
                    ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{v₁, v₁, u₁}.obj X).obj V) → Opposite.unop V ⟶ X) x))
                  ((hom (FC := TypeCat.Fun) (Functor.map (Functor.obj shrinkYoneda.{v₁, v₁, u₁} X) f) :
                      (a : (shrinkYoneda.{v₁, v₁, u₁}.obj X).obj U) → (shrinkYoneda.{v₁, v₁, u₁}.obj X).obj V)
                    (↑x : (shrinkYoneda.{v₁, v₁, u₁}.obj X).obj U))
                  ⋯)
              (Iso.hom
                (Equiv.toIso
                  {
                    toFun :=
                      fun
                        (a :
                          { a : Functor.obj (Functor.obj shrinkYoneda.{v₁, v₁, u₁} X) V //
                            S.arrows (Y := Opposite.unop V)
                              ((shrinkYonedaObjObjEquiv :
                                  (a : (shrinkYoneda.{v₁, v₁, u₁}.obj X).obj V) → Opposite.unop V ⟶ X)
                                a) }) ↦
                      Subtype.mk (p := fun (b : Opposite.unop V ⟶ X) ↦ S.arrows b)
                        ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{v₁, v₁, u₁}.obj X).obj V) → Opposite.unop V ⟶ X)
                          (↑a : (shrinkYoneda.{v₁, v₁, u₁}.obj X).obj V))
                        ⋯,
                    invFun := fun (b : { b : Opposite.unop V ⟶ X // S.arrows b }) ↦
                      Subtype.mk (p := fun (a : Functor.obj (Functor.obj shrinkYoneda.{v₁, v₁, u₁} X) V) ↦
                        S.arrows (Y := Opposite.unop V)
                          ((shrinkYonedaObjObjEquiv :
                              (a : (shrinkYoneda.{v₁, v₁, u₁}.obj X).obj V) → Opposite.unop V ⟶ X)
                            a))
                        ((Equiv.symm shrinkYonedaObjObjEquiv :
                            (a : Opposite.unop V ⟶ X) → (shrinkYoneda.{v₁, v₁, u₁}.obj X).obj V)
                          (↑b : Opposite.unop V ⟶ X))
                        ⋯,
                    left_inv := ⋯, right_inv := ⋯ :
                    { a : Functor.obj (Functor.obj shrinkYoneda.{v₁, v₁, u₁} X) V //
                        S.arrows (Y := Opposite.unop V)
                          ((shrinkYonedaObjObjEquiv :
                              (a : (shrinkYoneda.{v₁, v₁, u₁}.obj X).obj V) → Opposite.unop V ⟶ X)
                            a) } ≃
                      { b : Opposite.unop V ⟶ X // S.arrows b } }))))
          x) :
      Opposite.unop V ⟶ X)
    (↑(TypeCat.Fun.toFun
          (hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := { g : Opposite.unop U ⟶ X // S.arrows g })
              (Iso.hom
                (Equiv.toIso
                  {
                    toFun :=
                      fun
                        (a :
                          { a : Functor.obj (Functor.obj shrinkYoneda.{v₁, v₁, u₁} X) U //
                            S.arrows (Y := Opposite.unop U)
                              ((shrinkYonedaObjObjEquiv :
                                  (a : (shrinkYoneda.{v₁, v₁, u₁}.obj X).obj U) → Opposite.unop U ⟶ X)
                                a) }) ↦
                      Subtype.mk (p := fun (b : Opposite.unop U ⟶ X) ↦ S.arrows b)
                        ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{v₁, v₁, u₁}.obj X).obj U) → Opposite.unop U ⟶ X)
                          (↑a : (shrinkYoneda.{v₁, v₁, u₁}.obj X).obj U))
                        ⋯,
                    invFun := fun (b : { b : Opposite.unop U ⟶ X // S.arrows b }) ↦
                      Subtype.mk (p := fun (a : Functor.obj (Functor.obj shrinkYoneda.{v₁, v₁, u₁} X) U) ↦
                        S.arrows (Y := Opposite.unop U)
                          ((shrinkYonedaObjObjEquiv :
                              (a : (shrinkYoneda.{v₁, v₁, u₁}.obj X).obj U) → Opposite.unop U ⟶ X)
                            a))
                        ((Equiv.symm shrinkYonedaObjObjEquiv :
                            (a : Opposite.unop U ⟶ X) → (shrinkYoneda.{v₁, v₁, u₁}.obj X).obj U)
                          (↑b : Opposite.unop U ⟶ X))
                        ⋯,
                    left_inv := ⋯, right_inv := ⋯ :
                    { a : Functor.obj (Functor.obj shrinkYoneda.{v₁, v₁, u₁} X) U //
                        S.arrows (Y := Opposite.unop U)
                          ((shrinkYonedaObjObjEquiv :
                              (a : (shrinkYoneda.{v₁, v₁, u₁}.obj X).obj U) → Opposite.unop U ⟶ X)
                            a) } ≃
                      { b : Opposite.unop U ⟶ X // S.arrows b } }))
              (↾fun (g : { g : Opposite.unop U ⟶ X // S.arrows g }) ↦
                Subtype.mk (p := fun (g : Opposite.unop V ⟶ X) ↦ S.arrows g) (f.unop ≫ (↑g : Opposite.unop U ⟶ X)) ⋯)))
          x) :
      Opposite.unop V ⟶ X)

Tactic:
simp [shrinkYonedaObjObjEquiv_obj_map]

Premises used: CategoryTheory.shrinkYonedaObjObjEquiv_obj_map