internlm/Lean-Github huggingface dataset:
Theorem: FilterGame.Filter.mem_inf_principal_iff
Proof state before:
case heq
α : Type u_1
f : Filter α
s t : Set α
h : {x | x ∈ t → x ∈ s} ∈ f
⊢ {x | x ∈ t → x ∈ s} = tᶜ ∪ s
Tactic:
apply Set.ext
Proof state after:
case heq.h
α : Type u_1
f : Filter α
s t : Set α
h : {x | x ∈ t → x ∈ s} ∈ f
⊢ ∀ (x : α), x ∈ {x | x ∈ t → x ∈ s} ↔ x ∈ tᶜ ∪ s
Theorem: FilterGame.Filter.mem_inf_principal_iff
Proof state before:
case heq.h
α : Type u_1
f : Filter α
s t : Set α
h : {x | x ∈ t → x ∈ s} ∈ f
⊢ ∀ (x : α), x ∈ {x | x ∈ t → x ∈ s} ↔ x ∈ tᶜ ∪ s
Tactic:
intros x
Proof state after:
case heq.h
α : Type u_1
f : Filter α
s t : Set α
h : {x | x ∈ t → x ∈ s} ∈ f
x : α
⊢ x ∈ {x | x ∈ t → x ∈ s} ↔ x ∈ tᶜ ∪ s
Theorem: FilterGame.Filter.mem_inf_principal_iff
Proof state before:
case heq.h
α : Type u_1
f : Filter α
s t : Set α
h : {x | x ∈ t → x ∈ s} ∈ f
x : α
⊢ x ∈ {x | x ∈ t → x ∈ s} ↔ x ∈ tᶜ ∪ s
Tactic:
rw [Set.mem_iff, Set.mem_union, Set.mem_compl_iff, imp_iff_not_or]
Proof state after:
no goals
Theorem: FilterGame.Filter.mem_inf_principal_iff
Proof state before:
case heq
α : Type u_1
f : Filter α
s t : Set α
h : tᶜ ∪ s ∈ f
⊢ s = (tᶜ ∪ s) ∩ (t ∪ s)
Tactic:
rw [← Set.union_distrib_right, Set.compl_inter_self, Set.empty_union]
Proof state after:
no goals
Theorem: FilterGame.Basis.as_filter_le
Proof state before:
α : Type u_1
b c : Basis α
h : ∀ (s : Set α), s ∈ c → ∃ t, t ∈ b ∧ t ⊆ s
⊢ as_filter b ≤ as_filter c
Tactic:
intros s hs
Proof state after:
α : Type u_1
b c : Basis α
h : ∀ (s : Set α), s ∈ c → ∃ t, t ∈ b ∧ t ⊆ s
s : Set α
hs : s ∈ as_filter c
⊢ s ∈ as_filter b
Theorem: FilterGame.Basis.as_filter_le
Proof state before:
α : Type u_1
b c : Basis α
h : ∀ (s : Set α), s ∈ c → ∃ t, t ∈ b ∧ t ⊆ s
s : Set α
hs : s ∈ as_filter c
⊢ s ∈ as_filter b
Tactic:
have ⟨t, ht⟩ := hs
Proof state after:
α : Type u_1
b c : Basis α
h : ∀ (s : Set α), s ∈ c → ∃ t, t ∈ b ∧ t ⊆ s
s : Set α
hs : s ∈ as_filter c
t : Set α
ht : t ∈ c ∧ t ⊆ s
⊢ s ∈ as_filter b
Theorem: FilterGame.Basis.as_filter_le
Proof state before:
α : Type u_1
b c : Basis α
h : ∀ (s : Set α), s ∈ c → ∃ t, t ∈ b ∧ t ⊆ s
s : Set α
hs : s ∈ as_filter c
t : Set α
ht : t ∈ c ∧ t ⊆ s
⊢ s ∈ as_filter b
Tactic:
have ⟨u, hu⟩ := h t ht.1
Proof state after:
α : Type u_1
b c : Basis α
h : ∀ (s : Set α), s ∈ c → ∃ t, t ∈ b ∧ t ⊆ s
s : Set α
hs : s ∈ as_filter c
t : Set α
ht : t ∈ c ∧ t ⊆ s
u : Set α
hu : u ∈ b ∧ u ⊆ t
⊢ s ∈ as_filter b
Theorem: FilterGame.Basis.as_filter_le
Proof state before:
α : Type u_1
b c : Basis α
h : ∀ (s : Set α), s ∈ c → ∃ t, t ∈ b ∧ t ⊆ s
s : Set α
hs : s ∈ as_filter c
t : Set α
ht : t ∈ c ∧ t ⊆ s
u : Set α
hu : u ∈ b ∧ u ⊆ t
⊢ s ∈ as_filter b
Tactic:
exact ⟨u, hu.1, subset_trans hu.2 ht.2⟩
Proof state after:
no goals
Theorem: FilterGame.Filter.as_basis_le_iff
Proof state before:
α : Type u_1
f : Filter α
b : Basis α
⊢ as_basis f ≤' b ↔ f ≤ Basis.as_filter b
Tactic:
apply Iff.intro
Proof state after:
case mp
α : Type u_1
f : Filter α
b : Basis α
⊢ as_basis f ≤' b → f ≤ Basis.as_filter b

