C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf J (toPresheaf G)
⊢ sheafify J G ≤ G
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf J (toPresheaf G)
⊢ G = sheafify J G
apply (G.le_sheafify J).antisymm
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf J (toPresheaf G)
U : Cᵒᵖ
s : F.obj U
hs : s ∈ obj (sheafify J G) U
⊢ s ∈ obj G U
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf J (toPresheaf G)
⊢ sheafify J G ≤ G
intro U s hs
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf J (toPresheaf G)
U : Cᵒᵖ
s : F.obj U
hs : s ∈ obj (sheafify J G) U
⊢ ↑(Presieve.IsSheafFor.amalgamate (_ : Presieve.IsSheafFor (toPresheaf G) (sieveOfSection G s).arrows)
        (familyOfElementsOfSection G s) (_ : Presieve.FamilyOfElements.Compatible (familyOfElementsOfSection G s))) =
    s
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf J (toPresheaf G)
U : Cᵒᵖ
s : F.obj U
hs : s ∈ obj (sheafify J G) U
⊢ s ∈ obj G U
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
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf J (toPresheaf G)
U : Cᵒᵖ
s : F.obj U
hs : s ∈ obj (sheafify J G) U
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ U.unop⦄,
    (sieveOfSection G s).arrows f →
      F.map f.op
          ↑(Presieve.IsSheafFor.amalgamate (_ : Presieve.IsSheafFor (toPresheaf G) (sieveOfSection G s).arrows)
              (familyOfElementsOfSection G s)
              (_ : Presieve.FamilyOfElements.Compatible (familyOfElementsOfSection G s))) =
        F.map f.op s
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf J (toPresheaf G)
U : Cᵒᵖ
s : F.obj U
hs : s ∈ obj (sheafify J G) U
⊢ ↑(Presieve.IsSheafFor.amalgamate (_ : Presieve.IsSheafFor (toPresheaf G) (sieveOfSection G s).arrows)
        (familyOfElementsOfSection G s) (_ : Presieve.FamilyOfElements.Compatible (familyOfElementsOfSection G s))) =
    s
apply (h _ hs).isSeparatedFor.ext
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf J (toPresheaf G)
U : Cᵒᵖ
s : F.obj U
hs : s ∈ obj (sheafify J G) U
V : C
i : V ⟶ U.unop
hi : (sieveOfSection G s).arrows i
⊢ F.map i.op
      ↑(Presieve.IsSheafFor.amalgamate (_ : Presieve.IsSheafFor (toPresheaf G) (sieveOfSection G s).arrows)
          (familyOfElementsOfSection G s) (_ : Presieve.FamilyOfElements.Compatible (familyOfElementsOfSection G s))) =
    F.map i.op s
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf J (toPresheaf G)
U : Cᵒᵖ
s : F.obj U
hs : s ∈ obj (sheafify J G) U
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ U.unop⦄,
    (sieveOfSection G s).arrows f →
      F.map f.op
          ↑(Presieve.IsSheafFor.amalgamate (_ : Presieve.IsSheafFor (toPresheaf G) (sieveOfSection G s).arrows)
              (familyOfElementsOfSection G s)
              (_ : Presieve.FamilyOfElements.Compatible (familyOfElementsOfSection G s))) =
        F.map f.op s
intro V i hi
no goals
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf J (toPresheaf G)
U : Cᵒᵖ
s : F.obj U
hs : s ∈ obj (sheafify J G) U
V : C
i : V ⟶ U.unop
hi : (sieveOfSection G s).arrows i
⊢ F.map i.op
      ↑(Presieve.IsSheafFor.amalgamate (_ : Presieve.IsSheafFor (toPresheaf G) (sieveOfSection G s).arrows)
          (familyOfElementsOfSection G s) (_ : Presieve.FamilyOfElements.Compatible (familyOfElementsOfSection G s))) =
    F.map i.op s
exact (congr_arg Subtype.val ((hG _ hs).valid_glue (G.family_of_elements_compatible s) _ hi) : _)
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf J (toPresheaf G)
U : Cᵒᵖ
s : F.obj U
hs : s ∈ obj (sheafify J G) U
this :
  ↑(Presieve.IsSheafFor.amalgamate (_ : Presieve.IsSheafFor (toPresheaf G) (sieveOfSection G s).arrows)
        (familyOfElementsOfSection G s) (_ : Presieve.FamilyOfElements.Compatible (familyOfElementsOfSection G s))) =
    s
⊢ ↑(Presieve.IsSheafFor.amalgamate (_ : Presieve.IsSheafFor (toPresheaf G) (sieveOfSection G s).arrows)
        (familyOfElementsOfSection G s) (_ : Presieve.FamilyOfElements.Compatible (familyOfElementsOfSection G s))) ∈
    obj G U
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf J (toPresheaf G)
U : Cᵒᵖ
s : F.obj U
hs : s ∈ obj (sheafify J G) U
this :
  ↑(Presieve.IsSheafFor.amalgamate (_ : Presieve.IsSheafFor (toPresheaf G) (sieveOfSection G s).arrows)
        (familyOfElementsOfSection G s) (_ : Presieve.FamilyOfElements.Compatible (familyOfElementsOfSection G s))) =
    s
⊢ s ∈ obj G U
rw [← this]
no goals
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf J (toPresheaf G)
U : Cᵒᵖ
s : F.obj U
hs : s ∈ obj (sheafify J G) U
this :
  ↑(Presieve.IsSheafFor.amalgamate (_ : Presieve.IsSheafFor (toPresheaf G) (sieveOfSection G s).arrows)
        (familyOfElementsOfSection G s) (_ : Presieve.FamilyOfElements.Compatible (familyOfElementsOfSection G s))) =
    s
⊢ ↑(Presieve.IsSheafFor.amalgamate (_ : Presieve.IsSheafFor (toPresheaf G) (sieveOfSection G s).arrows)
        (familyOfElementsOfSection G s) (_ : Presieve.FamilyOfElements.Compatible (familyOfElementsOfSection G s))) ∈
    obj G U
exact ((hG _ hs).amalgamate _ (G.family_of_elements_compatible s)).2