-- 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
inst_2 : LocallySmall.{w, v₁, u₁} C
inst_3 : LocallySmall.{max w' w, v₁, u₁} C
U V : Cᵒᵖ
f : U ⟶ V
x :
  ULift.{w', w}
    { x : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) U //
      S.arrows (Y := Opposite.unop U)
        ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj U) → Opposite.unop U ⟶ X) x) }
h :
  Eq (α := Functor.obj (Functor.obj shrinkYoneda.{max w' w, v₁, u₁} X) V)
    ((hom (FC := TypeCat.Fun) (Functor.map (Functor.obj shrinkYoneda.{max w w', v₁, u₁} X) f.unop.op) :
          (a :
              (fun (X : Type (max w w')) ↦ X)
                ((shrinkYoneda.{max w w', v₁, u₁}.obj X).obj (Opposite.op (Opposite.unop U)))) →
            (fun (X : Type (max w w')) ↦ X)
              ((shrinkYoneda.{max w w', v₁, u₁}.obj X).obj (Opposite.op (Opposite.unop V))))
        ((Equiv.symm shrinkYonedaObjObjEquiv :
            (a : Opposite.unop (Opposite.op (Opposite.unop U)) ⟶ X) →
              (shrinkYoneda.{max w w', v₁, u₁}.obj X).obj (Opposite.op (Opposite.unop U)))
          ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj U) → Opposite.unop U ⟶ X)
            (↑x.down : (shrinkYoneda.{w, v₁, u₁}.obj X).obj U))) :
      (fun (X : Type (max w w')) ↦ X)
        (Functor.obj (Functor.obj shrinkYoneda.{max w w', v₁, u₁} X) (Opposite.op (Opposite.unop V))))
    ((hom (FC := TypeCat.Fun) (Functor.map (Functor.obj shrinkYoneda.{max w' w, v₁, u₁} X) f) :
          (a : (shrinkYoneda.{max w' w, v₁, u₁}.obj X).obj U) → (shrinkYoneda.{max w' w, v₁, u₁}.obj X).obj V)
        ((Equiv.symm shrinkYonedaObjObjEquiv :
            (a : Opposite.unop U ⟶ X) → (shrinkYoneda.{max w' w, v₁, u₁}.obj X).obj U)
          ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj U) → Opposite.unop U ⟶ X)
            (↑x.down : (shrinkYoneda.{w, v₁, u₁}.obj X).obj U))) :
      Functor.obj (Functor.obj shrinkYoneda.{max w' w, v₁, u₁} X) V)
⊢ Eq (α := Functor.obj (Functor.obj shrinkYoneda.{max w' w, v₁, u₁} X) V)
    ((Equiv.symm shrinkYonedaObjObjEquiv : (a : Opposite.unop V ⟶ X) → (shrinkYoneda.{max w' w, v₁, u₁}.obj X).obj V)
        ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj V) → Opposite.unop V ⟶ X)
          ((hom (FC := TypeCat.Fun) (Functor.map (Functor.obj shrinkYoneda.{w, v₁, u₁} X) f) :
              (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj U) → (shrinkYoneda.{w, v₁, u₁}.obj X).obj V)
            (↑x.down : (shrinkYoneda.{w, v₁, u₁}.obj X).obj U))) :
      Functor.obj (Functor.obj shrinkYoneda.{max w' w, v₁, u₁} X) V)
    ((hom (FC := TypeCat.Fun) (Functor.map (Functor.obj shrinkYoneda.{max w' w, v₁, u₁} X) f) :
          (a : (shrinkYoneda.{max w' w, v₁, u₁}.obj X).obj U) → (shrinkYoneda.{max w' w, v₁, u₁}.obj X).obj V)
        ((Equiv.symm shrinkYonedaObjObjEquiv :
            (a : Opposite.unop U ⟶ X) → (shrinkYoneda.{max w' w, v₁, u₁}.obj X).obj U)
          ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj U) → Opposite.unop U ⟶ X)
            (↑x.down : (shrinkYoneda.{w, v₁, u₁}.obj X).obj U))) :
      Functor.obj (Functor.obj shrinkYoneda.{max w' w, v₁, u₁} X) V)

Tactic:
rw [shrinkYonedaObjObjEquiv_obj_map, shrinkYonedaObjObjEquiv_symm_comp]

Premises used: CategoryTheory.shrinkYonedaObjObjEquiv_symm_comp, CategoryTheory.shrinkYonedaObjObjEquiv_obj_map