awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Subsheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf.{w, v, u} J G.toFunctor
apply : sheafify J G ≤ G
⊢ G = sheafify J G

Tactic:
apply (G.le_sheafify J).antisymm

Premises used: LE.le.antisymm, CategoryTheory.Subfunctor.le_sheafify
-- Module: Mathlib.CategoryTheory.Sites.Subsheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf.{w, v, u} J G.toFunctor
U : Cᵒᵖ
s : F.obj U
hs : s ∈ (sheafify J G).obj U
this : (↑(⋯.amalgamate (R := (G.sieveOfSection s).arrows) (G.familyOfElementsOfSection s) ⋯) : F.obj (op (unop U))) = s
rw :
  (↑(⋯.amalgamate (R := (G.sieveOfSection s).arrows) (G.familyOfElementsOfSection s) ⋯) : F.obj (op (unop U))) ∈ G.obj U
⊢ s ∈ G.obj U

Tactic:
rw [← this]
-- Module: Mathlib.CategoryTheory.Sites.Subsheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf.{w, v, u} J G.toFunctor
U : Cᵒᵖ
s : F.obj U
hs : s ∈ (sheafify J G).obj U
this : (↑(⋯.amalgamate (R := (G.sieveOfSection s).arrows) (G.familyOfElementsOfSection s) ⋯) : F.obj (op (unop U))) = s
⊢ (↑(⋯.amalgamate (R := (G.sieveOfSection s).arrows) (G.familyOfElementsOfSection s) ⋯) : F.obj (op (unop U))) ∈ G.obj U

Tactic:
((hG _ hs).amalgamate _ (G.family_of_elements_compatible s)).2

Premises used: Set.Mem, CategoryTheory.Presieve.IsSheafFor.amalgamate, CategoryTheory.Subfunctor.family_of_elements_compatible, Subtype.property
-- Module: Mathlib.CategoryTheory.Sites.Subsheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf.{w, v, u} J G.toFunctor
U : Cᵒᵖ
s : F.obj U
hs : s ∈ (sheafify J G).obj U
this : (↑(⋯.amalgamate (R := (G.sieveOfSection s).arrows) (G.familyOfElementsOfSection s) ⋯) : F.obj (op (unop U))) = s
⊢ (↑(⋯.amalgamate (R := (G.sieveOfSection s).arrows) (G.familyOfElementsOfSection s) ⋯) : F.obj (op (unop U))) ∈ G.obj U

Tactic:
exact ((hG _ hs).amalgamate _ (G.family_of_elements_compatible s)).2

Premises used: CategoryTheory.Presieve.IsSheafFor.amalgamate, CategoryTheory.Subfunctor.family_of_elements_compatible, Subtype.property
-- Module: Mathlib.CategoryTheory.Sites.Subsheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf.{w, v, u} J G.toFunctor
U : Cᵒᵖ
s : F.obj U
hs : s ∈ (sheafify J G).obj U
suffices :
  (↑(⋯.amalgamate (R := (G.sieveOfSection s).arrows) (G.familyOfElementsOfSection s) ⋯) : F.obj (op (unop U))) = s
⊢ s ∈ G.obj U

Tactic:
suffices ((hG _ hs).amalgamate _ (G.family_of_elements_compatible s)).1 = s by
    rw [← this]
    exact ((hG _ hs).amalgamate _ (G.family_of_elements_compatible s)).2
-- Module: Mathlib.CategoryTheory.Sites.Subsheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf.{w, v, u} J G.toFunctor
U : Cᵒᵖ
s : F.obj U
hs : s ∈ (sheafify J G).obj U
apply :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ unop U⦄,
    (G.sieveOfSection s).arrows f →
      Eq (α := (fun (X : Type w) ↦ X) (F.obj (op Y)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
              (a : (fun (X : Type w) ↦ X) (F.obj (op (unop U)))) → (fun (X : Type w) ↦ X) (F.obj (op Y)))
            (↑(⋯.amalgamate (R := (G.sieveOfSection s).arrows) (G.familyOfElementsOfSection s) ⋯) :
              F.obj (op (unop U))) :
          (fun (X : Type w) ↦ X) (F.obj (op Y)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
              (a : (fun (X : Type w) ↦ X) (F.obj (op (unop U)))) → (fun (X : Type w) ↦ X) (F.obj (op Y)))
            s :
          (fun (X : Type w) ↦ X) (F.obj (op Y)))
