-- 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
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
⊢ ∃! t, x.IsAmalgamation t

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

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
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
⊢ ∃! t, x.IsAmalgamation t

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
⊢ ∃! t, x.IsAmalgamation t

Tactic:
let S := Sieve.generate (Presieve.ofArrows (fun () ↦ Y) (fun () ↦ f))

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
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

Proof state:
case intro.intro.intro.intro.intro.refine_2
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
⊢ ∀ (y : (yoneda.obj W).obj (op X)), (fun t => x.IsAmalgamation t) y → y = t

Tactic:
exact fun y hy ↦ t_uniq y <| Presieve.isAmalgamation_sieveExtend x y hy

Result:
no goals

Proof state:
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

Tactic:
refine ⟨t, ?_, ?_⟩

Result:
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

case intro.intro.intro.intro.intro.refine_2
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
⊢ ∀ (y : (yoneda.obj W).obj (op X)), (fun t => x.IsAmalgamation t) y → y = t

Proof state:
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
this : S.regular
⊢ IsSheafFor (yoneda.obj W) S

Tactic:
obtain ⟨Y, f, rfl, hf⟩ := Presieve.regular.single_epi (R := S)

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
⊢ IsSheafFor (yoneda.obj W) (ofArrows (fun x => Y) fun x => f)