case mpr
α : Type u_1
f : Filter α
b : Basis α
⊢ f ≤ Basis.as_filter b → as_basis f ≤' b
Theorem: FilterGame.Filter.as_basis_le_iff
Proof state before:
case mp
α : Type u_1
f : Filter α
b : Basis α
⊢ as_basis f ≤' b → f ≤ Basis.as_filter b

case mpr
α : Type u_1
f : Filter α
b : Basis α
⊢ f ≤ Basis.as_filter b → as_basis f ≤' b
Tactic:
. intros h
  rw [← as_basis_as_filter_eq_self f]
  exact Basis.as_filter_le h
Proof state after:
case mpr
α : Type u_1
f : Filter α
b : Basis α
⊢ f ≤ Basis.as_filter b → as_basis f ≤' b
Theorem: FilterGame.Filter.as_basis_le_iff
Proof state before:
case mpr
α : Type u_1
f : Filter α
b : Basis α
⊢ f ≤ Basis.as_filter b → as_basis f ≤' b
Tactic:
. intros h
  rw [Basis.le_def]
  intros s hs
  have hs' := h s (Basis.mem_as_filter_of_mem hs)
  exact ⟨s, hs', subset_rfl⟩
Proof state after:
no goals
Theorem: FilterGame.Filter.as_basis_le_iff
Proof state before:
case mp
α : Type u_1
f : Filter α
b : Basis α
⊢ as_basis f ≤' b → f ≤ Basis.as_filter b
Tactic:
intros h
Proof state after:
case mp
α : Type u_1
f : Filter α
b : Basis α
h : as_basis f ≤' b
⊢ f ≤ Basis.as_filter b
Theorem: FilterGame.Filter.as_basis_le_iff
Proof state before:
case mp
α : Type u_1
f : Filter α
b : Basis α
h : as_basis f ≤' b
⊢ f ≤ Basis.as_filter b
Tactic:
rw [← as_basis_as_filter_eq_self f]
Proof state after:
case mp
α : Type u_1
f : Filter α
b : Basis α
h : as_basis f ≤' b
⊢ Basis.as_filter (as_basis f) ≤ Basis.as_filter b
Theorem: FilterGame.Filter.as_basis_le_iff
Proof state before:
case mp
α : Type u_1
f : Filter α
b : Basis α
h : as_basis f ≤' b
⊢ Basis.as_filter (as_basis f) ≤ Basis.as_filter b
Tactic:
exact Basis.as_filter_le h
Proof state after:
no goals
Theorem: FilterGame.Filter.as_basis_le_iff
Proof state before:
case mpr
α : Type u_1
f : Filter α
b : Basis α
⊢ f ≤ Basis.as_filter b → as_basis f ≤' b
Tactic:
intros h
Proof state after:
case mpr
α : Type u_1
f : Filter α
b : Basis α
h : f ≤ Basis.as_filter b
⊢ as_basis f ≤' b
Theorem: FilterGame.Filter.as_basis_le_iff
Proof state before:
case mpr
α : Type u_1
f : Filter α
b : Basis α
h : f ≤ Basis.as_filter b
⊢ as_basis f ≤' b
Tactic:
rw [Basis.le_def]
Proof state after:
case mpr
α : Type u_1
f : Filter α
b : Basis α
h : f ≤ Basis.as_filter b
⊢ ∀ (s : Set α), s ∈ b → ∃ t, t ∈ as_basis f ∧ t ⊆ s
Theorem: FilterGame.Filter.as_basis_le_iff
Proof state before:
case mpr
α : Type u_1
f : Filter α
b : Basis α
h : f ≤ Basis.as_filter b
⊢ ∀ (s : Set α), s ∈ b → ∃ t, t ∈ as_basis f ∧ t ⊆ s
Tactic:
intros s hs
Proof state after:
case mpr
α : Type u_1
f : Filter α
b : Basis α
h : f ≤ Basis.as_filter b
s : Set α
hs : s ∈ b
⊢ ∃ t, t ∈ as_basis f ∧ t ⊆ s
Theorem: FilterGame.Filter.as_basis_le_iff
Proof state before:
case mpr
α : Type u_1
f : Filter α
b : Basis α
h : f ≤ Basis.as_filter b
s : Set α
hs : s ∈ b
⊢ ∃ t, t ∈ as_basis f ∧ t ⊆ s
Tactic:
have hs' := h s (Basis.mem_as_filter_of_mem hs)
Proof state after:
case mpr
α : Type u_1
f : Filter α
b : Basis α
h : f ≤ Basis.as_filter b
s : Set α
hs : s ∈ b
hs' : s ∈ f
⊢ ∃ t, t ∈ as_basis f ∧ t ⊆ s
Theorem: FilterGame.Filter.as_basis_le_iff
Proof state before:
case mpr
α : Type u_1
f : Filter α
b : Basis α
h : f ≤ Basis.as_filter b
s : Set α
hs : s ∈ b
hs' : s ∈ f
⊢ ∃ t, t ∈ as_basis f ∧ t ⊆ s
Tactic:
exact ⟨s, hs', subset_rfl⟩
Proof state after:
no goals
Theorem: FilterGame.Basis.le_and_le_iff_filter_eq
Proof state before:
α : Type u_1
b c : Basis α
⊢ b ≤' c ∧ c ≤' b ↔ as_filter b = as_filter c
Tactic:
apply Iff.intro
Proof state after:
case mp
α : Type u_1
b c : Basis α
⊢ b ≤' c ∧ c ≤' b → as_filter b = as_filter c

