-- 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₁ :
  Presieve.FamilyOfElements.map (R :=
      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)))
      (G.familyOfElementsOfSection
        (↑((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))
      f j hj =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F'.map j.op) :
        (a : (fun (X : Type w) ↦ X) (F'.obj (op (unop V)))) → (fun (X : Type w) ↦ X) (F'.obj (op W)))
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((↾fun (s : (sheafify J G).toFunctor.obj U) ↦
              ⋯.amalgamate (R := (G.sieveOfSection (↑s : F.obj U)).arrows)
                ((G.familyOfElementsOfSection (↑s : F.obj U)).map (R := (G.sieveOfSection (↑s : F.obj U)).arrows) f)
                ⋯) ≫
            F'.map i))
        s)
⊢ Eq (α := (fun (X : Type w) ↦ X) (F'.obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F'.map j.op) :
          (a : (fun (X : Type w) ↦ X) (F'.obj (op (unop V)))) → (fun (X : Type w) ↦ X) (F'.obj (op W)))
        (TypeCat.Fun.toFun
          (ConcreteCategory.hom (FC := TypeCat.Fun)
            ((sheafify J G).toFunctor.map i ≫
              ↾fun (s : (sheafify J G).toFunctor.obj V) ↦
                ⋯.amalgamate (R := (G.sieveOfSection (↑s : F.obj V)).arrows)
                  ((G.familyOfElementsOfSection (↑s : F.obj V)).map (R := (G.sieveOfSection (↑s : F.obj V)).arrows) f)
                  ⋯))
          s) :
      (fun (X : Type w) ↦ X) (F'.obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F'.map j.op) :
          (a : (fun (X : Type w) ↦ X) (F'.obj (op (unop V)))) → (fun (X : Type w) ↦ X) (F'.obj (op W)))
        (TypeCat.Fun.toFun
          (ConcreteCategory.hom (FC := TypeCat.Fun)
            ((↾fun (s : (sheafify J G).toFunctor.obj U) ↦
                ⋯.amalgamate (R := (G.sieveOfSection (↑s : F.obj U)).arrows)
                  ((G.familyOfElementsOfSection (↑s : F.obj U)).map (R := (G.sieveOfSection (↑s : F.obj U)).arrows) f)
                  ⋯) ≫
              F'.map i))
          s) :
      (fun (X : Type w) ↦ X) (F'.obj (op W)))

Tactic:
refine (Presieve.IsSheafFor.valid_glue (h _ ((G.sheafify J).toFunctor.map i s).2)
      ((G.family_of_elements_compatible _).map _) _ hj).trans ?_

Premises used: CategoryTheory.Presieve.FamilyOfElements.Compatible.map, CategoryTheory.ConcreteCategory.hom, CategoryTheory.Subfunctor.toFunctor, CategoryTheory.Functor.map, CategoryTheory.Subfunctor.sheafify, CategoryTheory.Presieve.IsSheafFor.valid_glue, DFunLike.coe, CategoryTheory.Subfunctor.family_of_elements_compatible, Eq.trans, Subtype.property