-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
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) }
⊢ Eq (α := Functor.obj (Functor.obj shrinkYoneda.{max w' w, v₁, u₁} X) V)
    (↑(TypeCat.Fun.toFun
          (hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y :=
              ULift.{w', w}
                { x : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) V //
                  S.arrows (Y := Opposite.unop V)
                    ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj V) → Opposite.unop V ⟶ X)
                      x) })
              (↾fun
                  (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) }) ↦
                {
                  down :=
                    Subtype.mk (p :=
                      fun (x : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) V) ↦
                      S.arrows (Y := Opposite.unop V)
                        ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj V) → Opposite.unop V ⟶ X)
                          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))
                      ⋯ :
                  ULift.{w', w}
                    { x : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) V //
                      S.arrows (Y := Opposite.unop V)
                        ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj V) → Opposite.unop V ⟶ X)
                          x) } })
              (Iso.hom
                (Equiv.toIso
                  (Equiv.trans Equiv.ulift
                    (Equiv.subtypeEquiv (p :=
                      Membership.mem (γ :=
                        Set (Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) V))
                        {f : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) V |
                          S.arrows (Y := Opposite.unop V)
                            ((shrinkYonedaObjObjEquiv :
                                (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj V) → Opposite.unop V ⟶ X)
                              f)})
                      (q :=
                      Membership.mem (γ := Set (Functor.obj (Functor.obj shrinkYoneda.{max w' w, v₁, u₁} X) V))
                        {f : Functor.obj (Functor.obj shrinkYoneda.{max w w', v₁, u₁} X) V |
                          S.arrows (Y := Opposite.unop V)
                            ((shrinkYonedaObjObjEquiv :
                                (a : (shrinkYoneda.{max w w', v₁, u₁}.obj X).obj V) → Opposite.unop V ⟶ X)
                              f)})
                      (Equiv.trans shrinkYonedaObjObjEquiv (Equiv.symm shrinkYonedaObjObjEquiv)) ⋯))))))
          x) :
      (shrinkYoneda.{max w' w, v₁, u₁}.obj X).obj V)
    (↑(TypeCat.Fun.toFun
          (hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y :=
              { x : Functor.obj (Functor.obj shrinkYoneda.{max w' w, v₁, u₁} X) U //
                S.arrows (Y := Opposite.unop U)
                  ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{max w w', v₁, u₁}.obj X).obj U) → Opposite.unop U ⟶ X)
                    x) })
              (Iso.hom
                (Equiv.toIso
                  (Equiv.trans Equiv.ulift
                    (Equiv.subtypeEquiv (p :=
                      Membership.mem (γ :=
                        Set (Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) U))
                        {f : 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)
                              f)})
                      (q :=
                      Membership.mem (γ := Set (Functor.obj (Functor.obj shrinkYoneda.{max w' w, v₁, u₁} X) U))
                        {f : Functor.obj (Functor.obj shrinkYoneda.{max w w', v₁, u₁} X) U |
                          S.arrows (Y := Opposite.unop U)
                            ((shrinkYonedaObjObjEquiv :
                                (a : (shrinkYoneda.{max w w', v₁, u₁}.obj X).obj U) → Opposite.unop U ⟶ X)
                              f)})
                      (Equiv.trans shrinkYonedaObjObjEquiv (Equiv.symm shrinkYonedaObjObjEquiv)) ⋯))))
              (↾fun
                  (x :
                    { x : Functor.obj (Functor.obj shrinkYoneda.{max w' w, v₁, u₁} X) U //
                      S.arrows (Y := Opposite.unop U)
                        ((shrinkYonedaObjObjEquiv :
                            (a : (shrinkYoneda.{max w w', v₁, u₁}.obj X).obj U) → Opposite.unop U ⟶ X)
                          x) }) ↦
                Subtype.mk (p := fun (x : Functor.obj (Functor.obj shrinkYoneda.{max w' w, v₁, u₁} X) V) ↦
                  S.arrows (Y := Opposite.unop V)
                    ((shrinkYonedaObjObjEquiv :
                        (a : (shrinkYoneda.{max w w', v₁, u₁}.obj X).obj V) → Opposite.unop V ⟶ X)
                      x))
                  ((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)
                    (↑x : (shrinkYoneda.{max w' w, v₁, u₁}.obj X).obj U))
                  ⋯)))
          x) :
      (shrinkYoneda.{max w' w, v₁, u₁}.obj X).obj V)
have h : 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: dsimp [Equiv.subtypeEquiv]