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 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.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)))

Tactic:
Eq.trans ?_ (Presieve.IsSheafFor.valid_glue (h _ s.2)
      ((G.family_of_elements_compatible s.1).map f) (j ≫ i.unop) ?_).symm

Premises used: CategoryTheory.Presieve.FamilyOfElements.Compatible.map, Quiver.Hom.unop, CategoryTheory.CategoryStruct.comp, CategoryTheory.Presieve.IsSheafFor.valid_glue, Eq.symm, Subtype.val, 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₁ :
  (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) ⋯
h₂ : (G.sieveOfSection (↑s : F.obj U)).arrows (j ≫ i.unop)
⊢ 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)))

Tactic:
refine Eq.trans ?_ (Presieve.IsSheafFor.valid_glue (h _ s.2)
      ((G.family_of_elements_compatible s.1).map f) (j ≫ i.unop) ?_).symm

Premises used: CategoryTheory.Presieve.FamilyOfElements.Compatible.map, Quiver.Hom.unop, CategoryTheory.CategoryStruct.comp, CategoryTheory.Presieve.IsSheafFor.valid_glue, Eq.symm, Subtype.val, 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
⊢ 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))

Tactic:
rfl
-- 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₁ :
  Membership.mem (α := F.obj (op W)) (γ := Set (F.obj (op W))) (G.obj (op W))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (i ≫ j.op)) : (a : F.obj U) → F.obj (op W)) (↑s : F.obj U) :
      F.obj (op W))
⊢ (G.sieveOfSection (↑s : F.obj U)).arrows (j ≫ i.unop)

Tactic:
dsimp [Presieve.FamilyOfElements.map] at hj ⊢

Premises used: CategoryTheory.Presieve.FamilyOfElements.map
-- 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 :
  Membership.mem (α := F.obj (op W)) (γ := Set (F.obj (op W))) (G.obj (op W))
    ((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) :
      F.obj (op W))
h₁ :
  Membership.mem (α := F.obj (op W)) (γ := Set (F.obj (op W))) (G.obj (op W))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i ≫ F.map j.op) : (a : F.obj U) → F.obj (op W)) (↑s : F.obj U) :
      F.obj (op W))
h₂ h₃ h₄ h₅ :
  Membership.mem (α := F.obj (op W)) (γ := Set (F.obj (op W))) (G.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) (↑s : F.obj U) : F.obj V) :
      F.obj (op W))
⊢ Membership.mem (α := F.obj (op W)) (γ := Set (F.obj (op W))) (G.obj (op W))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (i ≫ j.op)) : (a : F.obj U) → F.obj (op W)) (↑s : F.obj U) :
      F.obj (op W))

Tactic:
rwa [Functor.map_comp, comp_apply]

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' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
f : G.toFunctor ⟶ F'
h : Presieve.IsSheaf J F'
w :
  ∀ (U : Cᵒᵖ) (s : G.toFunctor.obj U),
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((homOfLe ⋯ ≫ G.sheafifyLift f h).app U)).toFun s =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app U)).toFun s
⊢ homOfLe ⋯ ≫ G.sheafifyLift f h = f

Tactic:
ext U s
-- Module: Mathlib.CategoryTheory.Sites.Subsheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F F' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
f : G.toFunctor ⟶ F'
h : Presieve.IsSheaf J F'
U : Cᵒᵖ
s : G.toFunctor.obj U
w :
  ∀ ⦃Y : C⦄ ⦃f_1 : Y ⟶ unop U⦄,
    Sieve.arrows
        (G.sieveOfSection
          (↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((homOfLe ⋯).app U) :
                  (a : (fun (X : Type w) ↦ X) (G.toFunctor.obj U)) →
                    (fun (X : Type w) ↦ X) ((sheafify J G).toFunctor.obj U))
                s) :
            F.obj U))
        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 U)))) → (fun (X : Type w) ↦ X) (F'.obj (op Y)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) ((homOfLe ⋯ ≫ G.sheafifyLift f h).app U)).toFun 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 U)))) → (fun (X : Type w) ↦ X) (F'.obj (op Y)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app U)).toFun s) :
          (fun (X : Type w) ↦ X) (F'.obj (op Y)))
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) ((homOfLe ⋯ ≫ G.sheafifyLift f h).app U)).toFun s =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app U)).toFun s