⊢ (↑(⋯.amalgamate (R := (G.sieveOfSection s).arrows) (G.familyOfElementsOfSection s) ⋯) : F.obj (op (unop U))) = s

Tactic:
apply (h _ hs).isSeparatedFor.ext

Premises used: CategoryTheory.Presieve.IsSeparatedFor.ext, CategoryTheory.Presieve.IsSheafFor.isSeparatedFor
-- Module: Mathlib.CategoryTheory.Sites.Subsheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf.{w, v, u} J G.toFunctor
U : Cᵒᵖ
s : F.obj U
hs : s ∈ (sheafify J G).obj U
V : C
i : V ⟶ unop U
hi : (G.sieveOfSection s).arrows i
⊢ Eq (α := (fun (X : Type w) ↦ X) (F.obj (op V)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (op (unop U)))) → (fun (X : Type w) ↦ X) (F.obj (op V)))
        (↑(⋯.amalgamate (R := (G.sieveOfSection s).arrows) (G.familyOfElementsOfSection s) ⋯) : F.obj (op (unop U))) :
      (fun (X : Type w) ↦ X) (F.obj (op V)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (op (unop U)))) → (fun (X : Type w) ↦ X) (F.obj (op V)))
        s :
      (fun (X : Type w) ↦ X) (F.obj (op V)))

Tactic:
(congr_arg Subtype.val ((hG _ hs).valid_glue (G.family_of_elements_compatible s) _ hi) :)

Premises used: congr_arg, CategoryTheory.Presieve.IsSheafFor.valid_glue, Subtype.val, CategoryTheory.Subfunctor.family_of_elements_compatible
-- Module: Mathlib.CategoryTheory.Sites.Subsheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf.{w, v, u} J G.toFunctor
U : Cᵒᵖ
s : F.obj U
hs : s ∈ (sheafify J G).obj U
V : C
i : V ⟶ unop U
hi : (G.sieveOfSection s).arrows i
⊢ Eq (α := (fun (X : Type w) ↦ X) (F.obj (op V)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (op (unop U)))) → (fun (X : Type w) ↦ X) (F.obj (op V)))
        (↑(⋯.amalgamate (R := (G.sieveOfSection s).arrows) (G.familyOfElementsOfSection s) ⋯) : F.obj (op (unop U))) :
      (fun (X : Type w) ↦ X) (F.obj (op V)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (op (unop U)))) → (fun (X : Type w) ↦ X) (F.obj (op V)))
        s :
      (fun (X : Type w) ↦ X) (F.obj (op V)))

Tactic:
exact (congr_arg Subtype.val ((hG _ hs).valid_glue (G.family_of_elements_compatible s) _ hi) :)

Premises used: congr_arg, CategoryTheory.Presieve.IsSheafFor.valid_glue, Subtype.val, CategoryTheory.Subfunctor.family_of_elements_compatible
-- Module: Mathlib.CategoryTheory.Sites.Subsheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
h : Presieve.IsSheaf J F
⊢ G = sheafify J G ↔ Presieve.IsSheaf.{w, v, u} J G.toFunctor

Tactic:
⟨fun e => e.symm ▸ G.sheafify_isSheaf h, G.eq_sheafify h⟩

Premises used: Eq.rec, CategoryTheory.Subfunctor.sheafify_isSheaf, Iff.intro, CategoryTheory.Subfunctor.eq_sheafify, Eq.symm
-- Module: Mathlib.CategoryTheory.Sites.Subsheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
h : Presieve.IsSheaf J F
rw :
  G = sheafify J G ↔
    ∀ (U : Cᵒᵖ) (s : F.obj U),
      Membership.mem (γ := Set (Sieve.{v, u} (unop U))) ((J : (a : C) → Set (Sieve a)) (unop U)) (G.sieveOfSection s) →
        s ∈ G.obj U
⊢ Presieve.IsSheaf.{w, v, u} J G.toFunctor ↔
    ∀ (U : Cᵒᵖ) (s : F.obj U),
      Membership.mem (γ := Set (Sieve.{v, u} (unop U))) ((J : (a : C) → Set (Sieve a)) (unop U)) (G.sieveOfSection s) →
        s ∈ G.obj U

Tactic:
rw [← G.eq_sheafify_iff h]

