-- 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
s : Cocone S.arrows.diagram := S.arrows.compatibleYonedaFamily_toCocone W x hx
⊢ ∃! t, x.IsAmalgamation t

Tactic:
use H.desc s

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

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

Tactic:
exact fun g hg => H.uniq s g (fun ⟨⟨f, _, hom⟩, hf⟩ => hg hom hf)

Result:
no goals

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

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

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

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
⊢ S.arrows.cocone.ι.app f ≫ (fun s => Exists.choose ⋯) s = s.ι.app f

Tactic:
have ht := H.choose_spec.1 f.obj.hom f.property

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

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
⊢ S.arrows.cocone.ι.app f ≫ (fun s => Exists.choose ⋯) s = s.ι.app f

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
f : S.arrows.category
H : ∃! t, (S.arrows.yonedaFamilyOfElements_fromCocone s).IsAmalgamation t
⊢ 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) (m : S.arrows.cocone.pt ⟶ s.pt),
    (∀ (j : S.arrows.category), S.arrows.cocone.ι.app j ≫ m = s.ι.app j) → m = (fun s => Exists.choose ⋯) s

Tactic:
intro s Fs HFs

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
⊢ Fs = (fun s => Exists.choose ⋯) s