-- 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
h :
  ∀
    (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)
⊢ 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))
              ⋯ })
      (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)) ⋯)))))
    (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))
          ⋯))

Tactic:
ext