-- Mathlib/CategoryTheory/Sites/Subsheaf.lean
theorem Subpresheaf.eq_sheafify (h : Presieve.IsSheaf J F) (hG : Presieve.IsSheaf J G.toPresheaf) :
    G = G.sheafify J

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf J G.toPresheaf
U : Cᵒᵖ
s : F.obj U
hs : s ∈ (sheafify J G).obj U
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ unop U⦄,
    (G.sieveOfSection s).arrows f → F.map f.op ↑(⋯.amalgamate (G.familyOfElementsOfSection s) ⋯) = F.map f.op s

Tactic:
intro V i hi

Result:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf J G.toPresheaf
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
⊢ F.map i.op ↑(⋯.amalgamate (G.familyOfElementsOfSection s) ⋯) = F.map i.op s

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf J G.toPresheaf
U : Cᵒᵖ
s : F.obj U
hs : s ∈ (sheafify J G).obj U
⊢ 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

Result:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf J G.toPresheaf
U : Cᵒᵖ
s : F.obj U
hs : s ∈ (sheafify J G).obj U
⊢ ↑(⋯.amalgamate (G.familyOfElementsOfSection s) ⋯) = s

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf J G.toPresheaf
⊢ G = sheafify J G

Tactic:
apply (G.le_sheafify J).antisymm

Result:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf J G.toPresheaf
⊢ sheafify J G ≤ G

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf J G.toPresheaf
U : Cᵒᵖ
s : F.obj U
hs : s ∈ (sheafify J G).obj U
this : ↑(⋯.amalgamate (G.familyOfElementsOfSection s) ⋯) = s
⊢ s ∈ G.obj U

Tactic:
rw [← this]

Result:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf J G.toPresheaf
U : Cᵒᵖ
s : F.obj U
hs : s ∈ (sheafify J G).obj U
this : ↑(⋯.amalgamate (G.familyOfElementsOfSection s) ⋯) = s
⊢ ↑(⋯.amalgamate (G.familyOfElementsOfSection s) ⋯) ∈ G.obj U

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf J G.toPresheaf
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
⊢ F.map i.op ↑(⋯.amalgamate (G.familyOfElementsOfSection s) ⋯) = F.map i.op s

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

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf J G.toPresheaf
U : Cᵒᵖ
s : F.obj U
hs : s ∈ (sheafify J G).obj U
this : ↑(⋯.amalgamate (G.familyOfElementsOfSection s) ⋯) = s
⊢ ↑(⋯.amalgamate (G.familyOfElementsOfSection s) ⋯) ∈ G.obj U

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

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf J G.toPresheaf
U : Cᵒᵖ
s : F.obj U
hs : s ∈ (sheafify J G).obj U
⊢ ↑(⋯.amalgamate (G.familyOfElementsOfSection s) ⋯) = s

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

Result:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf J G.toPresheaf
U : Cᵒᵖ
s : F.obj U
hs : s ∈ (sheafify J G).obj U
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ unop U⦄,
    (G.sieveOfSection s).arrows f → F.map f.op ↑(⋯.amalgamate (G.familyOfElementsOfSection s) ⋯) = F.map f.op s

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf J G.toPresheaf
⊢ sheafify J G ≤ G

Tactic:
intro U s hs

Result:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf J G.toPresheaf
U : Cᵒᵖ
s : F.obj U
hs : s ∈ (sheafify J G).obj U
⊢ s ∈ G.obj U