-- 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
h₁ :
  TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (Subfunctor.ι (shrinkFunctor.{w, v₁, u₁} S) ≫ g) Y))
      (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)
        u hu) =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (g.app (op (unop Y))) :
        (a : (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v₁, u₁}.obj X).obj (op (unop Y)))) →
          (fun (X : Type w) ↦ X) (F.obj (op (unop Y))))
      ((Equiv.symm shrinkYonedaObjObjEquiv :
            (a : unop (op (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) :
        Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) (op (unop Y)))
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (Subfunctor.ι (shrinkFunctor.{w, v₁, u₁} S) ≫ g) Y))
      (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)
        u hu) =
    (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))

Tactic:
rw [shrinkYonedaEquiv_naturality, shrinkYonedaEquiv_comp, shrinkYonedaEquiv_shrinkYoneda_map]

Premises used: CategoryTheory.shrinkYonedaEquiv_comp, CategoryTheory.shrinkYonedaEquiv_naturality, CategoryTheory.shrinkYonedaEquiv_shrinkYoneda_map