awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : UniformSpace X
s : Set X
inst_1 : (𝓤 X).IsCountablyGenerated
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : l.NeBot
V : ℕ → Set (X × X)
hV : (𝓤 X).HasAntitoneBasis V
W : (n : ℕ) → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), SetRel.comp (W n) (W n) ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
t : ℕ → Set X
ht_anti : Antitone t
htl : ∀ (n : ℕ), t n ∈ l
htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n
hts : ∀ (n : ℕ), t n ⊆ s
u : (n : ℕ) → X
hu : ∀ (n : ℕ), u n ∈ t n
huc : CauchySeq u
x : X
hxs : x ∈ s
hx : Tendsto u atTop (𝓝 x)
refine : ∀ (N : ℕ), True → ball x (V N) ∈ l
⊢ ∃ x ∈ s, l ≤ 𝓝 x

Tactic:
refine ⟨x, hxs, (nhds_basis_uniformity' hV.toHasBasis).ge_iff.2 fun N _ => ?_⟩
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : UniformSpace X
s : Set X
inst_1 : (𝓤 X).IsCountablyGenerated
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : l.NeBot
V : ℕ → Set (X × X)
hV : (𝓤 X).HasAntitoneBasis V
W : (n : ℕ) → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), SetRel.comp (W n) (W n) ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
t : ℕ → Set X
ht_anti : Antitone t
htl : ∀ (n : ℕ), t n ∈ l
htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n
hts : ∀ (n : ℕ), t n ⊆ s
u : (n : ℕ) → X
hu : ∀ (n : ℕ), u n ∈ t n
huc : CauchySeq u
x : X
hxs : x ∈ s
hx : Tendsto u atTop (𝓝 x)
N : ℕ
h : True
⊢ ∃ (n : ℕ), N ≤ n ∧ u n ∈ ball x (W N)

Tactic:
((eventually_ge_atTop N).and (hx <| ball_mem_nhds x (hW N))).exists

Premises used: UniformSpace.ball_mem_nhds, Filter.Eventually.and, Filter.Eventually.exists, Filter.eventually_ge_atTop
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : UniformSpace X
s : Set X
inst_1 : (𝓤 X).IsCountablyGenerated
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : l.NeBot
V : ℕ → Set (X × X)
hV : (𝓤 X).HasAntitoneBasis V
W : (n : ℕ) → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), SetRel.comp (W n) (W n) ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
t : ℕ → Set X
ht_anti : Antitone t
htl : ∀ (n : ℕ), t n ∈ l
htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n
hts : ∀ (n : ℕ), t n ⊆ s
u : (n : ℕ) → X
hu : ∀ (n : ℕ), u n ∈ t n
huc : CauchySeq u
x : X
hxs : x ∈ s
hx : Tendsto u atTop (𝓝 x)
N : ℕ
h : True
obtain : ∀ (n : ℕ) (hNn : N ≤ n) (hn : u n ∈ ball x (W N)), ball x (V N) ∈ l
⊢ ball x (V N) ∈ l

Tactic:
obtain ⟨n, hNn, hn⟩ : ∃ n, N ≤ n ∧ u n ∈ ball x (W N) :=
    ((eventually_ge_atTop N).and (hx <| ball_mem_nhds x (hW N))).exists

Premises used: UniformSpace.ball_mem_nhds, Filter.Eventually.and, UniformSpace.ball, Filter.Eventually.exists, Filter.eventually_ge_atTop
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : UniformSpace X
s : Set X
inst_1 : (𝓤 X).IsCountablyGenerated
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : l.NeBot
V : ℕ → Set (X × X)
hV : (𝓤 X).HasAntitoneBasis V
W : (n : ℕ) → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), SetRel.comp (W n) (W n) ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
t : ℕ → Set X
ht_anti : Antitone t
htl : ∀ (n : ℕ), t n ∈ l
htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n
hts : ∀ (n : ℕ), t n ⊆ s
u : (n : ℕ) → X
hu : ∀ (n : ℕ), u n ∈ t n
huc : CauchySeq u
x : X
hxs : x ∈ s
hx : Tendsto u atTop (𝓝 x)
N : ℕ
h : True
n : ℕ
hNn : N ≤ n
hn : u n ∈ ball x (W N)
⊢ ball x (V N) ∈ l

