case inl
C : Type u
inst✝ : Category C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj ⊥.op)
c : C
s : Sieve ⊥
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) ⊥
⊢ Presieve.IsSheafFor (F ⋙ coyoneda.obj c.op) s.arrows

case inr
C : Type u
inst✝ : Category C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj ⊥.op)
c : C
U : TopologicalSpace.Opens ↑X
s : Sieve U
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) U
hne : U ≠ ⊥
⊢ Presieve.IsSheafFor (F ⋙ coyoneda.obj c.op) s.arrows
C : Type u
inst✝ : Category C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj ⊥.op)
c : C
U : TopologicalSpace.Opens ↑X
s : Sieve U
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) U
⊢ Presieve.IsSheafFor (F ⋙ coyoneda.obj c.op) s.arrows
obtain rfl | hne := eq_or_ne U ⊥
case inl
C : Type u
inst✝ : Category C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj ⊥.op)
c : C
s : Sieve ⊥
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) ⊥
x✝ : Presieve.FamilyOfElements (F ⋙ coyoneda.obj c.op) s.arrows
a✝ : Presieve.FamilyOfElements.Compatible x✝
⊢ ∃! t, Presieve.FamilyOfElements.IsAmalgamation x✝ t
case inl
C : Type u
inst✝ : Category C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj ⊥.op)
c : C
s : Sieve ⊥
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) ⊥
⊢ Presieve.IsSheafFor (F ⋙ coyoneda.obj c.op) s.arrows
intro _ _
case inl
C : Type u
inst✝ : Category C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj ⊥.op)
c : C
s : Sieve ⊥
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) ⊥
x✝ : Presieve.FamilyOfElements (F ⋙ coyoneda.obj c.op) s.arrows
a✝ : Presieve.FamilyOfElements.Compatible x✝
⊢ ∃ x, Presieve.FamilyOfElements.IsAmalgamation x✝ x

