-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
S : Sieve.{v₁, u₁} X
inst_1 : LocallySmall.{w, v₁, u₁} C
F : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
f : Subfunctor.toFunctor (F := Functor.obj shrinkYoneda.{w, v₁, u₁} X) (shrinkFunctor.{w, v₁, u₁} S) ⟶ F
g : Functor.obj shrinkYoneda.{w, v₁, u₁} X ⟶ F
h :
  ∀ ⦃Y : C⦄ (f_1 : Y ⟶ X) (h : S.arrows f_1),
    Eq (α := F.obj (op Y))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f_1.op) : (a : F.obj (op X)) → F.obj (op Y))
          ((shrinkYonedaEquiv : (a : shrinkYoneda.{w, v₁, u₁}.obj X ⟶ F) → F.obj (op X)) g : F.obj (op X)) :
        F.obj (op Y))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op Y)) :
            (a :
                { x : (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y) //
                  S.arrows
                    ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y)) → Y ⟶ X) x) }) →
              F.obj (op Y))
          (Subtype.mk (p := fun (x : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) (op Y)) ↦
              S.arrows (Y := Y)
                ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y)) → Y ⟶ X) x))
              ((Equiv.symm shrinkYonedaObjObjEquiv : (a : Y ⟶ X) → (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y)) f_1) ⋯ :
            { x : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) (op Y) //
              S.arrows (Y := Y)
                ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y)) → Y ⟶ X) x) }) :
        F.obj (op Y))
Y : Cᵒᵖ
u : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) Y
hu :
  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) u
⊢ Eq (α := F.obj (op (unop Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (F.map
              (Quiver.Hom.op
                ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj Y) → unop Y ⟶ X) u))) :
          (a : F.obj (op X)) → F.obj (op (unop Y)))
        ((shrinkYonedaEquiv : (a : shrinkYoneda.{w, v₁, u₁}.obj X ⟶ F) → F.obj (op X)) g : F.obj (op X)) :
      F.obj (op (unop Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op (unop Y))) :
          (a :
              { x : (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op (unop Y)) //
                S.arrows
                  ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op (unop Y))) → unop Y ⟶ X)
                    x) }) →
            F.obj (op (unop Y)))
        (Subtype.mk (p :=
            fun (x : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) (op (unop Y))) ↦
            S.arrows (Y := unop Y)
              ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op (unop Y))) → unop Y ⟶ X) x))
            ((Equiv.symm shrinkYonedaObjObjEquiv :
                (a : unop Y ⟶ X) → (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op (unop Y)))
              ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj Y) → unop Y ⟶ X) u))
            ⋯ :
          { x : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) (op (unop Y)) //
            S.arrows (Y := unop Y)
              ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op (unop Y))) → unop Y ⟶ X) x) }) :
      F.obj (op (unop Y)))

Tactic:
h (shrinkYonedaObjObjEquiv u) hu

Premises used: CategoryTheory.shrinkYonedaObjObjEquiv, DFunLike.coe