-- 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
⊢ (Subfunctor.toFunctor (F := Functor.obj shrinkYoneda.{w, v₁, u₁} X) (shrinkFunctor.{w, v₁, u₁} S) ⋙
            CategoryTheory.uliftFunctor.{w', w}).map
        f ≫
      Iso.hom
        ((fun (X_1 : Cᵒᵖ) ↦
            (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) X_1))
                      (Subfunctor.obj (shrinkFunctor.{w, v₁, u₁} S) X_1))
                    (q :=
                    Membership.mem (γ := Set (Functor.obj (Functor.obj shrinkYoneda.{max w' w, v₁, u₁} X) X_1))
                      (Subfunctor.obj (shrinkFunctor.{max w' w, v₁, u₁} S) X_1))
                    (Equiv.trans shrinkYonedaObjObjEquiv (Equiv.symm shrinkYonedaObjObjEquiv)) ⋯)) :
              (Subfunctor.toFunctor (F := Functor.obj shrinkYoneda.{w, v₁, u₁} X) (shrinkFunctor.{w, v₁, u₁} S) ⋙
                      CategoryTheory.uliftFunctor.{w', w}).obj
                  X_1 ≅
                (Subfunctor.toFunctor (F := Functor.obj shrinkYoneda.{max w' w, v₁, u₁} X)
                      (shrinkFunctor.{max w' w, v₁, u₁} S)).obj
                  X_1))
          V) =
    Iso.hom
        ((fun (X_1 : Cᵒᵖ) ↦
            (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) X_1))
                      (Subfunctor.obj (shrinkFunctor.{w, v₁, u₁} S) X_1))
                    (q :=
                    Membership.mem (γ := Set (Functor.obj (Functor.obj shrinkYoneda.{max w' w, v₁, u₁} X) X_1))
                      (Subfunctor.obj (shrinkFunctor.{max w' w, v₁, u₁} S) X_1))
                    (Equiv.trans shrinkYonedaObjObjEquiv (Equiv.symm shrinkYonedaObjObjEquiv)) ⋯)) :
              (Subfunctor.toFunctor (F := Functor.obj shrinkYoneda.{w, v₁, u₁} X) (shrinkFunctor.{w, v₁, u₁} S) ⋙
                      CategoryTheory.uliftFunctor.{w', w}).obj
                  X_1 ≅
                (Subfunctor.toFunctor (F := Functor.obj shrinkYoneda.{max w' w, v₁, u₁} X)
                      (shrinkFunctor.{max w' w, v₁, u₁} S)).obj
                  X_1))
          U) ≫
      (Subfunctor.toFunctor (F := Functor.obj shrinkYoneda.{max w' w, v₁, u₁} X)
            (shrinkFunctor.{max w' w, v₁, u₁} S)).map
        f
have dsimp : Eq (α :=
  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) } ⟶
    { 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) })
  (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))
            sorry })
    (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)) sorry)))))
  (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)) sorry))))
    (↾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))
        sorry))
Tactic: dsimp