C : Type u
inst✝ : Category C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj ⊥.op)
c : C
s : Sieve ⊥
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) ⊥
x✝ : Presieve.FamilyOfElements (F ⋙ coyoneda.obj c.op) s.arrows
a✝ : Presieve.FamilyOfElements.Compatible x✝
⊢ ∀ (x x_1 : (F ⋙ coyoneda.obj c.op).obj ⊥.op), x = x_1
case inl
C : Type u
inst✝ : Category C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj ⊥.op)
c : C
s : Sieve ⊥
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) ⊥
x✝ : Presieve.FamilyOfElements (F ⋙ coyoneda.obj c.op) s.arrows
a✝ : Presieve.FamilyOfElements.Compatible x✝
⊢ ∃! t, Presieve.FamilyOfElements.IsAmalgamation x✝ t
rw [@exists_unique_iff_exists _ ⟨fun _ _ => _⟩]
case inl
C : Type u
inst✝ : Category C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj ⊥.op)
c : C
s : Sieve ⊥
hs✝ : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) ⊥
x✝ : Presieve.FamilyOfElements (F ⋙ coyoneda.obj c.op) s.arrows
a✝ : Presieve.FamilyOfElements.Compatible x✝
U : TopologicalSpace.Opens ↑X
hU : U ⟶ ⊥
hs : s.arrows hU
⊢ IsTerminal (F.obj U.op)
case inl
C : Type u
inst✝ : Category C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj ⊥.op)
c : C
s : Sieve ⊥
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) ⊥
x✝ : Presieve.FamilyOfElements (F ⋙ coyoneda.obj c.op) s.arrows
a✝ : Presieve.FamilyOfElements.Compatible x✝
⊢ ∃ x, Presieve.FamilyOfElements.IsAmalgamation x✝ x
refine' ⟨it.from _, fun U hU hs => IsTerminal.hom_ext _ _ _⟩
no goals
case inl
C : Type u
inst✝ : Category C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj ⊥.op)
c : C
s : Sieve ⊥
hs✝ : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) ⊥
x✝ : Presieve.FamilyOfElements (F ⋙ coyoneda.obj c.op) s.arrows
a✝ : Presieve.FamilyOfElements.Compatible x✝
U : TopologicalSpace.Opens ↑X
hU : U ⟶ ⊥
hs : s.arrows hU
⊢ IsTerminal (F.obj U.op)
rwa [le_bot_iff.1 hU.le]
no goals
C : Type u
inst✝ : Category C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj ⊥.op)
c : C
s : Sieve ⊥
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) ⊥
x✝ : Presieve.FamilyOfElements (F ⋙ coyoneda.obj c.op) s.arrows
a✝ : Presieve.FamilyOfElements.Compatible x✝
⊢ ∀ (x x_1 : (F ⋙ coyoneda.obj c.op).obj ⊥.op), x = x_1
apply it.hom_ext
case h.e'_5.h.h.e'_4
C : Type u
inst✝ : Category C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj ⊥.op)
c : C
U : TopologicalSpace.Opens ↑X
s : Sieve U
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) U
hne : U ≠ ⊥
⊢ s = ⊤
case inr
C : Type u
inst✝ : Category C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj ⊥.op)
c : C
U : TopologicalSpace.Opens ↑X
s : Sieve U
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) U
hne : U ≠ ⊥
⊢ Presieve.IsSheafFor (F ⋙ coyoneda.obj c.op) s.arrows
convert Presieve.isSheafFor_top_sieve (F ⋙ coyoneda.obj (@op C c))
case h.e'_5.h.h.e'_4
C : Type u
inst✝ : Category C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj ⊥.op)
c : C
U : TopologicalSpace.Opens ↑X
s : Sieve U
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) U
hne : U ≠ ⊥
⊢ s.arrows (𝟙 U)
case h.e'_5.h.h.e'_4
C : Type u
inst✝ : Category C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj ⊥.op)
c : C
U : TopologicalSpace.Opens ↑X
s : Sieve U
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) U
hne : U ≠ ⊥
⊢ s = ⊤
rw [← Sieve.id_mem_iff_eq_top]
case h.e'_5.h.h.e'_4
C : Type u
inst✝ : Category C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj ⊥.op)
c : C
U : TopologicalSpace.Opens ↑X
s : Sieve U
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) U
hne : U ≠ ⊥
this : U = ⊤
⊢ s.arrows (𝟙 U)
case h.e'_5.h.h.e'_4
C : Type u
inst✝ : Category C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj ⊥.op)
c : C
U : TopologicalSpace.Opens ↑X
s : Sieve U
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) U
hne : U ≠ ⊥
⊢ s.arrows (𝟙 U)
have := (U.eq_bot_or_top hind).resolve_left hne
case h.e'_5.h.h.e'_4
C : Type u
inst✝ : Category C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj ⊥.op)
c : C
s : Sieve ⊤
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) ⊤
hne : ⊤ ≠ ⊥
⊢ s.arrows (𝟙 ⊤)
case h.e'_5.h.h.e'_4
C : Type u
inst✝ : Category C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj ⊥.op)
c : C
U : TopologicalSpace.Opens ↑X
s : Sieve U
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) U
hne : U ≠ ⊥
this : U = ⊤
⊢ s.arrows (𝟙 U)
subst this
case h.e'_5.h.h.e'_4.inl
C : Type u
inst✝ : Category C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj ⊥.op)
c : C
s : Sieve ⊤
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) ⊤
hne : ⊤ ≠ ⊥
he : IsEmpty ↑X
⊢ s.arrows (𝟙 ⊤)

