-- Module: Mathlib.CategoryTheory.Sites.Subsheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F F' F'' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G G' : Subfunctor F
f : G.toFunctor ⟶ F'
h : Presieve.IsSheaf J F'
U V : Cᵒᵖ
i : U ⟶ V
s : (sheafify J G).toFunctor.obj U
W : C
j : W ⟶ unop V
hj :
  Sieve.arrows
    (G.sieveOfSection
      (↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((sheafify J G).toFunctor.map i) :
              (a : (fun (X : Type w) ↦ X) ((sheafify J G).toFunctor.obj U)) →
                (fun (X : Type w) ↦ X) ((sheafify J G).toFunctor.obj V))
            s) :
        F.obj V))
    j
h₁ :
  Eq (α := F'.obj (op W))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op W)) : (a : (↑(G.obj (op W)) : Type w)) → F'.obj (op W))
        (Subtype.mk (p := fun (x : F.obj (op W)) ↦ Membership.mem (γ := Set (F.obj (op W))) (G.obj (op W)) x)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map j.op) : (a : F.obj V) → F.obj (op W))
              (↑(({
                        toFun := fun (x : (↑((sheafify J G).obj U) : Type w)) ↦
                          Subtype.mk (p := fun (x : F.obj V) ↦ x ∈ (sheafify J G).obj V)
                            ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i) : (a : F.obj U) → F.obj V)
                              (↑x : F.obj U))
                            ⋯ } :
                      (a : (↑((sheafify J G).obj U) : Type w)) → (↑((sheafify J G).obj V) : Type w))
                    s) :
                F.obj V))
            hj :
          { x : F.obj (op W) // Membership.mem (γ := Set (F.obj (op W))) (G.obj (op W)) x }) :
      F'.obj (op W))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op W)) : (a : (↑(G.obj (op W)) : Type w)) → F'.obj (op W))
        (Subtype.mk (p := fun (x : F.obj (op W)) ↦ Membership.mem (γ := Set (F.obj (op W))) (G.obj (op W)) x)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map j.op) : (a : F.obj V) → F.obj (op W))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i) : (a : F.obj U) → F.obj V) (↑s : F.obj U) : F.obj V))
            ⋯ :
          { x : F.obj (op W) // Membership.mem (γ := Set (F.obj (op W))) (G.obj (op W)) x }) :
      F'.obj (op W))
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op W)) : (a : (↑(G.obj (op W)) : Type w)) → F'.obj (op W))
      (G.familyOfElementsOfSection
        (↑(({
                  toFun := fun (x : (↑((sheafify J G).obj U) : Type w)) ↦
                    Subtype.mk (p := fun (x : F.obj V) ↦ x ∈ (sheafify J G).obj V)
                      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i) : (a : F.obj U) → F.obj V) (↑x : F.obj U))
                      ⋯ :
                  TypeCat.Fun (↑((sheafify J G).obj U) : Type w) (↑((sheafify J G).obj V) : Type w) } :
                (a : (↑((sheafify J G).obj U) : Type w)) → (↑((sheafify J G).obj V) : Type w))
              s) :
          F.obj V)
        j hj) =
    (G.familyOfElementsOfSection (↑s : F.obj U)).map (R := (G.sieveOfSection (↑s : F.obj U)).arrows) f (j ≫ i.unop) ⋯

Tactic:
simp [Presieve.FamilyOfElements.map, Subfunctor.familyOfElementsOfSection]

Premises used: CategoryTheory.Presieve.FamilyOfElements.map, CategoryTheory.Subfunctor.familyOfElementsOfSection