awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sheaves.PUnit
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf.{w, v, u} C X
it : IsTerminal.{v, u} (F.obj (op ⊥))
c : C
this : IndiscreteTopology.{w} (↑X : Type w)
s : Sieve (C := TopologicalSpace.Opens (↑X : Type w)) ⊥
hs :
  Membership.mem (γ := Set (Sieve (C := TopologicalSpace.Opens (↑X : Type w)) ⊥))
    ((Opens.grothendieckTopology (↑X : Type w) : (a : TopologicalSpace.Opens (↑X : Type w)) → Set (Sieve a)) ⊥) s
x : Presieve.FamilyOfElements (F ⋙ Functor.obj coyoneda (op c)) s.arrows
inl :
  x.Compatible (R := s.arrows) → ∃! t : (F ⋙ Functor.obj coyoneda (op c)).obj (op ⊥), x.IsAmalgamation (R := s.arrows) t
⊢ x.Compatible (R := s.arrows) → ∃! t : (F ⋙ Functor.obj coyoneda (op c)).obj (op ⊥), x.IsAmalgamation (R := s.arrows) t

Tactic:
_
-- Module: Mathlib.Topology.Sheaves.PUnit
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf.{w, v, u} C X
it : IsTerminal.{v, u} (F.obj (op ⊥))
c : C
this : IndiscreteTopology.{w} (↑X : Type w)
s : Sieve (C := TopologicalSpace.Opens (↑X : Type w)) ⊥
hs :
  Membership.mem (γ := Set (Sieve (C := TopologicalSpace.Opens (↑X : Type w)) ⊥))
    ((Opens.grothendieckTopology (↑X : Type w) : (a : TopologicalSpace.Opens (↑X : Type w)) → Set (Sieve a)) ⊥) s
x : Presieve.FamilyOfElements (F ⋙ Functor.obj coyoneda (op c)) s.arrows
h : x.Compatible (R := s.arrows)
inl : ∃ (x_1 : (F ⋙ Functor.obj coyoneda (op c)).obj (op ⊥)), x.IsAmalgamation (R := s.arrows) x_1
rw : ∀ (x x_1 : (F ⋙ Functor.obj coyoneda (op c)).obj (op ⊥)), x = x_1
⊢ ∃! t : (F ⋙ Functor.obj coyoneda (op c)).obj (op ⊥), x.IsAmalgamation (R := s.arrows) t

Tactic:
rw [@existsUnique_iff_exists _ ⟨fun _ _ => _⟩]

Premises used: existsUnique_iff_exists
-- Module: Mathlib.Topology.Sheaves.PUnit
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf.{w, v, u} C X
it : IsTerminal.{v, u} (F.obj (op ⊥))
c : C
this : IndiscreteTopology.{w} (↑X : Type w)
s : Sieve (C := TopologicalSpace.Opens (↑X : Type w)) ⊥
hs :
  Membership.mem (γ := Set (Sieve (C := TopologicalSpace.Opens (↑X : Type w)) ⊥))
    ((Opens.grothendieckTopology (↑X : Type w) : (a : TopologicalSpace.Opens (↑X : Type w)) → Set (Sieve a)) ⊥) s
x : Presieve.FamilyOfElements (F ⋙ Functor.obj coyoneda (op c)) s.arrows
h : x.Compatible (R := s.arrows)
⊢ ∃ (x_1 : (F ⋙ Functor.obj coyoneda (op c)).obj (op ⊥)), x.IsAmalgamation (R := s.arrows) x_1

Tactic:
⟨it.from _, fun U hU hs => IsTerminal.hom_ext ?_ _ _⟩

Premises used: CategoryTheory.Limits.IsTerminal.from, CategoryTheory.coyoneda, CategoryTheory.ConcreteCategory.hom, Quiver.Hom.op, CategoryTheory.Functor.comp, CategoryTheory.Functor.map, Opposite.op, Exists.intro, CategoryTheory.Limits.IsTerminal.hom_ext, DFunLike.coe, Opposite.unop, CategoryTheory.Functor.obj
-- Module: Mathlib.Topology.Sheaves.PUnit
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf.{w, v, u} C X
it : IsTerminal.{v, u} (F.obj (op ⊥))
c : C
this : IndiscreteTopology.{w} (↑X : Type w)
s : Sieve (C := TopologicalSpace.Opens (↑X : Type w)) ⊥
hs :
  Membership.mem (γ := Set (Sieve (C := TopologicalSpace.Opens (↑X : Type w)) ⊥))
    ((Opens.grothendieckTopology (↑X : Type w) : (a : TopologicalSpace.Opens (↑X : Type w)) → Set (Sieve a)) ⊥) s