case mpr
α : Type u_1
b c : Basis α
⊢ as_filter b = as_filter c → b ≤' c ∧ c ≤' b
Theorem: FilterGame.Basis.le_and_le_iff_filter_eq
Proof state before:
case mp
α : Type u_1
b c : Basis α
⊢ b ≤' c ∧ c ≤' b → as_filter b = as_filter c

case mpr
α : Type u_1
b c : Basis α
⊢ as_filter b = as_filter c → b ≤' c ∧ c ≤' b
Tactic:
. intros h
  apply le_antisymm
  . exact Basis.as_filter_le h.1
  . exact Basis.as_filter_le h.2
Proof state after:
case mpr
α : Type u_1
b c : Basis α
⊢ as_filter b = as_filter c → b ≤' c ∧ c ≤' b
Theorem: FilterGame.Basis.le_and_le_iff_filter_eq
Proof state before:
case mpr
α : Type u_1
b c : Basis α
⊢ as_filter b = as_filter c → b ≤' c ∧ c ≤' b
Tactic:
. suffices h : ∀ b c, Basis.as_filter b = Basis.as_filter c → b ≤' c
  . intros heq
    exact ⟨h _ _ heq, h _ _ heq.symm⟩
  intros b c hbc s hs
  have hs' := Basis.mem_as_filter_of_mem hs
  rw [← hbc] at hs'
  exact hs'
Proof state after:
no goals
Theorem: FilterGame.Basis.le_and_le_iff_filter_eq
Proof state before:
case mp
α : Type u_1
b c : Basis α
⊢ b ≤' c ∧ c ≤' b → as_filter b = as_filter c
Tactic:
intros h
Proof state after:
case mp
α : Type u_1
b c : Basis α
h : b ≤' c ∧ c ≤' b
⊢ as_filter b = as_filter c
Theorem: FilterGame.Basis.le_and_le_iff_filter_eq
Proof state before:
case mp
α : Type u_1
b c : Basis α
h : b ≤' c ∧ c ≤' b
⊢ as_filter b = as_filter c
Tactic:
apply le_antisymm
Proof state after:
case mp.a
α : Type u_1
b c : Basis α
h : b ≤' c ∧ c ≤' b
⊢ as_filter b ≤ as_filter c

case mp.a
α : Type u_1
b c : Basis α
h : b ≤' c ∧ c ≤' b
⊢ as_filter c ≤ as_filter b
Theorem: FilterGame.Basis.le_and_le_iff_filter_eq
Proof state before:
case mp.a
α : Type u_1
b c : Basis α
h : b ≤' c ∧ c ≤' b
⊢ as_filter b ≤ as_filter c

case mp.a
α : Type u_1
b c : Basis α
h : b ≤' c ∧ c ≤' b
⊢ as_filter c ≤ as_filter b
Tactic:
. exact Basis.as_filter_le h.1
Proof state after:
case mp.a
α : Type u_1
b c : Basis α
h : b ≤' c ∧ c ≤' b
⊢ as_filter c ≤ as_filter b
Theorem: FilterGame.Basis.le_and_le_iff_filter_eq
Proof state before:
case mp.a
α : Type u_1
b c : Basis α
h : b ≤' c ∧ c ≤' b
⊢ as_filter c ≤ as_filter b
Tactic:
. exact Basis.as_filter_le h.2
Proof state after:
no goals
Theorem: FilterGame.Basis.le_and_le_iff_filter_eq
Proof state before:
case mp.a
α : Type u_1
b c : Basis α
h : b ≤' c ∧ c ≤' b
⊢ as_filter b ≤ as_filter c
Tactic:
exact Basis.as_filter_le h.1
Proof state after:
no goals
Theorem: FilterGame.Basis.le_and_le_iff_filter_eq
Proof state before:
case mp.a
α : Type u_1
b c : Basis α
h : b ≤' c ∧ c ≤' b
⊢ as_filter c ≤ as_filter b
Tactic:
exact Basis.as_filter_le h.2
Proof state after:
no goals
Theorem: FilterGame.Basis.le_and_le_iff_filter_eq
Proof state before:
case mpr
α : Type u_1
b c : Basis α
⊢ as_filter b = as_filter c → b ≤' c ∧ c ≤' b
Tactic:
suffices h : ∀ b c, Basis.as_filter b = Basis.as_filter c → b ≤' c
Proof state after:
case mpr
α : Type u_1
b c : Basis α
h : ∀ (b c : Basis ?m.10532), as_filter b = as_filter c → b ≤' c
⊢ as_filter b = as_filter c → b ≤' c ∧ c ≤' b

