-- 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
U V : Cᵒᵖ
f : U ⟶ V
h :
  ∀
    (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) }),
    Eq (α := Opposite.unop V ⟶ X)
      (↑(TypeCat.Fun.toFun
            (hom (FC := TypeCat.Fun)
              (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))
                    ⋯)
                (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))
                          ⋯,
                      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))
                          ⋯,
                      left_inv := ⋯, right_inv := ⋯ :
                      { 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) } ≃
                        { b : Opposite.unop V ⟶ X // S.arrows b } }))))
            x) :
        Opposite.unop V ⟶ X)
      (↑(TypeCat.Fun.toFun
            (hom (FC := TypeCat.Fun)
              (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))
                          ⋯,
                      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))
                          ⋯,
                      left_inv := ⋯, right_inv := ⋯ :
                      { 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) } ≃
                        { b : Opposite.unop U ⟶ X // S.arrows b } }))
                (↾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))
                    ⋯)))
            x) :
        Opposite.unop V ⟶ X)
⊢ 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))
          ⋯)
      (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))
                ⋯,
            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))
                ⋯,
            left_inv := ⋯, right_inv := ⋯ })))
    (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))
                ⋯,
            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))
                ⋯,
            left_inv := ⋯, right_inv := ⋯ }))
      (↾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)) ⋯))

Tactic:
ext