x : Presieve.FamilyOfElements (F ⋙ Functor.obj coyoneda (op c)) s.arrows
h : x.Compatible (R := s.arrows)
inl : (U : TopologicalSpace.Opens (↑X : Type w)) → (hU : U ⟶ ⊥) → (hs : s.arrows hU) → IsTerminal.{v, u} (F.obj (op U))
⊢ ∃ (x_1 : (F ⋙ Functor.obj coyoneda (op c)).obj (op ⊥)), x.IsAmalgamation (R := s.arrows) x_1

Tactic:
refine ⟨it.from _, fun U hU hs => IsTerminal.hom_ext ?_ _ _⟩
-- Module: Mathlib.Topology.Sheaves.PUnit
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf.{w, v, u} C X
it : IsTerminal.{v, u} (F.obj (op ⊥))
c : C
this : IndiscreteTopology.{w} (↑X : Type w)
s : Sieve (C := TopologicalSpace.Opens (↑X : Type w)) ⊥
hs_1 :
  Membership.mem (γ := Set (Sieve (C := TopologicalSpace.Opens (↑X : Type w)) ⊥))
    ((Opens.grothendieckTopology (↑X : Type w) : (a : TopologicalSpace.Opens (↑X : Type w)) → Set (Sieve a)) ⊥) s
x : Presieve.FamilyOfElements (F ⋙ Functor.obj coyoneda (op c)) s.arrows
h : x.Compatible (R := s.arrows)
U : TopologicalSpace.Opens (↑X : Type w)
hU : U ⟶ ⊥
hs : s.arrows hU
inl inl₁ inl₂ inl₃ : IsTerminal.{v, u} (F.obj (op ⊥))
⊢ IsTerminal.{v, u} (F.obj (op U))

Tactic:
rwa [le_bot_iff.1 hU.le]

Premises used: le_bot_iff, Quiver.Hom.le, Iff.mp
-- Module: Mathlib.Topology.Sheaves.PUnit
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf.{w, v, u} C X
it : IsTerminal.{v, u} (F.obj (op ⊥))
c : C
this : IndiscreteTopology.{w} (↑X : Type w)
s : Sieve (C := TopologicalSpace.Opens (↑X : Type w)) ⊥
hs :
  Membership.mem (γ := Set (Sieve (C := TopologicalSpace.Opens (↑X : Type w)) ⊥))
    ((Opens.grothendieckTopology (↑X : Type w) : (a : TopologicalSpace.Opens (↑X : Type w)) → Set (Sieve a)) ⊥) s
x : Presieve.FamilyOfElements (F ⋙ Functor.obj coyoneda (op c)) s.arrows
h : x.Compatible (R := s.arrows)
⊢ ∀ (x x_1 : (F ⋙ Functor.obj coyoneda (op c)).obj (op ⊥)), x = x_1

Tactic:
apply it.hom_ext

Premises used: CategoryTheory.Limits.IsTerminal.hom_ext
-- Module: Mathlib.Topology.Sheaves.PUnit
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf.{w, v, u} C X
it : IsTerminal.{v, u} (F.obj (op ⊥))
c : C
U : TopologicalSpace.Opens (↑X : Type w)
s : Sieve U
hs : s ∈ (Opens.grothendieckTopology (↑X : Type w) : (a : TopologicalSpace.Opens (↑X : Type w)) → Set (Sieve a)) U
this : IndiscreteTopology.{w} (↑X : Type w)
hne : U ≠ ⊥
⊢ Presieve.IsSheafFor (X := U) (F ⋙ Functor.obj coyoneda (op c)) ⊤

Tactic:
Presieve.isSheafFor_top (F ⋙ coyoneda.obj (@op C c))

