-- Mathlib/CategoryTheory/Sites/SheafOfTypes.lean
theorem forallYonedaIsSheaf_iff_colimit (S : Sieve X) :
    (∀ W : C, Presieve.IsSheafFor (yoneda.obj W) (S : Presieve X)) ↔
      Nonempty (IsColimit S.arrows.cocone)

Proof state:
case mpr
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
W : C
x : FamilyOfElements (yoneda.obj W) S.arrows
hx : x.Compatible
H : IsColimit S.arrows.cocone
⊢ ∃! t, x.IsAmalgamation t

Tactic:
let s := compatibleYonedaFamily_toCocone S.arrows W x hx

Result:
case mpr
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
W : C
x : FamilyOfElements (yoneda.obj W) S.arrows
hx : x.Compatible
H : IsColimit S.arrows.cocone
s : Cocone S.arrows.diagram := S.arrows.compatibleYonedaFamily_toCocone W x hx
⊢ ∃! t, x.IsAmalgamation t

Proof state:
case mpr
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
H : Nonempty (IsColimit S.arrows.cocone)
W : C
x : FamilyOfElements (yoneda.obj W) S.arrows
hx : x.Compatible
⊢ ∃! t, x.IsAmalgamation t

Tactic:
replace H := Classical.choice H

Result:
case mpr
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
W : C
x : FamilyOfElements (yoneda.obj W) S.arrows
hx : x.Compatible
H : IsColimit S.arrows.cocone
⊢ ∃! t, x.IsAmalgamation t

Proof state:
case mp
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
H : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
⊢ IsColimit S.arrows.cocone

Tactic:
exact
{ desc := fun s => H s.pt (yonedaFamilyOfElements_fromCocone S.arrows s)
    (yonedaFamily_fromCocone_compatible S s) |>.choose
  fac := by
    intro s f
    replace H := H s.pt (yonedaFamilyOfElements_fromCocone S.arrows s)
      (yonedaFamily_fromCocone_compatible S s)
    have ht := H.choose_spec.1 f.obj.hom f.property
    aesop_cat
  uniq := by
    intro s Fs HFs
    replace H := H s.pt (yonedaFamilyOfElements_fromCocone S.arrows s)
      (yonedaFamily_fromCocone_compatible S s)
    apply H.choose_spec.2 Fs
    exact fun _ f hf => HFs ⟨Over.mk f, hf⟩ }

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
H✝ : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
s : Cocone S.arrows.diagram
f : S.arrows.category
H : ∃! t, (S.arrows.yonedaFamilyOfElements_fromCocone s).IsAmalgamation t
ht : (yoneda.obj s.pt).map f.obj.hom.op (Exists.choose H) = S.arrows.yonedaFamilyOfElements_fromCocone s f.obj.hom ⋯
⊢ S.arrows.cocone.ι.app f ≫ (fun s => Exists.choose ⋯) s = s.ι.app f

Tactic:
aesop_cat

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
H✝ : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
s : Cocone S.arrows.diagram
Fs : S.arrows.cocone.pt ⟶ s.pt
HFs : ∀ (j : S.arrows.category), S.arrows.cocone.ι.app j ≫ Fs = s.ι.app j
H : ∃! t, (S.arrows.yonedaFamilyOfElements_fromCocone s).IsAmalgamation t
⊢ (S.arrows.yonedaFamilyOfElements_fromCocone s).IsAmalgamation Fs

Tactic:
exact fun _ f hf => HFs ⟨Over.mk f, hf⟩

Result:
no goals

Proof state:
case h
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
W : C
x : FamilyOfElements (yoneda.obj W) S.arrows
hx : x.Compatible
H : IsColimit S.arrows.cocone
s : Cocone S.arrows.diagram := S.arrows.compatibleYonedaFamily_toCocone W x hx
⊢ (fun t => x.IsAmalgamation t) (H.desc s) ∧
    ∀ (y : (yoneda.obj W).obj (op X)), (fun t => x.IsAmalgamation t) y → y = H.desc s

Tactic:
constructor

Result:
case h.left
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
W : C
x : FamilyOfElements (yoneda.obj W) S.arrows
hx : x.Compatible
H : IsColimit S.arrows.cocone
s : Cocone S.arrows.diagram := S.arrows.compatibleYonedaFamily_toCocone W x hx
⊢ (fun t => x.IsAmalgamation t) (H.desc s)