case h
α : Type u_1
b c : Basis α
⊢ ∀ (b c : Basis ?m.10532), as_filter b = as_filter c → b ≤' c
Theorem: FilterGame.Basis.le_and_le_iff_filter_eq
Proof state before:
case mpr
α : Type u_1
b c : Basis α
h : ∀ (b c : Basis ?m.10532), as_filter b = as_filter c → b ≤' c
⊢ as_filter b = as_filter c → b ≤' c ∧ c ≤' b

case h
α : Type u_1
b c : Basis α
⊢ ∀ (b c : Basis ?m.10532), as_filter b = as_filter c → b ≤' c
Tactic:
. intros heq
  exact ⟨h _ _ heq, h _ _ heq.symm⟩
Proof state after:
case h
α : Type u_1
b c : Basis α
⊢ ∀ (b c : Basis α), as_filter b = as_filter c → b ≤' c
Theorem: FilterGame.Basis.le_and_le_iff_filter_eq
Proof state before:
case h
α : Type u_1
b c : Basis α
⊢ ∀ (b c : Basis α), as_filter b = as_filter c → b ≤' c
Tactic:
intros b c hbc s hs
Proof state after:
case h
α : Type u_1
b✝ c✝ b c : Basis α
hbc : as_filter b = as_filter c
s : Set α
hs : s ∈ c
⊢ ∃ t, t ∈ b ∧ t ⊆ s
Theorem: FilterGame.Basis.le_and_le_iff_filter_eq
Proof state before:
case h
α : Type u_1
b✝ c✝ b c : Basis α
hbc : as_filter b = as_filter c
s : Set α
hs : s ∈ c
⊢ ∃ t, t ∈ b ∧ t ⊆ s
Tactic:
have hs' := Basis.mem_as_filter_of_mem hs
Proof state after:
case h
α : Type u_1
b✝ c✝ b c : Basis α
hbc : as_filter b = as_filter c
s : Set α
hs : s ∈ c
hs' : s ∈ as_filter c
⊢ ∃ t, t ∈ b ∧ t ⊆ s
Theorem: FilterGame.Basis.le_and_le_iff_filter_eq
Proof state before:
case h
α : Type u_1
b✝ c✝ b c : Basis α
hbc : as_filter b = as_filter c
s : Set α
hs : s ∈ c
hs' : s ∈ as_filter c
⊢ ∃ t, t ∈ b ∧ t ⊆ s
Tactic:
rw [← hbc] at hs'
Proof state after:
case h
α : Type u_1
b✝ c✝ b c : Basis α
hbc : as_filter b = as_filter c
s : Set α
hs : s ∈ c
hs' : s ∈ as_filter b
⊢ ∃ t, t ∈ b ∧ t ⊆ s
Theorem: FilterGame.Basis.le_and_le_iff_filter_eq
Proof state before:
case h
α : Type u_1
b✝ c✝ b c : Basis α
hbc : as_filter b = as_filter c
s : Set α
hs : s ∈ c
hs' : s ∈ as_filter b
⊢ ∃ t, t ∈ b ∧ t ⊆ s
Tactic:
exact hs'
Proof state after:
no goals
Theorem: FilterGame.Basis.le_and_le_iff_filter_eq
Proof state before:
case mpr
α : Type u_1
b c : Basis α
h : ∀ (b c : Basis ?m.10532), as_filter b = as_filter c → b ≤' c
⊢ as_filter b = as_filter c → b ≤' c ∧ c ≤' b
Tactic:
intros heq
Proof state after:
case mpr
α : Type u_1
b c : Basis α
h : ∀ (b c : Basis ?m.10532), as_filter b = as_filter c → b ≤' c
heq : as_filter b = as_filter c
⊢ b ≤' c ∧ c ≤' b
Theorem: FilterGame.Basis.le_and_le_iff_filter_eq
Proof state before:
case mpr
α : Type u_1
b c : Basis α
h : ∀ (b c : Basis ?m.10532), as_filter b = as_filter c → b ≤' c
heq : as_filter b = as_filter c
⊢ b ≤' c ∧ c ≤' b
Tactic:
exact ⟨h _ _ heq, h _ _ heq.symm⟩
Proof state after:
no goals
Theorem: FilterGame.TopologicalSpace.mem_nhds_def
Proof state before:
α : Type u_1
τ : TopologicalSpace α
a : α
s : Set α
⊢ s ∈ 𝓝 a ↔ ∃ t, t ⊆ s ∧ sets τ t ∧ a ∈ t
Tactic:
exact Iff.rfl
Proof state after:
no goals
Theorem: FilterGame.TopologicalSpace.nhds_le_of_le
Proof state before:
α : Type u_1
τ : TopologicalSpace α
f : Filter α
a : α
s : Set α
h : a ∈ s
ho : sets τ s
hsf : 𝓟 s ≤ f
⊢ 𝓝 a ≤ f
Tactic:
intros u hu
Proof state after:
α : Type u_1
τ : TopologicalSpace α
f : Filter α
a : α
s : Set α
h : a ∈ s
ho : sets τ s
hsf : 𝓟 s ≤ f
u : Set α
hu : u ∈ f
⊢ u ∈ 𝓝 a
Theorem: FilterGame.TopologicalSpace.nhds_le_of_le
Proof state before:
α : Type u_1
τ : TopologicalSpace α
f : Filter α
a : α
s : Set α
h : a ∈ s
ho : sets τ s
hsf : 𝓟 s ≤ f
u : Set α
hu : u ∈ f
⊢ u ∈ 𝓝 a
Tactic:
rw [mem_nhds_def]
Proof state after:
α : Type u_1
τ : TopologicalSpace α
f : Filter α
a : α
s : Set α
h : a ∈ s
ho : sets τ s
hsf : 𝓟 s ≤ f
u : Set α
hu : u ∈ f
⊢ ∃ t, t ⊆ u ∧ sets τ t ∧ a ∈ t
Theorem: FilterGame.TopologicalSpace.nhds_le_of_le
Proof state before:
α : Type u_1
τ : TopologicalSpace α
f : Filter α
a : α
s : Set α
h : a ∈ s
ho : sets τ s
hsf : 𝓟 s ≤ f
u : Set α
hu : u ∈ f
⊢ ∃ t, t ⊆ u ∧ sets τ t ∧ a ∈ t
Tactic:
specialize hsf _ hu
Proof state after:
α : Type u_1
τ : TopologicalSpace α
f : Filter α
a : α
s : Set α
h : a ∈ s
ho : sets τ s
u : Set α
hu : u ∈ f
hsf : u ∈ 𝓟 s
⊢ ∃ t, t ⊆ u ∧ sets τ t ∧ a ∈ t
Theorem: FilterGame.TopologicalSpace.nhds_le_of_le
Proof state before:
α : Type u_1
τ : TopologicalSpace α
f : Filter α
a : α
s : Set α
h : a ∈ s
ho : sets τ s
u : Set α
hu : u ∈ f
hsf : u ∈ 𝓟 s
⊢ ∃ t, t ⊆ u ∧ sets τ t ∧ a ∈ t
Tactic:
rw [Filter.mem_principal_def] at hsf
Proof state after:
α : Type u_1
τ : TopologicalSpace α
f : Filter α
a : α
s : Set α
h : a ∈ s
ho : sets τ s
u : Set α
hu : u ∈ f
hsf : s ⊆ u
⊢ ∃ t, t ⊆ u ∧ sets τ t ∧ a ∈ t
Theorem: FilterGame.TopologicalSpace.nhds_le_of_le
Proof state before:
α : Type u_1
τ : TopologicalSpace α
f : Filter α
a : α
s : Set α
h : a ∈ s
ho : sets τ s
u : Set α
hu : u ∈ f
hsf : s ⊆ u
⊢ ∃ t, t ⊆ u ∧ sets τ t ∧ a ∈ t
Tactic:
exact ⟨s, hsf, ho, h⟩
Proof state after:
no goals
Theorem: FilterGame.TopologicalSpace.mem_of_mem_nhds
Proof state before:
α : Type u_1
τ : TopologicalSpace α
a : α
s : Set α
hs : s ∈ 𝓝 a
⊢ a ∈ s
Tactic:
rw [mem_nhds_def] at hs
Proof state after:
α : Type u_1
τ : TopologicalSpace α
a : α
s : Set α
hs : ∃ t, t ⊆ s ∧ sets τ t ∧ a ∈ t
⊢ a ∈ s
Theorem: FilterGame.TopologicalSpace.mem_of_mem_nhds
Proof state before:
α : Type u_1
τ : TopologicalSpace α
a : α
s : Set α
hs : ∃ t, t ⊆ s ∧ sets τ t ∧ a ∈ t
⊢ a ∈ s
Tactic:
have ⟨u, hu₁, hu₂, hu₃⟩ := hs
Proof state after:
α : Type u_1
τ : TopologicalSpace α
a : α
s : Set α
hs : ∃ t, t ⊆ s ∧ sets τ t ∧ a ∈ t
u : Set α
hu₁ : u ⊆ s
hu₂ : sets τ u
hu₃ : a ∈ u
⊢ a ∈ s
Theorem: FilterGame.TopologicalSpace.mem_of_mem_nhds
Proof state before:
α : Type u_1
τ : TopologicalSpace α
a : α
s : Set α
hs : ∃ t, t ⊆ s ∧ sets τ t ∧ a ∈ t
u : Set α
hu₁ : u ⊆ s
hu₂ : sets τ u
hu₃ : a ∈ u
⊢ a ∈ s
Tactic:
exact hu₁ hu₃
Proof state after:
no goals
Theorem: FilterGame.TopologicalSpace.OpenSets.mem_nhds
Proof state before:
α : Type u_1
τ : TopologicalSpace α
a : α
s : Set α
hs : sets τ s
ha : a ∈ s
⊢ s ∈ 𝓝 a
Tactic:
rw [mem_nhds_def]
Proof state after:
α : Type u_1
τ : TopologicalSpace α
a : α
s : Set α
hs : sets τ s
ha : a ∈ s
⊢ ∃ t, t ⊆ s ∧ sets τ t ∧ a ∈ t
Theorem: FilterGame.TopologicalSpace.OpenSets.mem_nhds
Proof state before:
α : Type u_1
τ : TopologicalSpace α
a : α
s : Set α
hs : sets τ s
ha : a ∈ s
⊢ ∃ t, t ⊆ s ∧ sets τ t ∧ a ∈ t
Tactic:
exact ⟨s, rfl.subset, hs, ha⟩
Proof state after:
no goals
Theorem: FilterGame.TopologicalSpace.OpenSets.mem_nhds_iff
Proof state before:
α : Type u_1
τ : TopologicalSpace α
a : α
s : Set α
hs : sets τ s
⊢ s ∈ 𝓝 a ↔ a ∈ s
Tactic:
apply Iff.intro
Proof state after:
case mp
α : Type u_1
τ : TopologicalSpace α
a : α
s : Set α
hs : sets τ s
⊢ s ∈ 𝓝 a → a ∈ s