case h.e'_5.h.h.e'_4.inr.intro
C : Type u
inst✝ : Category C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj ⊥.op)
c : C
s : Sieve ⊤
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) ⊤
hne : ⊤ ≠ ⊥
x : ↑X
⊢ s.arrows (𝟙 ⊤)
case h.e'_5.h.h.e'_4
C : Type u
inst✝ : Category C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj ⊥.op)
c : C
s : Sieve ⊤
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) ⊤
hne : ⊤ ≠ ⊥
⊢ s.arrows (𝟙 ⊤)
obtain he | ⟨⟨x⟩⟩ := isEmpty_or_nonempty X
case h.e'_5.h.h.e'_4.inr.intro.intro.intro.intro
C : Type u
inst✝ : Category C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj ⊥.op)
c : C
s : Sieve ⊤
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) ⊤
hne : ⊤ ≠ ⊥
x : ↑X
U : TopologicalSpace.Opens ↑X
f : U ⟶ ⊤
hf : s.arrows f
hm : x ∈ U
⊢ s.arrows (𝟙 ⊤)
case h.e'_5.h.h.e'_4.inr.intro
C : Type u
inst✝ : Category C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj ⊥.op)
c : C
s : Sieve ⊤
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) ⊤
hne : ⊤ ≠ ⊥
x : ↑X
⊢ s.arrows (𝟙 ⊤)
obtain ⟨U, f, hf, hm⟩ := hs x _root_.trivial
case h.e'_5.h.h.e'_4.inr.intro.intro.intro.intro.inl
C : Type u
inst✝ : Category C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj ⊥.op)
c : C
s : Sieve ⊤
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) ⊤
hne : ⊤ ≠ ⊥
x : ↑X
f : ⊥ ⟶ ⊤
hf : s.arrows f
hm : x ∈ ⊥
⊢ s.arrows (𝟙 ⊤)

case h.e'_5.h.h.e'_4.inr.intro.intro.intro.intro.inr
C : Type u
inst✝ : Category C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj ⊥.op)
c : C
s : Sieve ⊤
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) ⊤
hne : ⊤ ≠ ⊥
x : ↑X
f : ⊤ ⟶ ⊤
hf : s.arrows f
hm : x ∈ ⊤
⊢ s.arrows (𝟙 ⊤)
case h.e'_5.h.h.e'_4.inr.intro.intro.intro.intro
C : Type u
inst✝ : Category C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj ⊥.op)
c : C
s : Sieve ⊤
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) ⊤
hne : ⊤ ≠ ⊥
x : ↑X
U : TopologicalSpace.Opens ↑X
f : U ⟶ ⊤
hf : s.arrows f
hm : x ∈ U
⊢ s.arrows (𝟙 ⊤)
obtain rfl | rfl := U.eq_bot_or_top hind
no goals
case h.e'_5.h.h.e'_4.inl
C : Type u
inst✝ : Category C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj ⊥.op)
c : C
s : Sieve ⊤
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) ⊤
hne : ⊤ ≠ ⊥
he : IsEmpty ↑X
⊢ s.arrows (𝟙 ⊤)
exact (hne <| SetLike.ext'_iff.2 <| Set.univ_eq_empty_iff.2 he).elim
no goals
case h.e'_5.h.h.e'_4.inr.intro.intro.intro.intro.inl
C : Type u
inst✝ : Category C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj ⊥.op)
c : C
s : Sieve ⊤
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) ⊤
hne : ⊤ ≠ ⊥
x : ↑X
f : ⊥ ⟶ ⊤
hf : s.arrows f
hm : x ∈ ⊥
⊢ s.arrows (𝟙 ⊤)
cases hm
no goals
case h.e'_5.h.h.e'_4.inr.intro.intro.intro.intro.inr
C : Type u
inst✝ : Category C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj ⊥.op)
c : C
s : Sieve ⊤
hs : s ∈ GrothendieckTopology.sieves (Opens.grothendieckTopology ↑X) ⊤
hne : ⊤ ≠ ⊥
x : ↑X
f : ⊤ ⟶ ⊤
hf : s.arrows f
hm : x ∈ ⊤
⊢ s.arrows (𝟙 ⊤)
convert hf