case h.right
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
W : C
x : FamilyOfElements (yoneda.obj W) S.arrows
hx : x.Compatible
H : IsColimit S.arrows.cocone
s : Cocone S.arrows.diagram := S.arrows.compatibleYonedaFamily_toCocone W x hx
⊢ ∀ (y : (yoneda.obj W).obj (op X)), (fun t => x.IsAmalgamation t) y → y = H.desc s

Proof state:
case h.left
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
W : C
x : FamilyOfElements (yoneda.obj W) S.arrows
hx : x.Compatible
H : IsColimit S.arrows.cocone
s : Cocone S.arrows.diagram := S.arrows.compatibleYonedaFamily_toCocone W x hx
⊢ (fun t => x.IsAmalgamation t) (H.desc s)

Tactic:
exact fun _ f hf => (H.fac s) ⟨Over.mk f, hf⟩

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
H : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
⊢ ∀ (s : Cocone S.arrows.diagram) (j : S.arrows.category),
    S.arrows.cocone.ι.app j ≫ (fun s => Exists.choose ⋯) s = s.ι.app j

Tactic:
intro s f

Result:
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
H : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
s : Cocone S.arrows.diagram
f : S.arrows.category
⊢ S.arrows.cocone.ι.app f ≫ (fun s => Exists.choose ⋯) s = s.ι.app f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
H✝ : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
s : Cocone S.arrows.diagram
Fs : S.arrows.cocone.pt ⟶ s.pt
HFs : ∀ (j : S.arrows.category), S.arrows.cocone.ι.app j ≫ Fs = s.ι.app j
H : ∃! t, (S.arrows.yonedaFamilyOfElements_fromCocone s).IsAmalgamation t
⊢ Fs = (fun s => Exists.choose ⋯) s

Tactic:
apply H.choose_spec.2 Fs

Result:
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
H✝ : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
s : Cocone S.arrows.diagram
Fs : S.arrows.cocone.pt ⟶ s.pt
HFs : ∀ (j : S.arrows.category), S.arrows.cocone.ι.app j ≫ Fs = s.ι.app j
H : ∃! t, (S.arrows.yonedaFamilyOfElements_fromCocone s).IsAmalgamation t
⊢ (S.arrows.yonedaFamilyOfElements_fromCocone s).IsAmalgamation Fs

Proof state:
case mp
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
H : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
⊢ Nonempty (IsColimit S.arrows.cocone)

Tactic:
refine Nonempty.intro ?_

Result:
case mp
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
H : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
⊢ IsColimit S.arrows.cocone

Proof state:
case mpr
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
⊢ Nonempty (IsColimit S.arrows.cocone) → ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows

Tactic:
intro H W x hx

Result:
case mpr
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
H : Nonempty (IsColimit S.arrows.cocone)
W : C
x : FamilyOfElements (yoneda.obj W) S.arrows
hx : x.Compatible
⊢ ∃! t, x.IsAmalgamation t

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
H : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
s : Cocone S.arrows.diagram
Fs : S.arrows.cocone.pt ⟶ s.pt
HFs : ∀ (j : S.arrows.category), S.arrows.cocone.ι.app j ≫ Fs = s.ι.app j
⊢ Fs = (fun s => Exists.choose ⋯) s

Tactic:
replace H := H s.pt (yonedaFamilyOfElements_fromCocone S.arrows s)
  (yonedaFamily_fromCocone_compatible S s)

Result:
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
H✝ : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
s : Cocone S.arrows.diagram
Fs : S.arrows.cocone.pt ⟶ s.pt
HFs : ∀ (j : S.arrows.category), S.arrows.cocone.ι.app j ≫ Fs = s.ι.app j
H : ∃! t, (S.arrows.yonedaFamilyOfElements_fromCocone s).IsAmalgamation t
⊢ Fs = (fun s => Exists.choose ⋯) s

Proof state:
case mp
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
⊢ (∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows) → Nonempty (IsColimit S.arrows.cocone)

Tactic:
intro H

Result:
case mp
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
H : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
⊢ Nonempty (IsColimit S.arrows.cocone)