-- Mathlib/CategoryTheory/Sites/Coherent/RegularSheaves.lean
/-- Every Yoneda-presheaf is a sheaf for the regular topology. -/
lemma isSheaf_yoneda_obj [Preregular C] (W : C)  :
    Presieve.IsSheaf (regularTopology C) (yoneda.obj W)

Proof state:
case intro.intro.intro.intro.intro.refine_1
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
inst✝ : Preregular C
W X w✝ Y : C
f : Y ⟶ X
hf : EffectiveEpi f
hS : ∃ f_1, ((ofArrows (fun x => Y) fun x => f) = ofArrows (fun x => w✝) fun x => f_1) ∧ EffectiveEpi f_1
this : (ofArrows (fun x => Y) fun x => f).regular
h_colim : IsColimit (Sieve.generate (ofArrows (fun x => Y) fun x => f)).arrows.cocone
x : FamilyOfElements (yoneda.obj W) (ofArrows (fun x => Y) fun x => f)
hx : x.Compatible
x_ext : FamilyOfElements (yoneda.obj W) (Sieve.generate (ofArrows (fun x => Y) fun x => f)).arrows := x.sieveExtend
hx_ext : x.sieveExtend.Compatible
S : Sieve X :=
  Sieve.generate
    (ofArrows (fun x => Y) fun x =>
      match x with
      | PUnit.unit => f)
t : (yoneda.obj W).obj (op X)
t_amalg : x_ext.IsAmalgamation t
t_uniq : ∀ (y : (yoneda.obj W).obj (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 (fun () ↦ Y) (fun () ↦ f))) _ _ t_amalg

Result:
case h.e.h.e'_6.h.h.h
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
inst✝ : Preregular C
W X w✝ Y : C
f : Y ⟶ X
hf : EffectiveEpi f
hS : ∃ f_1, ((ofArrows (fun x => Y) fun x => f) = ofArrows (fun x => w✝) fun x => f_1) ∧ EffectiveEpi f_1
this : (ofArrows (fun x => Y) fun x => f).regular
h_colim : IsColimit (Sieve.generate (ofArrows (fun x => Y) fun x => f)).arrows.cocone
x : FamilyOfElements (yoneda.obj W) (ofArrows (fun x => Y) fun x => f)
hx : x.Compatible
x_ext : FamilyOfElements (yoneda.obj W) (Sieve.generate (ofArrows (fun x => Y) fun x => f)).arrows := x.sieveExtend
hx_ext : x.sieveExtend.Compatible
S : Sieve X :=
  Sieve.generate
    (ofArrows (fun x => Y) fun x =>
      match x with
      | PUnit.unit => f)
t : (yoneda.obj W).obj (op X)
t_amalg : x_ext.IsAmalgamation t
t_uniq : ∀ (y : (yoneda.obj W).obj (op X)), (fun t => x_ext.IsAmalgamation t) y → y = t
⊢ x = FamilyOfElements.restrict ⋯ x_ext

Proof state:
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
inst✝ : Preregular C
W : C
⊢ ∀ {X : C}, ∀ R ∈ (regularCoverage C).covering X, IsSheafFor (yoneda.obj W) R

Tactic:
intro X S ⟨_, hS⟩

Result:
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
inst✝ : Preregular C
W X : C
S : Presieve X
w✝ : C
hS : ∃ f, (S = ofArrows (fun x => w✝) fun x => f) ∧ EffectiveEpi f
⊢ IsSheafFor (yoneda.obj W) S

Proof state:
case intro.intro.intro
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
inst✝ : Preregular C
W X w✝ Y : C
f : Y ⟶ X
hf : EffectiveEpi f
hS : ∃ f_1, ((ofArrows (fun x => Y) fun x => f) = ofArrows (fun x => w✝) fun x => f_1) ∧ EffectiveEpi f_1
this : (ofArrows (fun x => Y) fun x => f).regular
h_colim : IsColimit (Sieve.generate (ofArrows (fun x => Y) fun x => f)).arrows.cocone
x : FamilyOfElements (yoneda.obj W) (ofArrows (fun x => Y) fun x => f)
hx : x.Compatible
x_ext : FamilyOfElements (yoneda.obj W) (Sieve.generate (ofArrows (fun x => Y) fun x => f)).arrows := x.sieveExtend
hx_ext : x.sieveExtend.Compatible
S : Sieve X :=
  Sieve.generate
    (ofArrows (fun x => Y) fun x =>
      match x with
      | PUnit.unit => f)
⊢ ∃! t, x.IsAmalgamation t

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

