-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
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
⊢ ((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
have 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))
              sorry))
      (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))
              sorry) ≫
          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)
Tactic: ext ⟨f, hf⟩