-- Mathlib/CategoryTheory/Sites/Coherent/CoherentSheaves.lean
theorem isSheaf_yoneda_obj (W : C) : Presieve.IsSheaf (coherentTopology C) (yoneda.obj W)

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Precoherent C
W : C
⊢ Presieve.IsSheaf (coherentTopology C) (yoneda.obj W)

Tactic:
rw [isSheaf_coherent]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Precoherent C
W : C
⊢ ∀ (B : C) (α : Type) [inst : Finite α] (X : α → C) (π : (a : α) → X a ⟶ B),
    EffectiveEpiFamily X π → Presieve.IsSheafFor (yoneda.obj W) (Presieve.ofArrows X π)

Proof state:
case intro.intro.refine_1
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Precoherent C
W X : C
α : Type
inst✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : Limits.IsColimit (Sieve.generate (Presieve.ofArrows Y π)).arrows.cocone
x : Presieve.FamilyOfElements (yoneda.obj W) (Presieve.ofArrows Y π)
hx : x.Compatible
x_ext : Presieve.FamilyOfElements (yoneda.obj W) (Sieve.generate (Presieve.ofArrows Y π)).arrows := x.sieveExtend
hx_ext : x.sieveExtend.Compatible
S : Sieve X := Sieve.generate (Presieve.ofArrows Y π)
t : (yoneda.obj W).obj (Opposite.op X)
t_amalg : x_ext.IsAmalgamation t
t_uniq : ∀ (y : (yoneda.obj W).obj (Opposite.op X)), (fun t => x_ext.IsAmalgamation t) y → y = t
⊢ (fun t => x.IsAmalgamation t) t

Tactic:
convert Presieve.isAmalgamation_restrict (Sieve.le_generate (Presieve.ofArrows Y π)) _ _ t_amalg

Result:
case h.e.h.e'_6.h.h.h
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Precoherent C
W X : C
α : Type
inst✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : Limits.IsColimit (Sieve.generate (Presieve.ofArrows Y π)).arrows.cocone
x : Presieve.FamilyOfElements (yoneda.obj W) (Presieve.ofArrows Y π)
hx : x.Compatible
x_ext : Presieve.FamilyOfElements (yoneda.obj W) (Sieve.generate (Presieve.ofArrows Y π)).arrows := x.sieveExtend
hx_ext : x.sieveExtend.Compatible
S : Sieve X := Sieve.generate (Presieve.ofArrows Y π)
t : (yoneda.obj W).obj (Opposite.op X)
t_amalg : x_ext.IsAmalgamation t
t_uniq : ∀ (y : (yoneda.obj W).obj (Opposite.op X)), (fun t => x_ext.IsAmalgamation t) y → y = t
⊢ x = Presieve.FamilyOfElements.restrict ⋯ x_ext

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Precoherent C
W X : C
α : Type
inst✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : Limits.IsColimit (Sieve.generate (Presieve.ofArrows Y π)).arrows.cocone
x : Presieve.FamilyOfElements (yoneda.obj W) (Presieve.ofArrows Y π)
hx : x.Compatible
x_ext : Presieve.FamilyOfElements (yoneda.obj W) (Sieve.generate (Presieve.ofArrows Y π)).arrows := x.sieveExtend
hx_ext : x.sieveExtend.Compatible
S : Sieve X := Sieve.generate (Presieve.ofArrows Y π)
⊢ ∃! t, x.IsAmalgamation t

Tactic:
obtain ⟨t, t_amalg, t_uniq⟩ : ∃! t, x_ext.IsAmalgamation t :=
  (Sieve.forallYonedaIsSheaf_iff_colimit S).mpr ⟨h_colim⟩ W x_ext hx_ext