Tactic:
apply (h _ ((Subfunctor.homOfLe (G.le_sheafify J)).app U s).prop).isSeparatedFor.ext

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Subfunctor.homOfLe, CategoryTheory.Subfunctor.le_sheafify, CategoryTheory.Presieve.IsSeparatedFor.ext, CategoryTheory.Presieve.IsSheafFor.isSeparatedFor, Subtype.prop, DFunLike.coe, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Sites.Subsheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F F' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
f : G.toFunctor ⟶ F'
h : Presieve.IsSheaf J F'
U : Cᵒᵖ
s : G.toFunctor.obj U
V : C
i : V ⟶ unop U
hi :
  Sieve.arrows
    (G.sieveOfSection
      (↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((homOfLe ⋯).app U) :
              (a : (fun (X : Type w) ↦ X) (G.toFunctor.obj U)) →
                (fun (X : Type w) ↦ X) ((sheafify J G).toFunctor.obj U))
            s) :
        F.obj U))
    i
⊢ ∀ ⦃X Y : Cᵒᵖ⦄ (f_1 : X ⟶ Y) (x : G.toFunctor.obj X),
    Eq (α := F'.obj Y)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Y) : (a : G.toFunctor.obj Y) → F'.obj Y)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.toFunctor.map f_1) :
                (a : G.toFunctor.obj X) → G.toFunctor.obj Y)
              x :
            G.toFunctor.obj Y) :
        F'.obj Y)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F'.map f_1) : (a : F'.obj X) → F'.obj Y)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) : (a : G.toFunctor.obj X) → F'.obj X) x : F'.obj X) :
        F'.obj Y)

Tactic:
have := elementwise_of% f.naturality
-- Module: Mathlib.CategoryTheory.Sites.Subsheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F F' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
f : G.toFunctor ⟶ F'
h : Presieve.IsSheaf J F'
U : Cᵒᵖ
s : G.toFunctor.obj U
V : C
i : V ⟶ unop U
hi :
  Sieve.arrows
    (G.sieveOfSection
      (↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((homOfLe ⋯).app U) :
              (a : (fun (X : Type w) ↦ X) (G.toFunctor.obj U)) →
                (fun (X : Type w) ↦ X) ((sheafify J G).toFunctor.obj U))
            s) :
        F.obj U))
    i
this :
  ∀ ⦃X Y : Cᵒᵖ⦄ (f_1 : X ⟶ Y) (x : G.toFunctor.obj X),
    Eq (α := F'.obj Y)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Y) : (a : G.toFunctor.obj Y) → F'.obj Y)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.toFunctor.map f_1) :
                (a : G.toFunctor.obj X) → G.toFunctor.obj Y)
              x :
            G.toFunctor.obj Y) :
        F'.obj Y)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F'.map f_1) : (a : F'.obj X) → F'.obj Y)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) : (a : G.toFunctor.obj X) → F'.obj X) x : F'.obj X) :
        F'.obj Y)
⊢ 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)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((homOfLe ⋯ ≫ G.sheafifyLift f h).app U)).toFun s) :
      (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)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app U)).toFun s) :
      (fun (X : Type w) ↦ X) (F'.obj (op V)))

Tactic:
(Presieve.IsSheafFor.valid_glue (h _ ((homOfLe (_ : _ ≤ sheafify _ _)).app _ _).2)
    ((G.family_of_elements_compatible _).map _) _ _).trans (this _ _)

Premises used: CategoryTheory.Presieve.FamilyOfElements.Compatible.map, CategoryTheory.ConcreteCategory.hom, CategoryTheory.Subfunctor.homOfLe, CategoryTheory.Presieve.IsSheafFor.amalgamate, Classical.choose, CategoryTheory.Presieve.IsSheafFor.valid_glue, DFunLike.coe, CategoryTheory.Subfunctor.family_of_elements_compatible, CategoryTheory.NatTrans.app, 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' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
f : G.toFunctor ⟶ F'
h : Presieve.IsSheaf J F'
U : Cᵒᵖ
s : G.toFunctor.obj U
V : C
i : V ⟶ unop U
hi :
  Sieve.arrows
    (G.sieveOfSection
      (↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((homOfLe ⋯).app U) :
              (a : (fun (X : Type w) ↦ X) (G.toFunctor.obj U)) →
                (fun (X : Type w) ↦ X) ((sheafify J G).toFunctor.obj U))
            s) :
        F.obj U))
    i
