-- 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
V' : C
i' : V' ⟶ unop (op V)
hi' : (G.sieveOfSection ↑(x i hi)).arrows i'
hi'' : S'.arrows (i' ≫ i)
this : (F.map i.op ≫ F.map i'.op) ↑s = x'' (i' ≫ i) hi''
⊢ F.map i'.op ↑((sheafify J G).toPresheaf.map i.op s) = F.map i'.op ↑(x i hi)

Tactic:
exact this.trans (congr_arg Subtype.val (hx _ _ (hi₂ _ _ hi'') hi (h₂ _ _ hi'')))

Result:
no goals

Proof state:
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
⊢ x''.Compatible

Tactic:
intro V₁ V₂ V₃ g₁ g₂ g₃ g₄ S₁ S₂ e

Result:
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
V₁ V₂ V₃ : C
g₁ : V₃ ⟶ V₁
g₂ : V₃ ⟶ V₂
g₃ : V₁ ⟶ U
g₄ : V₂ ⟶ U
S₁ : S'.arrows g₃
S₂ : S'.arrows g₄
e : g₁ ≫ g₃ = g₂ ≫ g₄
⊢ F.map g₁.op (x'' g₃ S₁) = F.map g₂.op (x'' g₄ S₂)

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
V : C
i : V ⟶ unop (op U)
hi : (Sieve.bind S.arrows fun V i hi => G.sieveOfSection ↑(x i hi)).arrows i
⊢ x'' i hi ∈ G.obj (op V)

Tactic:
exact h₁ _ _ hi

Result:
no goals

Proof state:
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)), x.IsAmalgamation s ↔ x''.IsAmalgamation ↑s

Tactic:
intro s

Result:
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)
⊢ x.IsAmalgamation s ↔ x''.IsAmalgamation ↑s