Result:
case intro.intro
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Precoherent C
W X : C
α : Type
inst✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : Limits.IsColimit (Sieve.generate (Presieve.ofArrows Y π)).arrows.cocone
x : Presieve.FamilyOfElements (yoneda.obj W) (Presieve.ofArrows Y π)
hx : x.Compatible
x_ext : Presieve.FamilyOfElements (yoneda.obj W) (Sieve.generate (Presieve.ofArrows Y π)).arrows := x.sieveExtend
hx_ext : x.sieveExtend.Compatible
S : Sieve X := Sieve.generate (Presieve.ofArrows Y π)
t : (yoneda.obj W).obj (Opposite.op X)
t_amalg : x_ext.IsAmalgamation t
t_uniq : ∀ (y : (yoneda.obj W).obj (Opposite.op X)), (fun t => x_ext.IsAmalgamation t) y → y = t
⊢ ∃! t, x.IsAmalgamation t

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Precoherent C
W X : C
α : Type
inst✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : Limits.IsColimit (Sieve.generateFamily Y π).arrows.cocone
⊢ Presieve.IsSheafFor (yoneda.obj W) (Presieve.ofArrows Y π)

Tactic:
rw [← Sieve.generateFamily_eq] at h_colim

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Precoherent C
W X : C
α : Type
inst✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : Limits.IsColimit (Sieve.generate (Presieve.ofArrows Y π)).arrows.cocone
⊢ Presieve.IsSheafFor (yoneda.obj W) (Presieve.ofArrows Y π)

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Precoherent C
W X : C
α : Type
inst✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : Limits.IsColimit (Sieve.generate (Presieve.ofArrows Y π)).arrows.cocone
x : Presieve.FamilyOfElements (yoneda.obj W) (Presieve.ofArrows Y π)
hx : x.Compatible
⊢ ∃! t, x.IsAmalgamation t

Tactic:
let x_ext := Presieve.FamilyOfElements.sieveExtend x

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Precoherent C
W X : C
α : Type
inst✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : Limits.IsColimit (Sieve.generate (Presieve.ofArrows Y π)).arrows.cocone
x : Presieve.FamilyOfElements (yoneda.obj W) (Presieve.ofArrows Y π)
hx : x.Compatible
x_ext : Presieve.FamilyOfElements (yoneda.obj W) (Sieve.generate (Presieve.ofArrows Y π)).arrows := x.sieveExtend
⊢ ∃! t, x.IsAmalgamation t

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Precoherent C
W : C
⊢ ∀ (B : C) (α : Type) [inst : Finite α] (X : α → C) (π : (a : α) → X a ⟶ B),
    EffectiveEpiFamily X π → Presieve.IsSheafFor (yoneda.obj W) (Presieve.ofArrows X π)

Tactic:
intro X α _ Y π H

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Precoherent C
W X : C
α : Type
inst✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
⊢ Presieve.IsSheafFor (yoneda.obj W) (Presieve.ofArrows Y π)

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Precoherent C
W X : C
α : Type
inst✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : Limits.IsColimit (Sieve.generate (Presieve.ofArrows Y π)).arrows.cocone
x : Presieve.FamilyOfElements (yoneda.obj W) (Presieve.ofArrows Y π)
hx : x.Compatible
x_ext : Presieve.FamilyOfElements (yoneda.obj W) (Sieve.generate (Presieve.ofArrows Y π)).arrows := x.sieveExtend
⊢ ∃! t, x.IsAmalgamation t

Tactic:
have hx_ext := Presieve.FamilyOfElements.Compatible.sieveExtend hx

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Precoherent C
W X : C
α : Type
inst✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : Limits.IsColimit (Sieve.generate (Presieve.ofArrows Y π)).arrows.cocone
x : Presieve.FamilyOfElements (yoneda.obj W) (Presieve.ofArrows Y π)
hx : x.Compatible
x_ext : Presieve.FamilyOfElements (yoneda.obj W) (Sieve.generate (Presieve.ofArrows Y π)).arrows := x.sieveExtend
hx_ext : x.sieveExtend.Compatible
⊢ ∃! t, x.IsAmalgamation t