case mpr
α : Type u_1
τ : TopologicalSpace α
a : α
s : Set α
hs : sets τ s
⊢ a ∈ s → s ∈ 𝓝 a
Theorem: FilterGame.TopologicalSpace.OpenSets.mem_nhds_iff
Proof state before:
case mp
α : Type u_1
τ : TopologicalSpace α
a : α
s : Set α
hs : sets τ s
⊢ s ∈ 𝓝 a → a ∈ s

case mpr
α : Type u_1
τ : TopologicalSpace α
a : α
s : Set α
hs : sets τ s
⊢ a ∈ s → s ∈ 𝓝 a
Tactic:
. exact mem_of_mem_nhds
Proof state after:
case mpr
α : Type u_1
τ : TopologicalSpace α
a : α
s : Set α
hs : sets τ s
⊢ a ∈ s → s ∈ 𝓝 a
Theorem: FilterGame.TopologicalSpace.OpenSets.mem_nhds_iff
Proof state before:
case mpr
α : Type u_1
τ : TopologicalSpace α
a : α
s : Set α
hs : sets τ s
⊢ a ∈ s → s ∈ 𝓝 a
Tactic:
. exact mem_nhds hs
Proof state after:
no goals
Theorem: FilterGame.TopologicalSpace.OpenSets.mem_nhds_iff
Proof state before:
case mp
α : Type u_1
τ : TopologicalSpace α
a : α
s : Set α
hs : sets τ s
⊢ s ∈ 𝓝 a → a ∈ s
Tactic:
exact mem_of_mem_nhds
Proof state after:
no goals
Theorem: FilterGame.TopologicalSpace.OpenSets.mem_nhds_iff
Proof state before:
case mpr
α : Type u_1
τ : TopologicalSpace α
a : α
s : Set α
hs : sets τ s
⊢ a ∈ s → s ∈ 𝓝 a
Tactic:
exact mem_nhds hs
Proof state after:
no goals
Theorem: FilterGame.Basis.mem_def
Proof state before:
α : Type u_1
b : Basis α
s : Set α
⊢ s ∈ b ↔ s ∈ b.sets
Tactic:
exact Iff.rfl
Proof state after:
no goals
Theorem: FilterGame.Basis.eq_def
Proof state before:
α : Type u_1
b c : Basis α
⊢ b = c ↔ b.sets = c.sets
Tactic:
apply Iff.intro
Proof state after:
case mp
α : Type u_1
b c : Basis α
⊢ b = c → b.sets = c.sets

