-- Mathlib/CategoryTheory/Sites/Subsheaf.lean
theorem Subpresheaf.sheafify_isSheaf (hF : Presieve.IsSheaf J F) :
    Presieve.IsSheaf J (G.sheafify J).toPresheaf

Proof state:
case mpr
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ J U
x : Presieve.FamilyOfElements (sheafify J G).toPresheaf S.arrows
hx : x.Compatible
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => G.sieveOfSection ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), F.map (i₁ V i hi).op ↑(x (i₂ V i hi) ⋯) ∈ G.obj (op V)
h₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows := fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) ⋯)
s : (sheafify J G).toPresheaf.obj (op U)
H : x''.IsAmalgamation ↑s
V : C
i : V ⟶ U
hi : S.arrows i
⊢ (sheafify J G).toPresheaf.map i.op s = x i hi

Tactic:
refine Subtype.ext ?_

Result:
case mpr
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ J U
x : Presieve.FamilyOfElements (sheafify J G).toPresheaf S.arrows
hx : x.Compatible
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => G.sieveOfSection ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), F.map (i₁ V i hi).op ↑(x (i₂ V i hi) ⋯) ∈ G.obj (op V)
h₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows := fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) ⋯)
s : (sheafify J G).toPresheaf.obj (op U)
H : x''.IsAmalgamation ↑s
V : C
i : V ⟶ U
hi : S.arrows i
⊢ ↑((sheafify J G).toPresheaf.map i.op s) = ↑(x i hi)

Proof state:
case intro.intro
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ J U
x : Presieve.FamilyOfElements (sheafify J G).toPresheaf S.arrows
hx : x.Compatible
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => G.sieveOfSection ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), F.map (i₁ V i hi).op ↑(x (i₂ V i hi) ⋯) ∈ G.obj (op V)
h₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows := fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) ⋯)
H : ∀ (s : (sheafify J G).toPresheaf.obj (op U)), x.IsAmalgamation s ↔ x''.IsAmalgamation ↑s
this : x''.Compatible
t : F.obj (op U)
ht : x''.IsAmalgamation t
ht' : ∀ (y : F.obj (op U)), (fun t => x''.IsAmalgamation t) y → y = t
⊢ t ∈ (sheafify J G).obj (op U)

Tactic:
refine J.superset_covering ?_ (J.bind_covering hS fun V i hi => (x i hi).2)

Result:
case intro.intro
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ J U
x : Presieve.FamilyOfElements (sheafify J G).toPresheaf S.arrows
hx : x.Compatible
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => G.sieveOfSection ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), F.map (i₁ V i hi).op ↑(x (i₂ V i hi) ⋯) ∈ G.obj (op V)
h₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows := fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) ⋯)
H : ∀ (s : (sheafify J G).toPresheaf.obj (op U)), x.IsAmalgamation s ↔ x''.IsAmalgamation ↑s
this : x''.Compatible
t : F.obj (op U)
ht : x''.IsAmalgamation t
ht' : ∀ (y : F.obj (op U)), (fun t => x''.IsAmalgamation t) y → y = t
⊢ (Sieve.bind S.arrows fun V i hi => G.sieveOfSection ↑(x i hi)) ≤ G.sieveOfSection t

Proof state:
case mp
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ J U
x : Presieve.FamilyOfElements (sheafify J G).toPresheaf S.arrows
hx : x.Compatible
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => G.sieveOfSection ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), F.map (i₁ V i hi).op ↑(x (i₂ V i hi) ⋯) ∈ G.obj (op V)
h₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows := fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) ⋯)
s : (sheafify J G).toPresheaf.obj (op U)
H : x.IsAmalgamation s
V : C
i : V ⟶ U
hi : S'.arrows i
⊢ F.map i.op ↑s = F.map (i₁ V i hi).op ↑(x (i₂ V i hi) ⋯)

Tactic:
conv_lhs => rw [← h₂ _ _ hi]

Result:
case mp
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ J U
x : Presieve.FamilyOfElements (sheafify J G).toPresheaf S.arrows
hx : x.Compatible
S' : Sieve U := Sieve.bind S.arrows fun Y f hf => G.sieveOfSection ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), F.map (i₁ V i hi).op ↑(x (i₂ V i hi) ⋯) ∈ G.obj (op V)
h₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows := fun V i hi => F.map (i₁ V i hi).op ↑(x (i₂ V i hi) ⋯)
s : (sheafify J G).toPresheaf.obj (op U)
H : x.IsAmalgamation s
V : C
i : V ⟶ U
hi : S'.arrows i
⊢ F.map (i₁ V i hi ≫ i₂ V i hi).op ↑s = F.map (i₁ V i hi).op ↑(x (i₂ V i hi) ⋯)