Premises used: CategoryTheory.Subfunctor.eq_sheafify_iff
-- Module: Mathlib.CategoryTheory.Sites.Subsheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
h : Presieve.IsSheaf J F
⊢ G = sheafify J G ↔ sheafify J G ≤ G

Tactic:
⟨Eq.ge, (G.le_sheafify J).antisymm⟩

Premises used: Eq.ge, LE.le.antisymm, CategoryTheory.Subfunctor.le_sheafify, Iff.intro
-- Module: Mathlib.CategoryTheory.Sites.Subsheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
h : Presieve.IsSheaf J F
⊢ G = sheafify J G ↔ sheafify J G ≤ G

Tactic:
exact ⟨Eq.ge, (G.le_sheafify J).antisymm⟩
-- Module: Mathlib.CategoryTheory.Sites.Subsheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
h : Presieve.IsSheaf J F
⊢ sheafify J (sheafify J G) = sheafify J G

Tactic:
((Subfunctor.eq_sheafify_iff _ h).mpr <| G.sheafify_isSheaf h).symm

Premises used: Iff.mpr, CategoryTheory.Subfunctor.sheafify_isSheaf, Eq.symm, CategoryTheory.Subfunctor.eq_sheafify_iff
-- 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
h₁ :
  ∀ ⦃Y : C⦄ ⦃f_1 : Y ⟶ unop V⦄,
    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))
        f_1 →
      Eq (α := (fun (X : Type w) ↦ X) (F'.obj (op Y)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F'.map f_1.op) :
              (a : (fun (X : Type w) ↦ X) (F'.obj (op (unop V)))) → (fun (X : Type w) ↦ X) (F'.obj (op Y)))
            (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 Y)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F'.map f_1.op) :
              (a : (fun (X : Type w) ↦ X) (F'.obj (op (unop V)))) → (fun (X : Type w) ↦ X) (F'.obj (op Y)))
            (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 Y)))
⊢ 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 =
    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

Tactic:
apply (h _ ((Subfunctor.sheafify J G).toFunctor.map i s).prop).isSeparatedFor.ext

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Presieve.IsSeparatedFor.ext, CategoryTheory.Subfunctor.toFunctor, CategoryTheory.Functor.map, CategoryTheory.Presieve.IsSheafFor.isSeparatedFor, Subtype.prop, CategoryTheory.Subfunctor.sheafify, DFunLike.coe
-- 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
⊢ 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:
(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.Presieve.IsSheafFor.amalgamate, Classical.choose, CategoryTheory.Subfunctor.sheafify, CategoryTheory.Presieve.IsSheafFor.valid_glue, DFunLike.coe, CategoryTheory.Subfunctor.family_of_elements_compatible, Eq.trans, Subtype.property
-- 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))
        (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) :
      F'.obj (op W))
    ((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)
            (⋯.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'.obj V) :
      F'.obj (op W))
⊢ 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)

Tactic:
dsimp
-- 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))
        (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) :
      F'.obj (op W))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F'.map (i ≫ j.op)) : (a : F'.obj U) → F'.obj (op W))
        (⋯.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'.obj (op W))
⊢ 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))
        (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) :
      F'.obj (op W))
    ((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)
            (⋯.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'.obj V) :
      F'.obj (op W))

Tactic:
simp only [← comp_apply, ← Functor.map_comp]

Premises used: CategoryTheory.comp_apply, CategoryTheory.Functor.map_comp
-- 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 (α := (fun (X : Type 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) :
      F'.obj (op W))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F'.map (j ≫ i.unop).op) :
          (a : (fun (X : Type w) ↦ X) (F'.obj (op (unop U)))) → (fun (X : Type w) ↦ X) (F'.obj (op W)))
        (⋯.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) ⋯) :
      (fun (X : Type w) ↦ X) (F'.obj (op W)))
⊢ 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))
        (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) :
      F'.obj (op W))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F'.map (i ≫ j.op)) : (a : F'.obj U) → F'.obj (op W))
        (⋯.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'.obj (op W))

Tactic:
change _ = F'.map (j ≫ i.unop).op _

Premises used: CategoryTheory.ConcreteCategory.hom, Quiver.Hom.op, Quiver.Hom.unop, CategoryTheory.Functor.map, CategoryTheory.CategoryStruct.comp, DFunLike.coe