case mpr
α : Type u_1
b c : Basis α
⊢ b.sets = c.sets → b = c
Theorem: FilterGame.Basis.eq_def
Proof state before:
case mp
α : Type u_1
b c : Basis α
⊢ b = c → b.sets = c.sets

case mpr
α : Type u_1
b c : Basis α
⊢ b.sets = c.sets → b = c
Tactic:
. intro h; rw [h]
Proof state after:
case mpr
α : Type u_1
b c : Basis α
⊢ b.sets = c.sets → b = c
Theorem: FilterGame.Basis.eq_def
Proof state before:
case mpr
α : Type u_1
b c : Basis α
⊢ b.sets = c.sets → b = c
Tactic:
. intro h; cases b; cases c; congr
Proof state after:
no goals
Theorem: FilterGame.Basis.eq_def
Proof state before:
case mp
α : Type u_1
b c : Basis α
⊢ b = c → b.sets = c.sets
Tactic:
intro h
Proof state after:
case mp
α : Type u_1
b c : Basis α
h : b = c
⊢ b.sets = c.sets
Theorem: FilterGame.Basis.eq_def
Proof state before:
case mp
α : Type u_1
b c : Basis α
h : b = c
⊢ b.sets = c.sets
Tactic:
rw [h]
Proof state after:
no goals
Theorem: FilterGame.Basis.eq_def
Proof state before:
case mpr
α : Type u_1
b c : Basis α
⊢ b.sets = c.sets → b = c
Tactic:
intro h
Proof state after:
case mpr
α : Type u_1
b c : Basis α
h : b.sets = c.sets
⊢ b = c
Theorem: FilterGame.Basis.eq_def
Proof state before:
case mpr
α : Type u_1
b c : Basis α
h : b.sets = c.sets
⊢ b = c
Tactic:
cases b
Proof state after:
case mpr.mk
α : Type u_1
c : Basis α
sets✝ : Set (Set α)
sets_nonempty✝ : ∃ s, s ∈ sets✝
inter_mem_sets✝ : ∀ {s t : Set α}, s ∈ sets✝ → t ∈ sets✝ → ∃ u, u ∈ sets✝ ∧ u ⊆ s ∩ t
h : { sets := sets✝, sets_nonempty := sets_nonempty✝, inter_mem_sets := inter_mem_sets✝ }.sets = c.sets
⊢ { sets := sets✝, sets_nonempty := sets_nonempty✝, inter_mem_sets := inter_mem_sets✝ } = c
Theorem: FilterGame.Basis.eq_def
Proof state before:
case mpr.mk
α : Type u_1
c : Basis α
sets✝ : Set (Set α)
sets_nonempty✝ : ∃ s, s ∈ sets✝
inter_mem_sets✝ : ∀ {s t : Set α}, s ∈ sets✝ → t ∈ sets✝ → ∃ u, u ∈ sets✝ ∧ u ⊆ s ∩ t
h : { sets := sets✝, sets_nonempty := sets_nonempty✝, inter_mem_sets := inter_mem_sets✝ }.sets = c.sets
⊢ { sets := sets✝, sets_nonempty := sets_nonempty✝, inter_mem_sets := inter_mem_sets✝ } = c
Tactic:
cases c
Proof state after:
case mpr.mk.mk
α : Type u_1
sets✝¹ : Set (Set α)
sets_nonempty✝¹ : ∃ s, s ∈ sets✝¹
inter_mem_sets✝¹ : ∀ {s t : Set α}, s ∈ sets✝¹ → t ∈ sets✝¹ → ∃ u, u ∈ sets✝¹ ∧ u ⊆ s ∩ t
sets✝ : Set (Set α)
sets_nonempty✝ : ∃ s, s ∈ sets✝
inter_mem_sets✝ : ∀ {s t : Set α}, s ∈ sets✝ → t ∈ sets✝ → ∃ u, u ∈ sets✝ ∧ u ⊆ s ∩ t
h :
  { sets := sets✝¹, sets_nonempty := sets_nonempty✝¹, inter_mem_sets := inter_mem_sets✝¹ }.sets =
    { sets := sets✝, sets_nonempty := sets_nonempty✝, inter_mem_sets := inter_mem_sets✝ }.sets