Tactic:
mem_of_superset (htl n) fun y hy => hWV N ⟨u n, hn, htW N ?_⟩

Premises used: And.intro, Exists.intro, Filter.mem_of_superset
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : UniformSpace X
s : Set X
inst_1 : (𝓤 X).IsCountablyGenerated
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : l.NeBot
V : ℕ → Set (X × X)
hV : (𝓤 X).HasAntitoneBasis V
W : (n : ℕ) → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), SetRel.comp (W n) (W n) ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
t : ℕ → Set X
ht_anti : Antitone t
htl : ∀ (n : ℕ), t n ∈ l
htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n
hts : ∀ (n : ℕ), t n ⊆ s
u : (n : ℕ) → X
hu : ∀ (n : ℕ), u n ∈ t n
huc : CauchySeq u
x : X
hxs : x ∈ s
hx : Tendsto u atTop (𝓝 x)
N : ℕ
h : True
n : ℕ
hNn : N ≤ n
hn : u n ∈ ball x (W N)
refine : ∀ (y : X) (hy : y ∈ t n), (u n, y) ∈ t N ×ˢ t N
⊢ ball x (V N) ∈ l

Tactic:
refine mem_of_superset (htl n) fun y hy => hWV N ⟨u n, hn, htW N ?_⟩
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : UniformSpace X
s : Set X
inst_1 : (𝓤 X).IsCountablyGenerated
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : l.NeBot
V : ℕ → Set (X × X)
hV : (𝓤 X).HasAntitoneBasis V
W : (n : ℕ) → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), SetRel.comp (W n) (W n) ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
t : ℕ → Set X
ht_anti : Antitone t
htl : ∀ (n : ℕ), t n ∈ l
htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n
hts : ∀ (n : ℕ), t n ⊆ s
u : (n : ℕ) → X
hu : ∀ (n : ℕ), u n ∈ t n
huc : CauchySeq u
x : X
hxs : x ∈ s
hx : Tendsto u atTop (𝓝 x)
N : ℕ
h : True
n : ℕ
hNn : N ≤ n
hn : u n ∈ ball x (W N)
y : X
hy : y ∈ t n
⊢ (u n, y) ∈ t N ×ˢ t N

Tactic:
⟨ht_anti hNn (hu n), ht_anti hNn hy⟩

Premises used: Set.Mem, setOf, Set.prod, And.intro
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : UniformSpace X
s : Set X
inst_1 : (𝓤 X).IsCountablyGenerated
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : l.NeBot
V : ℕ → Set (X × X)
hV : (𝓤 X).HasAntitoneBasis V
W : (n : ℕ) → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), SetRel.comp (W n) (W n) ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
t : ℕ → Set X
ht_anti : Antitone t
htl : ∀ (n : ℕ), t n ∈ l
htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n
hts : ∀ (n : ℕ), t n ⊆ s
u : (n : ℕ) → X
hu : ∀ (n : ℕ), u n ∈ t n
huc : CauchySeq u
x : X
hxs : x ∈ s
hx : Tendsto u atTop (𝓝 x)
N : ℕ
h : True
n : ℕ
hNn : N ≤ n
hn : u n ∈ ball x (W N)
y : X
hy : y ∈ t n
⊢ (u n, y) ∈ t N ×ˢ t N

Tactic:
exact ⟨ht_anti hNn (hu n), ht_anti hNn hy⟩
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PseudoMetrizableSpace X
s : Set X
hs : IsSeqCompact s
⊢ IsCompact s