Premises used: CategoryTheory.coyoneda, CategoryTheory.Functor.comp, Opposite.op, CategoryTheory.Presieve.isSheafFor_top, CategoryTheory.Functor.obj
-- Module: Mathlib.Topology.Sheaves.PUnit
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf.{w, v, u} C X
it : IsTerminal.{v, u} (F.obj (op ⊥))
c : C
U : TopologicalSpace.Opens (↑X : Type w)
s : Sieve U
hs : s ∈ (Opens.grothendieckTopology (↑X : Type w) : (a : TopologicalSpace.Opens (↑X : Type w)) → Set (Sieve a)) U
this : IndiscreteTopology.{w} (↑X : Type w)
hne : U ≠ ⊥
h : s.arrows = ⊤
⊢ Presieve.IsSheafFor (F ⋙ Functor.obj coyoneda (op c)) s.arrows

Tactic:
convert! Presieve.isSheafFor_top (F ⋙ coyoneda.obj (@op C c))

Premises used: CategoryTheory.coyoneda, CategoryTheory.Functor.comp, Opposite.op, CategoryTheory.Presieve.isSheafFor_top, CategoryTheory.Functor.obj
-- Module: Mathlib.Topology.Sheaves.PUnit
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf.{w, v, u} C X
it : IsTerminal.{v, u} (F.obj (op ⊥))
c : C
U : TopologicalSpace.Opens (↑X : Type w)
s : Sieve U
hs : s ∈ (Opens.grothendieckTopology (↑X : Type w) : (a : TopologicalSpace.Opens (↑X : Type w)) → Set (Sieve a)) U
this : IndiscreteTopology.{w} (↑X : Type w)
hne : U ≠ ⊥
h : s.arrows (𝟙 U)
⊢ s.arrows = ⊤

Tactic:
rw [Sieve.arrows_eq_top_iff, ← Sieve.id_mem_iff_eq_top]

Premises used: CategoryTheory.Sieve.arrows_eq_top_iff, CategoryTheory.Sieve.id_mem_iff_eq_top
-- Module: Mathlib.Topology.Sheaves.PUnit
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf.{w, v, u} C X
it : IsTerminal.{v, u} (F.obj (op ⊥))
c : C
U : TopologicalSpace.Opens (↑X : Type w)
s : Sieve U
hs : s ∈ (Opens.grothendieckTopology (↑X : Type w) : (a : TopologicalSpace.Opens (↑X : Type w)) → Set (Sieve a)) U
this : IndiscreteTopology.{w} (↑X : Type w)
hne : U ≠ ⊥
⊢ U = ⊤

Tactic:
have := U.eq_bot_or_top.resolve_left hne
-- Module: Mathlib.Topology.Sheaves.PUnit
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf.{w, v, u} C X
it : IsTerminal.{v, u} (F.obj (op ⊥))
c : C
U : TopologicalSpace.Opens (↑X : Type w)
s : Sieve U
hs : s ∈ (Opens.grothendieckTopology (↑X : Type w) : (a : TopologicalSpace.Opens (↑X : Type w)) → Set (Sieve a)) U
this_1 : IndiscreteTopology.{w} (↑X : Type w)
hne : U ≠ ⊥
this : U = ⊤
h :
  ∀ (s : Sieve (C := TopologicalSpace.Opens (↑X : Type w)) ⊤)
    (hs :
      Membership.mem (γ := Set (Sieve (C := TopologicalSpace.Opens (↑X : Type w)) ⊤))
        ((Opens.grothendieckTopology (↑X : Type w) : (a : TopologicalSpace.Opens (↑X : Type w)) → Set (Sieve a)) ⊤) s)
    (hne : Ne.{w + 1} (α := TopologicalSpace.Opens (↑X : Type w)) ⊤ ⊥), s.arrows (𝟙 ⊤)
⊢ s.arrows (𝟙 U)

Tactic:
subst this
-- Module: Mathlib.Topology.Sheaves.PUnit
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf.{w, v, u} C X
it : IsTerminal.{v, u} (F.obj (op ⊥))
c : C
this : IndiscreteTopology.{w} (↑X : Type w)
s : Sieve (C := TopologicalSpace.Opens (↑X : Type w)) ⊤
hs :
  Membership.mem (γ := Set (Sieve (C := TopologicalSpace.Opens (↑X : Type w)) ⊤))
    ((Opens.grothendieckTopology (↑X : Type w) : (a : TopologicalSpace.Opens (↑X : Type w)) → Set (Sieve a)) ⊤) s
hne : Ne.{w + 1} (α := TopologicalSpace.Opens (↑X : Type w)) ⊤ ⊥
h : ∀ (he : IsEmpty.{w + 1} (↑X : Type w)), s.arrows (𝟙 ⊤)
h₁ : ∀ (x : (↑X : Type w)), s.arrows (𝟙 ⊤)
⊢ s.arrows (𝟙 ⊤)

