-- 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
U V : Cᵒᵖ
f : U ⟶ V
⊢ (Subfunctor.toFunctor (F := Functor.obj shrinkYoneda.{v₁, v₁, u₁} X) (shrinkFunctor.{v₁, v₁, u₁} S)).map f ≫
      Iso.hom
        ((fun (Y : Cᵒᵖ) ↦
            (Equiv.subtypeEquiv (p :=
                Membership.mem (γ := Set (Functor.obj (Functor.obj shrinkYoneda.{v₁, v₁, u₁} X) Y))
                  (Subfunctor.obj (shrinkFunctor.{v₁, v₁, u₁} S) Y))
                (q := S.arrows) shrinkYonedaObjObjEquiv ⋯).toIso)
          V) =
    Iso.hom
        ((fun (Y : Cᵒᵖ) ↦
            (Equiv.subtypeEquiv (p :=
                Membership.mem (γ := Set (Functor.obj (Functor.obj shrinkYoneda.{v₁, v₁, u₁} X) Y))
                  (Subfunctor.obj (shrinkFunctor.{v₁, v₁, u₁} S) Y))
                (q := S.arrows) shrinkYonedaObjObjEquiv ⋯).toIso)
          U) ≫
      S.functor.map f
have dsimp : Eq.{v₁ + 1} (α :=
  { 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) } ⟶
    { g : Opposite.unop V ⟶ X // S.arrows g })
  (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))
        sorry)
    (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))
              sorry,
          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))
              sorry,
          left_inv := sorry, right_inv := sorry })))
  (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))
              sorry,
          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))
              sorry,
          left_inv := sorry, right_inv := sorry }))
    (↾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)) sorry))
Tactic: dsimp [Equiv.subtypeEquiv]