this :
  ∀ ⦃X Y : Cᵒᵖ⦄ (f_1 : X ⟶ Y) (x : G.toFunctor.obj X),
    Eq (α := F'.obj Y)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Y) : (a : G.toFunctor.obj Y) → F'.obj Y)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.toFunctor.map f_1) :
                (a : G.toFunctor.obj X) → G.toFunctor.obj Y)
              x :
            G.toFunctor.obj Y) :
        F'.obj Y)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F'.map f_1) : (a : F'.obj X) → F'.obj Y)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) : (a : G.toFunctor.obj X) → F'.obj X) x : F'.obj X) :
        F'.obj Y)
⊢ 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)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((homOfLe ⋯ ≫ G.sheafifyLift f h).app U)).toFun s) :
      (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)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app U)).toFun s) :
      (fun (X : Type w) ↦ X) (F'.obj (op V)))

Tactic:
exact (Presieve.IsSheafFor.valid_glue (h _ ((homOfLe (_ : _ ≤ sheafify _ _)).app _ _).2)
    ((G.family_of_elements_compatible _).map _) _ _).trans (this _ _)

Premises used: CategoryTheory.Presieve.FamilyOfElements.Compatible.map, CategoryTheory.ConcreteCategory.hom, CategoryTheory.Subfunctor.homOfLe, CategoryTheory.Presieve.IsSheafFor.valid_glue, DFunLike.coe, CategoryTheory.Subfunctor.family_of_elements_compatible, CategoryTheory.NatTrans.app, 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' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
h : Presieve.IsSheaf J F'
l₁ l₂ : (sheafify J G).toFunctor ⟶ F'
e : homOfLe ⋯ ≫ l₁ = homOfLe ⋯ ≫ l₂
w :
  ∀ (U : Cᵒᵖ) (s : (sheafify J G).toFunctor.obj U),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (l₁.app U)).toFun s =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (l₂.app U)).toFun s
⊢ l₁ = l₂

Tactic:
ext U s
-- Module: Mathlib.CategoryTheory.Sites.Subsheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F F' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
h : Presieve.IsSheaf J F'
l₁ l₂ : (sheafify J G).toFunctor ⟶ F'
e : homOfLe ⋯ ≫ l₁ = homOfLe ⋯ ≫ l₂
U : Cᵒᵖ
s : (sheafify J G).toFunctor.obj U
w :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ unop U⦄,
    (G.sieveOfSection (↑s : F.obj U)).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)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (l₁.app U)).toFun s) :
          (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)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (l₂.app U)).toFun s) :
          (fun (X : Type w) ↦ X) (F'.obj (op Y)))
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (l₁.app U)).toFun s =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (l₂.app U)).toFun s

Tactic:
apply (h _ s.prop).isSeparatedFor.ext

Premises used: CategoryTheory.Presieve.IsSeparatedFor.ext, CategoryTheory.Presieve.IsSheafFor.isSeparatedFor, Subtype.prop
-- Module: Mathlib.CategoryTheory.Sites.Subsheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F F' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
h : Presieve.IsSheaf J F'
l₁ l₂ : (sheafify J G).toFunctor ⟶ F'
e : homOfLe ⋯ ≫ l₁ = homOfLe ⋯ ≫ l₂
U : Cᵒᵖ
s : (sheafify J G).toFunctor.obj U
V : C
i : V ⟶ unop U
hi : (G.sieveOfSection (↑s : F.obj U)).arrows i
w :
  Eq (α := F'.obj (op V))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F'.map i.op) : (a : F'.obj U) → F'.obj (op V))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (l₁.app U) : (a : (↑((sheafify J G).obj U) : Type w)) → F'.obj U) s :
          F'.obj U) :
      F'.obj (op V))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F'.map i.op) : (a : F'.obj U) → F'.obj (op V))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (l₂.app U) : (a : (↑((sheafify J G).obj U) : Type w)) → F'.obj U) s :
          F'.obj U) :
      F'.obj (op V))
⊢ 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)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (l₁.app U)).toFun s) :
      (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)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (l₂.app U)).toFun s) :
      (fun (X : Type w) ↦ X) (F'.obj (op V)))

Tactic:
dsimp