Tactic:
obtain he | ⟨⟨x⟩⟩ := isEmpty_or_nonempty X

Premises used: isEmpty_or_nonempty, TopCat.carrier
-- Module: Mathlib.Topology.Sheaves.PUnit
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf.{w, v, u} C X
it : IsTerminal.{v, u} (F.obj (op ⊥))
c : C
this : IndiscreteTopology.{w} (↑X : Type w)
s : Sieve (C := TopologicalSpace.Opens (↑X : Type w)) ⊤
hs :
  Membership.mem (γ := Set (Sieve (C := TopologicalSpace.Opens (↑X : Type w)) ⊤))
    ((Opens.grothendieckTopology (↑X : Type w) : (a : TopologicalSpace.Opens (↑X : Type w)) → Set (Sieve a)) ⊤) s
hne : Ne.{w + 1} (α := TopologicalSpace.Opens (↑X : Type w)) ⊤ ⊥
he : IsEmpty.{w + 1} (↑X : Type w)
⊢ s.arrows (𝟙 ⊤)

Tactic:
(hne <| SetLike.ext'_iff.2 <| Set.univ_eq_empty_iff.2 he).elim

Premises used: Iff.mpr, False.elim, Set.univ_eq_empty_iff, SetLike.ext'_iff
-- Module: Mathlib.Topology.Sheaves.PUnit
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf.{w, v, u} C X
it : IsTerminal.{v, u} (F.obj (op ⊥))
c : C
this : IndiscreteTopology.{w} (↑X : Type w)
s : Sieve (C := TopologicalSpace.Opens (↑X : Type w)) ⊤
hs :
  Membership.mem (γ := Set (Sieve (C := TopologicalSpace.Opens (↑X : Type w)) ⊤))
    ((Opens.grothendieckTopology (↑X : Type w) : (a : TopologicalSpace.Opens (↑X : Type w)) → Set (Sieve a)) ⊤) s
hne : Ne.{w + 1} (α := TopologicalSpace.Opens (↑X : Type w)) ⊤ ⊥
he : IsEmpty.{w + 1} (↑X : Type w)
⊢ s.arrows (𝟙 ⊤)

Tactic:
exact (hne <| SetLike.ext'_iff.2 <| Set.univ_eq_empty_iff.2 he).elim

Premises used: Iff.mpr, False.elim, Set.univ_eq_empty_iff, SetLike.ext'_iff
-- Module: Mathlib.Topology.Sheaves.PUnit
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf.{w, v, u} C X
it : IsTerminal.{v, u} (F.obj (op ⊥))
c : C
this : IndiscreteTopology.{w} (↑X : Type w)
s : Sieve (C := TopologicalSpace.Opens (↑X : Type w)) ⊤
hs :
  Membership.mem (γ := Set (Sieve (C := TopologicalSpace.Opens (↑X : Type w)) ⊤))
    ((Opens.grothendieckTopology (↑X : Type w) : (a : TopologicalSpace.Opens (↑X : Type w)) → Set (Sieve a)) ⊤) s
hne : Ne.{w + 1} (α := TopologicalSpace.Opens (↑X : Type w)) ⊤ ⊥
x : (↑X : Type w)
h : ∀ (U : TopologicalSpace.Opens (↑X : Type w)) (f : U ⟶ ⊤) (hf : s.arrows f) (hm : x ∈ U), s.arrows (𝟙 ⊤)
⊢ s.arrows (𝟙 ⊤)

Tactic:
obtain ⟨U, f, hf, hm⟩ := hs x _root_.trivial

Premises used: trivial
-- Module: Mathlib.Topology.Sheaves.PUnit
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf.{w, v, u} C X
it : IsTerminal.{v, u} (F.obj (op ⊥))
c : C
this : IndiscreteTopology.{w} (↑X : Type w)
s : Sieve (C := TopologicalSpace.Opens (↑X : Type w)) ⊤
hs :
  Membership.mem (γ := Set (Sieve (C := TopologicalSpace.Opens (↑X : Type w)) ⊤))
    ((Opens.grothendieckTopology (↑X : Type w) : (a : TopologicalSpace.Opens (↑X : Type w)) → Set (Sieve a)) ⊤) s
hne : Ne.{w + 1} (α := TopologicalSpace.Opens (↑X : Type w)) ⊤ ⊥
x : (↑X : Type w)
U : TopologicalSpace.Opens (↑X : Type w)
f : U ⟶ ⊤
hf : s.arrows f
hm : x ∈ U
h :
  ∀ (f : Quiver.Hom (V := TopologicalSpace.Opens (↑X : Type w)) ⊥ ⊤) (hf : s.arrows f)
    (hm : Membership.mem (γ := TopologicalSpace.Opens (↑X : Type w)) ⊥ x), s.arrows (𝟙 ⊤)
h₁ :
  ∀ (f : Quiver.Hom (V := TopologicalSpace.Opens (↑X : Type w)) ⊤ ⊤) (hf : s.arrows f)
    (hm : Membership.mem (γ := TopologicalSpace.Opens (↑X : Type w)) ⊤ x), s.arrows (𝟙 ⊤)
⊢ s.arrows (𝟙 ⊤)

Tactic:
obtain rfl | rfl := U.eq_bot_or_top

Premises used: TopologicalSpace.Opens.eq_bot_or_top, rfl
-- Module: Mathlib.Topology.Sheaves.PUnit
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf.{w, v, u} C X
it : IsTerminal.{v, u} (F.obj (op ⊥))
c : C
this : IndiscreteTopology.{w} (↑X : Type w)
s : Sieve (C := TopologicalSpace.Opens (↑X : Type w)) ⊤
hs :
  Membership.mem (γ := Set (Sieve (C := TopologicalSpace.Opens (↑X : Type w)) ⊤))
    ((Opens.grothendieckTopology (↑X : Type w) : (a : TopologicalSpace.Opens (↑X : Type w)) → Set (Sieve a)) ⊤) s
hne : Ne.{w + 1} (α := TopologicalSpace.Opens (↑X : Type w)) ⊤ ⊥
x : (↑X : Type w)
f : Quiver.Hom (V := TopologicalSpace.Opens (↑X : Type w)) ⊥ ⊤
hf : s.arrows f
hm : Membership.mem (γ := TopologicalSpace.Opens (↑X : Type w)) ⊥ x
⊢ s.arrows (𝟙 ⊤)

Tactic:
cases hm
-- Module: Mathlib.Topology.Sheaves.PUnit
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf.{w, v, u} C X
it : IsTerminal.{v, u} (F.obj (op ⊥))
c : C
this : IndiscreteTopology.{w} (↑X : Type w)
s : Sieve (C := TopologicalSpace.Opens (↑X : Type w)) ⊤
hs :
  Membership.mem (γ := Set (Sieve (C := TopologicalSpace.Opens (↑X : Type w)) ⊤))
    ((Opens.grothendieckTopology (↑X : Type w) : (a : TopologicalSpace.Opens (↑X : Type w)) → Set (Sieve a)) ⊤) s
hne : Ne.{w + 1} (α := TopologicalSpace.Opens (↑X : Type w)) ⊤ ⊥
x : (↑X : Type w)
f : Quiver.Hom (V := TopologicalSpace.Opens (↑X : Type w)) ⊤ ⊤
hf : s.arrows f
hm : Membership.mem (γ := TopologicalSpace.Opens (↑X : Type w)) ⊤ x
⊢ s.arrows f

Tactic:
hf
-- Module: Mathlib.Topology.Sheaves.PUnit
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf.{w, v, u} C X
it : IsTerminal.{v, u} (F.obj (op ⊥))
c : C
this : IndiscreteTopology.{w} (↑X : Type w)
s : Sieve (C := TopologicalSpace.Opens (↑X : Type w)) ⊤
hs :
  Membership.mem (γ := Set (Sieve (C := TopologicalSpace.Opens (↑X : Type w)) ⊤))
    ((Opens.grothendieckTopology (↑X : Type w) : (a : TopologicalSpace.Opens (↑X : Type w)) → Set (Sieve a)) ⊤) s
hne : Ne.{w + 1} (α := TopologicalSpace.Opens (↑X : Type w)) ⊤ ⊥
x : (↑X : Type w)
f : Quiver.Hom (V := TopologicalSpace.Opens (↑X : Type w)) ⊤ ⊤
hf : s.arrows f
hm : Membership.mem (γ := TopologicalSpace.Opens (↑X : Type w)) ⊤ x
⊢ s.arrows (𝟙 ⊤)

Tactic:
convert! hf
-- Module: Mathlib.Topology.Sheaves.PUnit
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf.{w, v, u} C X
⊢ F.IsSheaf ↔ Nonempty (IsTerminal.{v, u} (F.obj (op ⊥)))

Tactic:
⟨fun h => ⟨Sheaf.isTerminalOfEmpty ⟨F, h⟩⟩, fun ⟨it⟩ =>
    isSheaf_of_isTerminal_of_indiscrete hind F it⟩

Premises used: TopCat.Presheaf.isSheaf_of_isTerminal_of_indiscrete, CategoryTheory.ObjectProperty.FullSubcategory.mk, TopCat.Sheaf.isTerminalOfEmpty, TopCat.Presheaf.IsSheaf, _private.0.TopCat.Presheaf.isSheaf_iff_isTerminal_of_indiscrete.match_1, Nonempty.intro, Iff.intro
-- Module: Mathlib.Topology.Sheaves.PUnit
Goal:
C : Type u
inst : Category.{v, u} C
F : Presheaf.{u_1, v, u} C (of PUnit.{u_1 + 1})
it : IsTerminal.{v, u} (F.obj (op ⊥))
⊢ F.IsSheaf

Tactic:
isSheaf_of_isTerminal_of_indiscrete (@Subsingleton.elim (TopologicalSpace PUnit) _ _ _) F it

Premises used: TopCat.Presheaf.isSheaf_of_isTerminal_of_indiscrete
-- Module: Mathlib.Topology.Sheaves.PUnit
Goal:
C : Type u
inst : Category.{v, u} C
F : Presheaf.{u_1, v, u} C (of PUnit.{u_1 + 1})
⊢ F.IsSheaf ↔ Nonempty (IsTerminal.{v, u} (F.obj (op ⊥)))

Tactic:
⟨fun h => ⟨Sheaf.isTerminalOfEmpty ⟨F, h⟩⟩, fun ⟨it⟩ => isSheaf_on_punit_of_isTerminal F it⟩

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.mk, TopCat.Sheaf.isTerminalOfEmpty, _private.0.TopCat.Presheaf.isSheaf_on_punit_iff_isTerminal.match_1, TopCat.Presheaf.IsSheaf, Nonempty.intro, TopCat.Presheaf.isSheaf_on_punit_of_isTerminal, Iff.intro
-- Module: Mathlib.Topology.Sheaves.Points
Goal:
X : Type u
inst : TopologicalSpace X
x : X
U : Opens X
hU : x ∈ U
V : Opens X
hV : x ∈ V
⊢ Sigma.fst (β := fun (c : Opens X) ↦
      Functor.obj
        { obj := fun (U : Opens X) ↦ ULift.{u, 0} (PLift (x ∈ U)),
          map := fun {X_1 Y : Opens X} (f : X_1 ⟶ Y) ↦
            ↾fun (h : ULift.{u, 0} (PLift (x ∈ X_1))) ↦
              { down := { down := ⋯ : PLift (x ∈ Y) } : ULift.{u, 0} (PLift (x ∈ Y)) },
          map_id := ⋯, map_comp := ⋯ : Opens X ⥤ Type u }
        c)
      (Sigma.mk (β := fun (c : Opens X) ↦
        Functor.obj
          { obj := fun (U : Opens X) ↦ ULift.{u, 0} (PLift (x ∈ U)),
            map := fun {X_1 Y : Opens X} (f : X_1 ⟶ Y) ↦
              ↾fun (h : ULift.{u, 0} (PLift (x ∈ X_1))) ↦
                { down := { down := ⋯ : PLift (x ∈ Y) } : ULift.{u, 0} (PLift (x ∈ Y)) },
            map_id := ⋯, map_comp := ⋯ : Opens X ⥤ Type u }
          c)
        (U ⊓ V) { down := { down := ⋯ : PLift (x ∈ U ⊓ V) } : ULift.{u, 0} (PLift (x ∈ U ⊓ V)) }) ≤
    Sigma.fst (β := fun (c : Opens X) ↦
      Functor.obj
        { obj := fun (U : Opens X) ↦ ULift.{u, 0} (PLift (x ∈ U)),
          map := fun {X_1 Y : Opens X} (f : X_1 ⟶ Y) ↦
            ↾fun (h : ULift.{u, 0} (PLift (x ∈ X_1))) ↦ { down := { down := ⋯ } },
          map_id := ⋯, map_comp := ⋯ }
        c)
      (Sigma.mk (β := fun (c : Opens X) ↦
        Functor.obj
          { obj := fun (U : Opens X) ↦ ULift.{u, 0} (PLift (x ∈ U)),
            map := fun {X_1 Y : Opens X} (f : X_1 ⟶ Y) ↦
              ↾fun (h : ULift.{u, 0} (PLift (x ∈ X_1))) ↦ { down := { down := ⋯ } },
            map_id := ⋯, map_comp := ⋯ }
          c)
        U { down := { down := hU : PLift (x ∈ U) } : ULift.{u, 0} (PLift (x ∈ U)) })

Tactic:
simp
-- Module: Mathlib.Topology.Sheaves.Points
Goal:
X : Type u
inst : TopologicalSpace X
x : X
U : Opens X
hU : x ∈ U
V : Opens X
hV : x ∈ V
⊢ Sigma.fst (β := fun (c : Opens X) ↦
      Functor.obj
        { obj := fun (U : Opens X) ↦ ULift.{u, 0} (PLift (x ∈ U)),
          map := fun {X_1 Y : Opens X} (f : X_1 ⟶ Y) ↦
            ↾fun (h : ULift.{u, 0} (PLift (x ∈ X_1))) ↦
              { down := { down := ⋯ : PLift (x ∈ Y) } : ULift.{u, 0} (PLift (x ∈ Y)) },
          map_id := ⋯, map_comp := ⋯ : Opens X ⥤ Type u }
        c)
      (Sigma.mk (β := fun (c : Opens X) ↦
        Functor.obj
          { obj := fun (U : Opens X) ↦ ULift.{u, 0} (PLift (x ∈ U)),
            map := fun {X_1 Y : Opens X} (f : X_1 ⟶ Y) ↦
              ↾fun (h : ULift.{u, 0} (PLift (x ∈ X_1))) ↦
                { down := { down := ⋯ : PLift (x ∈ Y) } : ULift.{u, 0} (PLift (x ∈ Y)) },
            map_id := ⋯, map_comp := ⋯ : Opens X ⥤ Type u }
          c)
        (U ⊓ V) { down := { down := ⋯ : PLift (x ∈ U ⊓ V) } : ULift.{u, 0} (PLift (x ∈ U ⊓ V)) }) ≤
    Sigma.fst (β := fun (c : Opens X) ↦
      Functor.obj
        { obj := fun (U : Opens X) ↦ ULift.{u, 0} (PLift (x ∈ U)),
          map := fun {X_1 Y : Opens X} (f : X_1 ⟶ Y) ↦
            ↾fun (h : ULift.{u, 0} (PLift (x ∈ X_1))) ↦ { down := { down := ⋯ } },
          map_id := ⋯, map_comp := ⋯ }
        c)
      (Sigma.mk (β := fun (c : Opens X) ↦
        Functor.obj
          { obj := fun (U : Opens X) ↦ ULift.{u, 0} (PLift (x ∈ U)),
            map := fun {X_1 Y : Opens X} (f : X_1 ⟶ Y) ↦
              ↾fun (h : ULift.{u, 0} (PLift (x ∈ X_1))) ↦ { down := { down := ⋯ } },
            map_id := ⋯, map_comp := ⋯ }
          c)
        V { down := { down := hV : PLift (x ∈ V) } : ULift.{u, 0} (PLift (x ∈ V)) })

Tactic:
simp
-- Module: Mathlib.Topology.Sheaves.Points
Goal:
X : Type u
inst : TopologicalSpace X
x : X
U : Opens X
hU : x ∈ U
V : Opens X
hV : x ∈ V
⊢ ∃ (W :
    Functor.Elements (C := Opens X)
      { obj := fun (U : Opens X) ↦ ULift.{u, 0} (PLift (x ∈ U)),
        map := fun {X_1 Y : Opens X} (f : X_1 ⟶ Y) ↦
          ↾fun (h : ULift.{u, 0} (PLift (x ∈ X_1))) ↦ { down := { down := ⋯ } },
        map_id := ⋯, map_comp := ⋯ })
    (x_1 :
    W ⟶
      Sigma.mk (β := fun (c : Opens X) ↦
        Functor.obj
          { obj := fun (U : Opens X) ↦ ULift.{u, 0} (PLift (x ∈ U)),
            map := fun {X_1 Y : Opens X} (f : X_1 ⟶ Y) ↦
              ↾fun (h : ULift.{u, 0} (PLift (x ∈ X_1))) ↦ { down := { down := ⋯ } },
            map_id := ⋯, map_comp := ⋯ }
          c)
        U { down := { down := hU : PLift (x ∈ U) } : ULift.{u, 0} (PLift (x ∈ U)) })
    (x :
    W ⟶
      Sigma.mk (β := fun (c : Opens X) ↦
        Functor.obj
          { obj := fun (U : Opens X) ↦ ULift.{u, 0} (PLift (x ∈ U)),
            map := fun {X_1 Y : Opens X} (f : X_1 ⟶ Y) ↦
              ↾fun (h : ULift.{u, 0} (PLift (x ∈ X_1))) ↦ { down := { down := ⋯ } },
            map_id := ⋯, map_comp := ⋯ }
          c)
        V { down := { down := hV : PLift (x ∈ V) } : ULift.{u, 0} (PLift (x ∈ V)) }),
    True

Tactic:
exact ⟨⟨U ⊓ V, ⟨⟨⟨hU, hV⟩⟩⟩⟩, ⟨homOfLE (by simp), rfl⟩,
          ⟨homOfLE (by simp), rfl⟩, ⟨⟩⟩
-- Module: Mathlib.Topology.Sheaves.Points
Goal:
X : Type u
inst : TopologicalSpace X
x : X
⊢ Membership.mem (γ := Opens X) ⊤ x

Tactic:
simp
-- Module: Mathlib.Topology.Sheaves.Points
Goal:
X : Type u
inst : TopologicalSpace X
x : X
U : Opens X
R : Sieve U
hR : R ∈ (grothendieckTopology X : (a : Opens X) → Set (Sieve a)) U
hU : x ∈ U
V : Opens X
f : V ⟶ U
hf : R.arrows f
hV : x ∈ V
⊢ ∃ (Y : Opens X) (f : Y ⟶ U) (_ : R.arrows f) (y :
    Functor.obj
      { obj := fun (U : Opens X) ↦ ULift.{u, 0} (PLift (x ∈ U)),
        map := fun {X_1 Y : Opens X} (f : X_1 ⟶ Y) ↦
          ↾fun (h : ULift.{u, 0} (PLift (x ∈ X_1))) ↦ { down := { down := ⋯ } },
        map_id := ⋯, map_comp := ⋯ }
      Y),
    (ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryTheory.Functor.map
              { obj := fun (U : Opens X) ↦ ULift.{u, 0} (PLift (x ∈ U)),
                map := fun {X_1 Y : Opens X} (f : X_1 ⟶ Y) ↦
                  ↾fun (h : ULift.{u, 0} (PLift (x ∈ X_1))) ↦
                    { down := { down := ⋯ : PLift (x ∈ Y) } : ULift.{u, 0} (PLift (x ∈ Y)) },
                map_id := ⋯, map_comp := ⋯ : Opens X ⥤ Type u }
              f) :
          (a :
              (fun (X : Type u) ↦ X)
                ({ obj := fun (U : Opens X) ↦ ULift.{u, 0} (PLift (x ∈ U)),
                      map := fun {X_1 Y : Opens X} (f : X_1 ⟶ Y) ↦
                        ↾fun (h : ULift.{u, 0} (PLift (x ∈ X_1))) ↦ { down := { down := ⋯ } },
                      map_id := ⋯, map_comp := ⋯ }.obj
                  Y)) →
            (fun (X : Type u) ↦ X)
              ({ obj := fun (U : Opens X) ↦ ULift.{u, 0} (PLift (x ∈ U)),
                    map := fun {X_1 Y : Opens X} (f : X_1 ⟶ Y) ↦
                      ↾fun (h : ULift.{u, 0} (PLift (x ∈ X_1))) ↦ { down := { down := ⋯ } },
                    map_id := ⋯, map_comp := ⋯ }.obj
                U))
        y =
      { down := { down := hU : PLift (x ∈ U) } : ULift.{u, 0} (PLift (x ∈ U)) }

Tactic:
⟨_, _, hf, ⟨⟨hV⟩⟩, rfl⟩

Premises used: PLift.up, Exists.intro, ULift.up, rfl