Result:
case intro.intro.intro.intro.intro
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
inst✝ : Preregular C
W X w✝ Y : C
f : Y ⟶ X
hf : EffectiveEpi f
hS : ∃ f_1, ((ofArrows (fun x => Y) fun x => f) = ofArrows (fun x => w✝) fun x => f_1) ∧ EffectiveEpi f_1
this : (ofArrows (fun x => Y) fun x => f).regular
h_colim : IsColimit (Sieve.generate (ofArrows (fun x => Y) fun x => f)).arrows.cocone
x : FamilyOfElements (yoneda.obj W) (ofArrows (fun x => Y) fun x => f)
hx : x.Compatible
x_ext : FamilyOfElements (yoneda.obj W) (Sieve.generate (ofArrows (fun x => Y) fun x => f)).arrows := x.sieveExtend
hx_ext : x.sieveExtend.Compatible
S : Sieve X :=
  Sieve.generate
    (ofArrows (fun x => Y) fun x =>
      match x with
      | PUnit.unit => f)
t : (yoneda.obj W).obj (op X)
t_amalg : x_ext.IsAmalgamation t
t_uniq : ∀ (y : (yoneda.obj W).obj (op X)), (fun t => x_ext.IsAmalgamation t) y → y = t
⊢ ∃! t, x.IsAmalgamation t

Proof state:
case h.e.h.e'_6.h.h.h
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
inst✝ : Preregular C
W X w✝ Y : C
f : Y ⟶ X
hf : EffectiveEpi f
hS : ∃ f_1, ((ofArrows (fun x => Y) fun x => f) = ofArrows (fun x => w✝) fun x => f_1) ∧ EffectiveEpi f_1
this : (ofArrows (fun x => Y) fun x => f).regular
h_colim : IsColimit (Sieve.generate (ofArrows (fun x => Y) fun x => f)).arrows.cocone
x : FamilyOfElements (yoneda.obj W) (ofArrows (fun x => Y) fun x => f)
hx : x.Compatible
x_ext : FamilyOfElements (yoneda.obj W) (Sieve.generate (ofArrows (fun x => Y) fun x => f)).arrows := x.sieveExtend
hx_ext : x.sieveExtend.Compatible
S : Sieve X :=
  Sieve.generate
    (ofArrows (fun x => Y) fun x =>
      match x with
      | PUnit.unit => f)
t : (yoneda.obj W).obj (op X)
t_amalg : x_ext.IsAmalgamation t
t_uniq : ∀ (y : (yoneda.obj W).obj (op X)), (fun t => x_ext.IsAmalgamation t) y → y = t
⊢ x = FamilyOfElements.restrict ⋯ x_ext

Tactic:
exact (Presieve.restrict_extend hx).symm

Result:
no goals

Proof state:
case intro.intro.intro
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
inst✝ : Preregular C
W X w✝ Y : C
f : Y ⟶ X
hf : EffectiveEpi f
hS : ∃ f_1, ((ofArrows (fun x => Y) fun x => f) = ofArrows (fun x => w✝) fun x => f_1) ∧ EffectiveEpi f_1
this : (ofArrows (fun x => Y) fun x => f).regular
⊢ IsSheafFor (yoneda.obj W) (ofArrows (fun x => Y) fun x => f)

Tactic:
have h_colim := isColimitOfEffectiveEpiStruct f hf.effectiveEpi.some

Result:
case intro.intro.intro
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
inst✝ : Preregular C
W X w✝ Y : C
f : Y ⟶ X
hf : EffectiveEpi f
hS : ∃ f_1, ((ofArrows (fun x => Y) fun x => f) = ofArrows (fun x => w✝) fun x => f_1) ∧ EffectiveEpi f_1
this : (ofArrows (fun x => Y) fun x => f).regular
h_colim : IsColimit (Sieve.generateSingleton f).arrows.cocone
⊢ IsSheafFor (yoneda.obj W) (ofArrows (fun x => Y) fun x => f)

Proof state:
case intro.intro.intro
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
inst✝ : Preregular C
W X w✝ Y : C
f : Y ⟶ X
hf : EffectiveEpi f
hS : ∃ f_1, ((ofArrows (fun x => Y) fun x => f) = ofArrows (fun x => w✝) fun x => f_1) ∧ EffectiveEpi f_1
this : (ofArrows (fun x => Y) fun x => f).regular
h_colim : IsColimit (Sieve.generateSingleton f).arrows.cocone
⊢ IsSheafFor (yoneda.obj W) (ofArrows (fun x => Y) fun x => f)

Tactic:
rw [← Sieve.generateSingleton_eq, ← Presieve.ofArrows_pUnit] at h_colim

Result:
case intro.intro.intro
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
inst✝ : Preregular C
W X w✝ Y : C
f : Y ⟶ X
hf : EffectiveEpi f
hS : ∃ f_1, ((ofArrows (fun x => Y) fun x => f) = ofArrows (fun x => w✝) fun x => f_1) ∧ EffectiveEpi f_1
this : (ofArrows (fun x => Y) fun x => f).regular
h_colim : IsColimit (Sieve.generate (ofArrows (fun x => Y) fun x => f)).arrows.cocone
⊢ IsSheafFor (yoneda.obj W) (ofArrows (fun x => Y) fun x => f)