Tactic:
letI := pseudoMetrizableSpaceUniformity X
  haveI := pseudoMetrizableSpaceUniformity_countably_generated X
  isCompact_iff_totallyBounded_isComplete.2 ⟨hs.totallyBounded, hs.isComplete⟩

Premises used: Iff.mpr, IsSeqCompact.isComplete, isCompact_iff_totallyBounded_isComplete, And.intro, IsSeqCompact.totallyBounded
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PseudoMetrizableSpace X
s : Set X
⊢ IsCompact s ↔ IsSeqCompact s

Tactic:
⟨fun H => H.isSeqCompact, fun H => H.isCompact⟩

Premises used: IsSeqCompact.isCompact, Iff.intro, IsCompact.isSeqCompact
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PseudoMetrizableSpace X
⊢ CompactSpace X ↔ SeqCompactSpace X

Tactic:
simp only [← isCompact_univ_iff, seqCompactSpace_iff, isCompact_iff_isSeqCompact]

Premises used: isCompact_iff_isSeqCompact, isCompact_univ_iff, seqCompactSpace_iff
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s t : Closeds α
h : s.carrier = t.carrier
mk :
  ∀ (carrier : Set α) (isClosed' : IsClosed[inst] carrier)
    (h : { carrier := carrier, isClosed' := isClosed' : Closeds α }.carrier = t.carrier),
    { carrier := carrier, isClosed' := isClosed' : Closeds α } = t
⊢ s = t

Tactic:
cases s
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
t : Closeds α
carrier : Set α
isClosed' : IsClosed[inst] carrier
h : { carrier := carrier, isClosed' := isClosed' : Closeds α }.carrier = t.carrier
mk :
  ∀ (carrier_1 : Set α) (isClosed'_1 : IsClosed[inst] carrier_1)
    (h :
      { carrier := carrier, isClosed' := isClosed' : Closeds α }.carrier =
        { carrier := carrier_1, isClosed' := isClosed'_1 : Closeds α }.carrier),
    { carrier := carrier, isClosed' := isClosed' : Closeds α } = { carrier := carrier_1, isClosed' := isClosed'_1 }
⊢ { carrier := carrier, isClosed' := isClosed' : Closeds α } = t

Tactic:
cases t
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
carrier : Set α
isClosed' : IsClosed[inst] carrier
carrier_1 : Set α
isClosed'_1 : IsClosed[inst] carrier_1
h :
  { carrier := carrier, isClosed' := isClosed' : Closeds α }.carrier =
    { carrier := carrier_1, isClosed' := isClosed'_1 : Closeds α }.carrier
⊢ { carrier := carrier, isClosed' := isClosed' : Closeds α } = { carrier := carrier_1, isClosed' := isClosed'_1 }

Tactic:
congr
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
s : Closeds α
⊢ IsClosed[inst] (↑s : Set α)

Tactic:
s.isClosed'

Premises used: TopologicalSpace.Closeds.isClosed'
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
s : Closeds α
⊢ s.carrier = (↑s : Set α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
s t : Closeds α
h : (↑s : Set α) = (↑t : Set α)
⊢ s = t

Tactic:
SetLike.ext' h

Premises used: SetLike.ext'
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
s : Set α
h : IsClosed[inst] s
⊢ (↑{ carrier := s, isClosed' := h : Closeds α } : Set α) = s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
s : Set α
hs : IsClosed[inst] s
x : α
⊢ x ∈ { carrier := s, isClosed' := hs : Closeds α } ↔ x ∈ s

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
s : Set α
x : α
⊢ Membership.mem (γ := Closeds α) (Closeds.closure s) x ↔ x ∈ closure[inst] s

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, closure, Set.sInter
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
⊢ GaloisConnection (β := Closeds α) Closeds.closure SetLike.coe

Tactic:
fun _ U =>
  ⟨subset_closure.trans, fun h => closure_minimal h U.isClosed⟩

Premises used: TopologicalSpace.Closeds.isClosed, subset_closure, closure_minimal, HasSubset.Subset.trans, Iff.intro, GaloisConnection
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
s : Set α
t : Closeds α
⊢ Closeds.closure s ≤ t ↔ s ⊆ (↑t : Set α)

Tactic:
t.isClosed.closure_subset_iff

Premises used: TopologicalSpace.Closeds.isClosed, Set.Mem, setOf, Set.Subset, IsClosed.closure_subset_iff, closure, Set.sInter
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
s t : Closeds α
⊢ (↑(s ⊔ t) : Set α) = (↑s : Set α) ∪ (↑t : Set α)

Tactic:
rfl
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
s t : Closeds α
⊢ (↑(s ⊓ t) : Set α) = (↑s : Set α) ∩ (↑t : Set α)

Tactic:
rfl

Premises used: setOf, Set.inter, rfl
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
⊢ (↑⊤ : Set α) = univ

Tactic:
rfl

Premises used: Set.univ, setOf, rfl
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
s : Closeds α
⊢ (↑s : Set α) = univ ↔ s = ⊤

Tactic:
SetLike.coe_injective.eq_iff' rfl

Premises used: Function.Injective.eq_iff', SetLike.coe_injective, rfl
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
⊢ (↑⊥ : Set α) = ∅

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
s : Closeds α
⊢ (↑s : Set α) = ∅ ↔ s = ⊥

Tactic:
SetLike.coe_injective.eq_iff' rfl

Premises used: Function.Injective.eq_iff', SetLike.coe_injective, rfl
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
s : Closeds α
⊢ (↑s : Set α).Nonempty ↔ s ≠ ⊥

Tactic:
nonempty_iff_ne_empty.trans coe_eq_empty.not

Premises used: TopologicalSpace.Closeds.coe_eq_empty, Iff.not, Set.nonempty_iff_ne_empty, Iff.trans
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
S : Set (Closeds α)
⊢ (↑(sInf S) : Set α) = ⋂ i ∈ S, (↑i : Set α)

Tactic:
rfl

Premises used: iInf, Set.iInter, setOf, rfl
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
S : Set (Closeds α)
⊢ (↑(sSup S) : Set α) = closure[inst] (⋃₀ (SetLike.coe '' S))

Tactic:
rfl
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
ι : Type u_1
α : Type u_2
inst : TopologicalSpace α
f : ι → Closeds α
s : Finset ι
⊢ (↑(s.sup f) : Set α) = s.sup (SetLike.coe ∘ f)

Tactic:
map_finset_sup (⟨⟨(↑), coe_sup⟩, coe_bot⟩ : SupBotHom (Closeds α) (Set α)) _ _

Premises used: TopologicalSpace.Closeds.coe_bot, TopologicalSpace.Closeds.coe_sup, SetLike.coe, SupHom.mk, map_finset_sup, SupBotHom.mk
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
ι : Type u_1
α : Type u_2
inst : TopologicalSpace α
f : ι → Closeds α
s : Finset ι
⊢ (↑(s.inf f) : Set α) = s.inf (SetLike.coe ∘ f)

Tactic:
map_finset_inf (⟨⟨(↑), coe_inf⟩, coe_top⟩ : InfTopHom (Closeds α) (Set α)) _ _

Premises used: map_finset_inf, InfTopHom.mk, TopologicalSpace.Closeds.coe_inf, TopologicalSpace.Closeds.coe_top, SetLike.coe, InfHom.mk
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
S : Set (Closeds α)
x : α
⊢ x ∈ sInf S ↔ ∀ s ∈ S, x ∈ s

Tactic:
mem_iInter₂

Premises used: iInf, Set.Mem, Set.iInter, setOf, Set.mem_iInter₂
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
ι : Sort u_4
x : α
s : ι → Closeds α
⊢ x ∈ iInf s ↔ ∀ (i : ι), x ∈ s i

Tactic:
simp [iInf]

Premises used: iInf
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
ι : Sort u_4
s : ι → Closeds α
h : ∀ (x : α), x ∈ (↑(⨅ (i : ι), s i) : Set α) ↔ Membership.mem (γ := Set α) (⋂ (i : ι), (↑(s i) : Set α)) x
⊢ (↑(⨅ (i : ι), s i) : Set α) = ⋂ (i : ι), (↑(s i) : Set α)

Tactic:
ext
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
ι : Sort u_4
s : ι → Closeds α
x : α
⊢ x ∈ (↑(⨅ (i : ι), s i) : Set α) ↔ Membership.mem (γ := Set α) (⋂ (i : ι), (↑(s i) : Set α)) x

Tactic:
simp
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
ι : Sort u_4
s : ι → Closeds α
h : (↑(⨅ (i : ι), s i) : Set α) = (↑{ carrier := ⋂ (i : ι), (↑(s i) : Set α), isClosed' := ⋯ } : Set α)
⊢ Eq.{u_2 + 1} (α := Closeds α) (⨅ (i : ι), s i) { carrier := ⋂ (i : ι), (↑(s i) : Set α), isClosed' := ⋯ }

Tactic:
ext1
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
ι : Sort u_4
s : ι → Closeds α
⊢ (↑(⨅ (i : ι), s i) : Set α) = (↑{ carrier := ⋂ (i : ι), (↑(s i) : Set α), isClosed' := ⋯ } : Set α)

Tactic:
simp
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
ι : Sort u_4
s : ι → Set α
h : ∀ (i : ι), IsClosed[inst] (s i)
⊢ ⨅ (i : ι), { carrier := s i, isClosed' := ⋯ } = { carrier := ⋂ (i : ι), s i, isClosed' := ⋯ : Closeds α }

Tactic:
iInf_def _

Premises used: TopologicalSpace.Closeds.iInf_def
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
a : Closeds α
s : Set (Closeds α)
⊢ (↑(⨅ b ∈ s, a ⊔ b) : Set α) = (↑(a ⊔ sInf s) : Set α)

Tactic:
simp only [coe_sup, coe_iInf, coe_sInf, Set.union_iInter₂]

Premises used: TopologicalSpace.Closeds.coe_iInf, TopologicalSpace.Closeds.coe_sup, TopologicalSpace.Closeds.coe_sInf, Set.union_iInter₂
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
inst_1 : T1Space α
x : α
⊢ Eq (α := Closeds α) { carrier := {x}, isClosed' := ⋯ } {x}

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
inst_1 : T1Space α
a b : α
⊢ Membership.mem (γ := Closeds α) {b} a ↔ a = b

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.singleton
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
inst_1 : T1Space α
⊢ Function.Injective (β := Closeds α) fun (x : α) ↦ {x}

Tactic:
.of_comp (f := SetLike.coe) Set.singleton_injective

Premises used: Set.singleton_injective, Function.Injective.of_comp
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
inst_1 : T1Space α
x y : α
⊢ Eq (α := Closeds α) {x} {y} ↔ x = y

Tactic:
singleton_injective.eq_iff

Premises used: TopologicalSpace.Closeds.singleton_injective, Function.Injective.eq_iff
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Closeds α
t : Closeds β
⊢ (↑(s ×ˢ t) : Set (α × β)) = (↑s : Set α) ×ˢ (↑t : Set β)

Tactic:
rfl

Premises used: setOf, Set.prod, rfl
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Closeds α
t : Closeds β
x : α × β
⊢ x ∈ s ×ˢ t ↔ x.1 ∈ s ∧ x.2 ∈ t

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.prod
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : T1Space α
inst_3 : T1Space β
x : α
y : β
⊢ SProd.sprod (α := Closeds α) (β := Closeds β) {x} {y} = {(x, y)}

Tactic:
Closeds.ext Set.singleton_prod_singleton

Premises used: Set.singleton_prod_singleton, TopologicalSpace.Closeds.ext
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
s : Closeds α
⊢ s.compl.compl = s

Tactic:
Closeds.ext (compl_compl (s : Set α))

Premises used: compl_compl, TopologicalSpace.Closeds.ext, SetLike.coe
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
s : Opens α
⊢ s.compl.compl = s

Tactic:
Opens.ext (compl_compl (s : Set α))

Premises used: compl_compl, TopologicalSpace.Opens.ext, SetLike.coe
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
⊢ Function.Bijective.{u_2 + 1, u_2 + 1} (α := Closeds α) compl

Tactic:
Function.bijective_iff_has_inverse.mpr ⟨Opens.compl, Closeds.compl_compl, Opens.compl_compl⟩

Premises used: Iff.mpr, TopologicalSpace.Closeds.compl_compl, Function.bijective_iff_has_inverse, And.intro, Exists.intro, TopologicalSpace.Opens.compl, TopologicalSpace.Opens.compl_compl
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
⊢ Function.Bijective.{u_2 + 1, u_2 + 1} (α := Opens α) compl

Tactic:
Function.bijective_iff_has_inverse.mpr ⟨Closeds.compl, Opens.compl_compl, Closeds.compl_compl⟩

Premises used: Iff.mpr, TopologicalSpace.Closeds.compl_compl, Function.bijective_iff_has_inverse, TopologicalSpace.Closeds.compl, And.intro, Exists.intro, TopologicalSpace.Opens.compl_compl
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Closeds α
⊢ Function.comp (α := (Opens α)ᵒᵈ) Opens.compl (⇑ofDual : (a : (Opens α)ᵒᵈ) → Opens α)
      (((⇑toDual : (a : Opens α) → (Opens α)ᵒᵈ) ∘ compl) s) =
    s

Tactic:
simp [Closeds.compl_compl]

Premises used: TopologicalSpace.Closeds.compl_compl
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : (Opens α)ᵒᵈ
⊢ Function.comp (α := Closeds α) (⇑toDual : (a : Opens α) → (Opens α)ᵒᵈ) compl
      ((Opens.compl ∘ (⇑ofDual : (a : (Opens α)ᵒᵈ) → Opens α)) s) =
    s

Tactic:
simp [Opens.compl_compl]

Premises used: TopologicalSpace.Opens.compl_compl
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : Opens α
⊢ Function.comp (α := (Closeds α)ᵒᵈ) Closeds.compl (⇑ofDual : (a : (Closeds α)ᵒᵈ) → Closeds α)
      (((⇑toDual : (a : Closeds α) → (Closeds α)ᵒᵈ) ∘ compl) s) =
    s

Tactic:
simp [Opens.compl_compl]

Premises used: TopologicalSpace.Opens.compl_compl
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : (Closeds α)ᵒᵈ
⊢ Function.comp (α := Opens α) (⇑toDual : (a : Closeds α) → (Closeds α)ᵒᵈ) compl
      ((Closeds.compl ∘ (⇑ofDual : (a : (Closeds α)ᵒᵈ) → Closeds α)) s) =
    s

Tactic:
simp [Closeds.compl_compl]

Premises used: TopologicalSpace.Closeds.compl_compl
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
inst_1 : T0Space α
s : Closeds α
hs : IsAtom s
⊢ ∃ (a : α), (↑s : Set α) = {a}

Tactic:
minimal_nonempty_closed_eq_singleton s.2 (coe_nonempty.2 hs.1) fun t hts ht ht' ↦ ?_

Premises used: Iff.mpr, TopologicalSpace.Closeds.coe_nonempty, And.left, minimal_nonempty_closed_eq_singleton, TopologicalSpace.Closeds.isClosed'
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
inst_1 : T0Space α
s : Closeds α
hs : IsAtom s
refine : ∀ (t : Set α) (hts : t ⊆ (↑s : Set α)) (ht : t.Nonempty) (ht' : IsClosed[inst] t), t = (↑s : Set α)
⊢ ∃ (a : α), (↑s : Set α) = {a}

Tactic:
refine minimal_nonempty_closed_eq_singleton s.2 (coe_nonempty.2 hs.1) fun t hts ht ht' ↦ ?_

Premises used: Iff.mpr, TopologicalSpace.Closeds.coe_nonempty, And.left, minimal_nonempty_closed_eq_singleton, TopologicalSpace.Closeds.isClosed'
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
inst_1 : T0Space α
s : Closeds α
hs : IsAtom s
t : Set α
hts : t ⊆ (↑s : Set α)
ht : t.Nonempty
ht' : IsClosed[inst] t
⊢ IsClosed[inst] t

Tactic:
ht'
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
inst_1 : T0Space α
s : Closeds α
hs : IsAtom s
t : Set α
hts : t ⊆ (↑s : Set α)
ht : t.Nonempty
ht' : IsClosed[inst] t
lift : ∀ (t : Closeds α) (hts : (↑t : Set α) ⊆ (↑s : Set α)) (ht : (↑t : Set α).Nonempty), (↑t : Set α) = (↑s : Set α)
⊢ t = (↑s : Set α)

Tactic:
lift t to Closeds α using ht'

Premises used: TopologicalSpace.Closeds
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
inst_1 : T0Space α
s : Closeds α
hs : IsAtom s
t : Closeds α
hts : (↑t : Set α) ⊆ (↑s : Set α)
ht : (↑t : Set α).Nonempty
⊢ (↑t : Set α) = (↑s : Set α)

Tactic:
SetLike.coe_injective.eq_iff.2 <| (hs.le_iff_eq <| coe_nonempty.1 ht).1 hts

Premises used: Iff.mpr, Function.Injective.eq_iff, SetLike.coe_injective, TopologicalSpace.Closeds.coe_nonempty, Iff.mp, IsAtom.le_iff_eq
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
inst_1 : T0Space α
s : Closeds α
hs : IsAtom s
t : Closeds α
hts : (↑t : Set α) ⊆ (↑s : Set α)
ht : (↑t : Set α).Nonempty
⊢ (↑t : Set α) = (↑s : Set α)

Tactic:
exact SetLike.coe_injective.eq_iff.2 <| (hs.le_iff_eq <| coe_nonempty.1 ht).1 hts

Premises used: Iff.mpr, Function.Injective.eq_iff, SetLike.coe_injective, TopologicalSpace.Closeds.coe_nonempty, Iff.mp, IsAtom.le_iff_eq
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
inst_1 : T1Space α
s : Closeds α
t : Set α
ht : IsAtom t
obtain : ∀ (x : α) (ht : IsAtom (α := Set α) {x}), (↑(Closeds.closure {x}) : Set α) = {x}
⊢ (↑(Closeds.closure t) : Set α) = t

Tactic:
obtain ⟨x, rfl⟩ := Set.isAtom_iff.1 ht

Premises used: Set.isAtom_iff, Iff.mp, rfl
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
inst_1 : T1Space α
s : Closeds α
x : α
ht : IsAtom (α := Set α) {x}
⊢ (↑(Closeds.closure {x}) : Set α) = {x}

Tactic:
closure_singleton

Premises used: setOf, closure_singleton, closure, Set.sInter
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
inst_1 : T1Space α
s : Closeds α
x : α
ht : IsAtom (α := Set α) {x}
⊢ (↑(Closeds.closure {x}) : Set α) = {x}

Tactic:
exact closure_singleton

Premises used: closure_singleton
-- Module: Mathlib.Topology.Sets.Closeds
Goal:
α : Type u_2
inst : TopologicalSpace α
inst_1 : T1Space α
s : Closeds α
⊢ IsAtom s ↔ ∃ (x : α), s = {x}

Tactic:
simp [← Closeds.isAtom_coe, Set.isAtom_iff, SetLike.ext_iff, Set.ext_iff]

Premises used: SetLike.ext_iff, Set.isAtom_iff, TopologicalSpace.Closeds.isAtom_coe, Set.ext_iff