⊢ { sets := sets✝¹, sets_nonempty := sets_nonempty✝¹, inter_mem_sets := inter_mem_sets✝¹ } =
    { sets := sets✝, sets_nonempty := sets_nonempty✝, inter_mem_sets := inter_mem_sets✝ }
Theorem: FilterGame.Basis.eq_def
Proof state before:
case mpr.mk.mk
α : Type u_1
sets✝¹ : Set (Set α)
sets_nonempty✝¹ : ∃ s, s ∈ sets✝¹
inter_mem_sets✝¹ : ∀ {s t : Set α}, s ∈ sets✝¹ → t ∈ sets✝¹ → ∃ u, u ∈ sets✝¹ ∧ u ⊆ s ∩ t
sets✝ : Set (Set α)
sets_nonempty✝ : ∃ s, s ∈ sets✝
inter_mem_sets✝ : ∀ {s t : Set α}, s ∈ sets✝ → t ∈ sets✝ → ∃ u, u ∈ sets✝ ∧ u ⊆ s ∩ t
h :
  { sets := sets✝¹, sets_nonempty := sets_nonempty✝¹, inter_mem_sets := inter_mem_sets✝¹ }.sets =
    { sets := sets✝, sets_nonempty := sets_nonempty✝, inter_mem_sets := inter_mem_sets✝ }.sets
⊢ { sets := sets✝¹, sets_nonempty := sets_nonempty✝¹, inter_mem_sets := inter_mem_sets✝¹ } =
    { sets := sets✝, sets_nonempty := sets_nonempty✝, inter_mem_sets := inter_mem_sets✝ }
