-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q U : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X Y_1 : C
S : Sieve.{v₁, u₁} X
R : Presieve.{v₁, u₁} X
inst_1 : LocallySmall.{w, v₁, u₁} C
F : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
t : { x : FamilyOfElements F S.arrows // x.Compatible (R := S.arrows) }
Y Z : Cᵒᵖ
g : Y ⟶ Z
h :
  ∀ (f : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) Y)
    (hf :
      Membership.mem (γ := Set (Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) Y))
        (Subfunctor.obj (shrinkFunctor.{w, v₁, u₁} S) Y) f),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((Subfunctor.toFunctor (F := Functor.obj shrinkYoneda.{w, v₁, u₁} X) (shrinkFunctor.{w, v₁, u₁} S)).map g ≫
            ↾fun
                (f :
                  (Subfunctor.toFunctor (F := Functor.obj shrinkYoneda.{w, v₁, u₁} X) (shrinkFunctor.{w, v₁, u₁} S)).obj
                    Z) ↦
              (↑t : FamilyOfElements F S.arrows)
                ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj Z) → unop Z ⟶ X)
                  (↑f : (shrinkYoneda.{w, v₁, u₁}.obj X).obj Z))
                ⋯))
        (Subtype.mk (p := fun (x : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) Y) ↦
          Membership.mem (γ := Set (Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) Y))
            (Subfunctor.obj (shrinkFunctor.{w, v₁, u₁} S) Y) x)
          f hf) =
      TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((↾fun
                (f :
                  (Subfunctor.toFunctor (F := Functor.obj shrinkYoneda.{w, v₁, u₁} X) (shrinkFunctor.{w, v₁, u₁} S)).obj
                    Y) ↦
              (↑t : FamilyOfElements F S.arrows)
                ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj Y) → unop Y ⟶ X)
                  (↑f : (shrinkYoneda.{w, v₁, u₁}.obj X).obj Y))
                ⋯) ≫
            F.map g))
        (Subtype.mk (p := fun (x : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) Y) ↦
          Membership.mem (γ := Set (Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) Y))
            (Subfunctor.obj (shrinkFunctor.{w, v₁, u₁} S) Y) x)
          f hf)
⊢ ((Subfunctor.toFunctor (F := Functor.obj shrinkYoneda.{w, v₁, u₁} X) (shrinkFunctor.{w, v₁, u₁} S)).map g ≫
      ↾fun
          (f :
            (Subfunctor.toFunctor (F := Functor.obj shrinkYoneda.{w, v₁, u₁} X) (shrinkFunctor.{w, v₁, u₁} S)).obj Z) ↦
        (↑t : FamilyOfElements F S.arrows)
          ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj Z) → unop Z ⟶ X)
            (↑f : (shrinkYoneda.{w, v₁, u₁}.obj X).obj Z))
          ⋯) =
    (↾fun
          (f :
            (Subfunctor.toFunctor (F := Functor.obj shrinkYoneda.{w, v₁, u₁} X) (shrinkFunctor.{w, v₁, u₁} S)).obj Y) ↦
        (↑t : FamilyOfElements F S.arrows)
          ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj Y) → unop Y ⟶ X)
            (↑f : (shrinkYoneda.{w, v₁, u₁}.obj X).obj Y))
          ⋯) ≫
      F.map g

Tactic:
ext ⟨f, hf⟩