Tactic:
congr
Proof state after:
no goals
Theorem: FilterGame.Basis.ext_iff
Proof state before:
α : Type u_1
b c : Basis α
⊢ b = c ↔ ∀ (s : Set α), s ∈ b ↔ s ∈ c
Tactic:
simp_rw [eq_def, mem_def, Set.ext_iff]
Proof state after:
no goals
Theorem: FilterGame.Basis.ext
Proof state before:
α : Type u_1
b c : Basis α
⊢ (∀ (s : Set α), s ∈ b ↔ s ∈ c) → b = c
Tactic:
exact (ext_iff _ _).mpr
Proof state after:
no goals
Theorem: FilterGame.Filter.mem_as_basis_def
Proof state before:
α : Type u_1
f : Filter α
t : Set α
⊢ t ∈ as_basis f ↔ t ∈ f
Tactic:
exact Iff.rfl
Proof state after:
no goals
Theorem: FilterGame.Basis.mem_as_filter_def
Proof state before:
α : Type u_1
b : Basis α
s : Set α
⊢ s ∈ as_filter b ↔ ∃ t, t ∈ b ∧ t ⊆ s
Tactic:
exact Iff.rfl
Proof state after:
no goals
Theorem: FilterGame.Basis.mem_as_filter_of_mem
Proof state before:
α : Type u_1
b : Basis α
s : Set α
h : s ∈ b
⊢ s ∈ as_filter b
Tactic:
rw [Basis.mem_as_filter_def]
Proof state after:
α : Type u_1
b : Basis α
s : Set α
h : s ∈ b
⊢ ∃ t, t ∈ b ∧ t ⊆ s
Theorem: FilterGame.Basis.mem_as_filter_of_mem
Proof state before:
α : Type u_1
b : Basis α
s : Set α
h : s ∈ b
⊢ ∃ t, t ∈ b ∧ t ⊆ s
Tactic:
exact ⟨s, h, subset_rfl⟩
Proof state after:
no goals
Theorem: FilterGame.Filter.as_basis_as_filter_eq_self
Proof state before:
α : Type u_1
f : Filter α
⊢ Basis.as_filter (as_basis f) = f
Tactic:
rw [eq_def]
Proof state after:
α : Type u_1
f : Filter α
⊢ (Basis.as_filter (as_basis f)).sets = f.sets
Theorem: FilterGame.Filter.as_basis_as_filter_eq_self
Proof state before:
α : Type u_1
f : Filter α
⊢ (Basis.as_filter (as_basis f)).sets = f.sets
Tactic:
apply Set.ext
Proof state after:
case h
α : Type u_1
f : Filter α
⊢ ∀ (x : Set α), x ∈ (Basis.as_filter (as_basis f)).sets ↔ x ∈ f.sets
Theorem: FilterGame.Filter.as_basis_as_filter_eq_self
Proof state before:
case h
α : Type u_1
f : Filter α
⊢ ∀ (x : Set α), x ∈ (Basis.as_filter (as_basis f)).sets ↔ x ∈ f.sets
Tactic:
intros x
Proof state after:
case h
α : Type u_1
f : Filter α
x : Set α
⊢ x ∈ (Basis.as_filter (as_basis f)).sets ↔ x ∈ f.sets
Theorem: FilterGame.Filter.as_basis_as_filter_eq_self
Proof state before:
case h
α : Type u_1
f : Filter α
x : Set α
⊢ x ∈ (Basis.as_filter (as_basis f)).sets ↔ x ∈ f.sets
Tactic:
simp_rw [← mem_def, Basis.mem_as_filter_def, mem_as_basis_def]
Proof state after:
case h
α : Type u_1
f : Filter α
x : Set α
⊢ (∃ t, t ∈ f ∧ t ⊆ x) ↔ x ∈ f
Theorem: FilterGame.Filter.as_basis_as_filter_eq_self
Proof state before:
case h
α : Type u_1
f : Filter α
x : Set α
⊢ (∃ t, t ∈ f ∧ t ⊆ x) ↔ x ∈ f
Tactic:
apply Iff.intro
Proof state after:
case h.mp
α : Type u_1
f : Filter α
x : Set α
⊢ (∃ t, t ∈ f ∧ t ⊆ x) → x ∈ f

case h.mpr
α : Type u_1
f : Filter α
x : Set α
⊢ x ∈ f → ∃ t, t ∈ f ∧ t ⊆ x
Theorem: FilterGame.Filter.as_basis_as_filter_eq_self
Proof state before:
case h.mp
α : Type u_1
f : Filter α
x : Set α
⊢ (∃ t, t ∈ f ∧ t ⊆ x) → x ∈ f

case h.mpr
α : Type u_1
f : Filter α
x : Set α
⊢ x ∈ f → ∃ t, t ∈ f ∧ t ⊆ x
Tactic:
. intros hx; have ⟨t, ht⟩ := hx; exact superset_mem ht.1 ht.2
Proof state after:
case h.mpr
α : Type u_1
f : Filter α
x : Set α
⊢ x ∈ f → ∃ t, t ∈ f ∧ t ⊆ x