internlm/Lean-Github huggingface dataset:
Theorem: FilterGame.Set.mem_iff
Proof state before:
α : Type u_1
p : α → Prop
y : α
⊢ y ∈ {x | p x} ↔ p y
Tactic:
exact Iff.rfl
Proof state after:
no goals
Theorem: FilterGame.Filter.le_def
Proof state before:
α : Type u_1
f g : Filter α
⊢ f ≤ g ↔ ∀ (s : Set α), s ∈ g → s ∈ f
Tactic:
exact Iff.rfl
Proof state after:
no goals
Theorem: FilterGame.Basis.le_def
Proof state before:
α : Type u_1
b c : Basis α
⊢ b ≤' c ↔ ∀ (s : Set α), s ∈ c → ∃ t, t ∈ b ∧ t ⊆ s
Tactic:
exact Iff.rfl
Proof state after:
no goals
Theorem: FilterGame.Basis.as_filter_le
Proof state before:
α : Type u_1
b c : Basis α
h : b ≤' c
⊢ as_filter b ≤ as_filter c
Tactic:
rw [Basis.le_def] at h
Proof state after:
α : Type u_1
b c : Basis α
h : ∀ (s : Set α), s ∈ c → ∃ t, t ∈ b ∧ t ⊆ s
⊢ as_filter b ≤ as_filter c
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:
sorry
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:
sorry
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:
sorry
Proof state after:
no goals
Theorem: FilterGame.Filter.ext_iff
Proof state before:
α : Type u_1
f g : Filter α
⊢ f = g ↔ ∀ (s : Set α), s ∈ f ↔ s ∈ g
Tactic:
simp only [eq_def, mem_def, Set.ext_iff]
Proof state after:
no goals
Theorem: FilterGame.Filter.ext
Proof state before:
α : Type u_1
f g : Filter α
⊢ (∀ (s : Set α), s ∈ f ↔ s ∈ g) → f = g
Tactic:
exact (ext_iff _ _).mpr
Proof state after:
no goals
Theorem: FilterGame.Ultrafilter.unique
Proof state before:
α : Type u_1
f : Ultrafilter α
g : Filter α
h : g ≤ f.as_filter
hg : g ≠ ⊥
⊢ g = f.as_filter
Tactic:
apply le_antisymm h
Proof state after:
α : Type u_1
f : Ultrafilter α
g : Filter α
h : g ≤ f.as_filter
hg : g ≠ ⊥
⊢ f.as_filter ≤ g
Theorem: FilterGame.Ultrafilter.unique
Proof state before:
α : Type u_1
f : Ultrafilter α
g : Filter α
h : g ≤ f.as_filter
hg : g ≠ ⊥
⊢ f.as_filter ≤ g
Tactic:
exact f.le_of_le hg h
Proof state after:
no goals
Theorem: FilterGame.Ultrafilter.mem_coe
Proof state before:
α : Type u_1
f : Ultrafilter α
s : Set α
⊢ s ∈ f.as_filter ↔ s ∈ f
Tactic:
exact Iff.rfl
Proof state after:
no goals
Theorem: FilterGame.Ultrafilter.coe_injective
Proof state before:
α : Type u_1
⊢ Function.Injective Coe.coe
Tactic:
intros f g h
Proof state after:
α : Type u_1
f g : Ultrafilter α
h : Coe.coe f = Coe.coe g
⊢ f = g
Theorem: FilterGame.Ultrafilter.coe_injective
Proof state before:
α : Type u_1
f g : Ultrafilter α
h : Coe.coe f = Coe.coe g
⊢ f = g
Tactic:
cases f
Proof state after:
case mk
α : Type u_1
g : Ultrafilter α
as_filter✝ : Filter α
ne_bot✝ : as_filter✝ ≠ ⊥
le_of_le✝ : ∀ {g : Filter α}, g ≠ ⊥ → g ≤ as_filter✝ → as_filter✝ ≤ g
h : Coe.coe { as_filter := as_filter✝, ne_bot := ne_bot✝, le_of_le := le_of_le✝ } = Coe.coe g
⊢ { as_filter := as_filter✝, ne_bot := ne_bot✝, le_of_le := le_of_le✝ } = g
Theorem: FilterGame.Ultrafilter.coe_injective
Proof state before:
case mk
α : Type u_1
g : Ultrafilter α
as_filter✝ : Filter α
ne_bot✝ : as_filter✝ ≠ ⊥
le_of_le✝ : ∀ {g : Filter α}, g ≠ ⊥ → g ≤ as_filter✝ → as_filter✝ ≤ g
h : Coe.coe { as_filter := as_filter✝, ne_bot := ne_bot✝, le_of_le := le_of_le✝ } = Coe.coe g
⊢ { as_filter := as_filter✝, ne_bot := ne_bot✝, le_of_le := le_of_le✝ } = g
Tactic:
cases g
Proof state after:
case mk.mk
α : Type u_1
as_filter✝¹ : Filter α
ne_bot✝¹ : as_filter✝¹ ≠ ⊥
le_of_le✝¹ : ∀ {g : Filter α}, g ≠ ⊥ → g ≤ as_filter✝¹ → as_filter✝¹ ≤ g
as_filter✝ : Filter α
ne_bot✝ : as_filter✝ ≠ ⊥
le_of_le✝ : ∀ {g : Filter α}, g ≠ ⊥ → g ≤ as_filter✝ → as_filter✝ ≤ g
h :
  Coe.coe { as_filter := as_filter✝¹, ne_bot := ne_bot✝¹, le_of_le := le_of_le✝¹ } =
    Coe.coe { as_filter := as_filter✝, ne_bot := ne_bot✝, le_of_le := le_of_le✝ }
⊢ { as_filter := as_filter✝¹, ne_bot := ne_bot✝¹, le_of_le := le_of_le✝¹ } =
    { as_filter := as_filter✝, ne_bot := ne_bot✝, le_of_le := le_of_le✝ }
Theorem: FilterGame.Ultrafilter.coe_injective
Proof state before:
case mk.mk
α : Type u_1
as_filter✝¹ : Filter α
ne_bot✝¹ : as_filter✝¹ ≠ ⊥
le_of_le✝¹ : ∀ {g : Filter α}, g ≠ ⊥ → g ≤ as_filter✝¹ → as_filter✝¹ ≤ g
as_filter✝ : Filter α
ne_bot✝ : as_filter✝ ≠ ⊥
le_of_le✝ : ∀ {g : Filter α}, g ≠ ⊥ → g ≤ as_filter✝ → as_filter✝ ≤ g
h :
  Coe.coe { as_filter := as_filter✝¹, ne_bot := ne_bot✝¹, le_of_le := le_of_le✝¹ } =
    Coe.coe { as_filter := as_filter✝, ne_bot := ne_bot✝, le_of_le := le_of_le✝ }
⊢ { as_filter := as_filter✝¹, ne_bot := ne_bot✝¹, le_of_le := le_of_le✝¹ } =
    { as_filter := as_filter✝, ne_bot := ne_bot✝, le_of_le := le_of_le✝ }
Tactic:
congr
Proof state after:
no goals
Theorem: FilterGame.Ultrafilter.eq_of_le
Proof state before:
α : Type u_1
f g : Ultrafilter α
h : f.as_filter ≤ g.as_filter
⊢ f = g
Tactic:
exact coe_injective (g.unique h f.ne_bot)
Proof state after:
no goals
Theorem: FilterGame.Ultrafilter.coe_le_coe_iff_eq
Proof state before:
α : Type u_1
f g : Ultrafilter α
⊢ f.as_filter ≤ g.as_filter ↔ f = g
Tactic:
apply Iff.intro
Proof state after:
case mp
α : Type u_1
f g : Ultrafilter α
⊢ f.as_filter ≤ g.as_filter → f = g

case mpr
α : Type u_1
f g : Ultrafilter α
⊢ f = g → f.as_filter ≤ g.as_filter
Theorem: FilterGame.Ultrafilter.coe_le_coe_iff_eq
Proof state before:
case mp
α : Type u_1
f g : Ultrafilter α
⊢ f.as_filter ≤ g.as_filter → f = g

case mpr
α : Type u_1
f g : Ultrafilter α
⊢ f = g → f.as_filter ≤ g.as_filter
Tactic:
. exact eq_of_le
Proof state after:
case mpr
α : Type u_1
f g : Ultrafilter α
⊢ f = g → f.as_filter ≤ g.as_filter
Theorem: FilterGame.Ultrafilter.coe_le_coe_iff_eq
Proof state before:
case mpr
α : Type u_1
f g : Ultrafilter α
⊢ f = g → f.as_filter ≤ g.as_filter
Tactic:
. intros h; rw [h]
Proof state after:
no goals
Theorem: FilterGame.Ultrafilter.coe_le_coe_iff_eq
Proof state before:
case mp
α : Type u_1
f g : Ultrafilter α
⊢ f.as_filter ≤ g.as_filter → f = g
Tactic:
exact eq_of_le
Proof state after:
no goals
Theorem: FilterGame.Ultrafilter.coe_le_coe_iff_eq
Proof state before:
case mpr
α : Type u_1
f g : Ultrafilter α
⊢ f = g → f.as_filter ≤ g.as_filter
Tactic:
intros h
Proof state after:
case mpr
α : Type u_1
f g : Ultrafilter α
h : f = g
⊢ f.as_filter ≤ g.as_filter
Theorem: FilterGame.Ultrafilter.coe_le_coe_iff_eq
Proof state before:
case mpr
α : Type u_1
f g : Ultrafilter α
h : f = g
⊢ f.as_filter ≤ g.as_filter
Tactic:
rw [h]
Proof state after:
no goals
Theorem: FilterGame.Ultrafilter.coe_inj
Proof state before:
α : Type u_1
f g : Ultrafilter α
⊢ f.as_filter = g.as_filter ↔ f = g
Tactic:
exact coe_injective.eq_iff
Proof state after:
no goals
Theorem: FilterGame.Ultrafilter.ext
Proof state before:
α : Type u_1
f g : Ultrafilter α
h : ∀ (s : Set α), s ∈ f ↔ s ∈ g
⊢ f = g
Tactic:
exact coe_injective (Filter.ext h)
Proof state after:
no goals
Theorem: FilterGame.Ultrafilter.le_of_inf_ne_bot
Proof state before:
α : Type u_1
f : Ultrafilter α
g : Filter α
hg : f.as_filter ⊓ g ≠ ⊥
⊢ f.as_filter ≤ g
Tactic:
apply le_of_inf_eq
Proof state after:
case a
α : Type u_1
f : Ultrafilter α
g : Filter α
hg : f.as_filter ⊓ g ≠ ⊥
⊢ f.as_filter ⊓ g = f.as_filter
Theorem: FilterGame.Ultrafilter.le_of_inf_ne_bot
Proof state before:
case a
α : Type u_1
f : Ultrafilter α
g : Filter α
hg : f.as_filter ⊓ g ≠ ⊥
⊢ f.as_filter ⊓ g = f.as_filter
Tactic:
refine unique ?_ hg
Proof state after:
case a
α : Type u_1
f : Ultrafilter α
g : Filter α
hg : f.as_filter ⊓ g ≠ ⊥
⊢ f.as_filter ⊓ g ≤ f.as_filter
Theorem: FilterGame.Ultrafilter.le_of_inf_ne_bot
Proof state before:
case a
α : Type u_1
f : Ultrafilter α
g : Filter α
hg : f.as_filter ⊓ g ≠ ⊥
⊢ f.as_filter ⊓ g ≤ f.as_filter
Tactic:
exact inf_le_left
Proof state after:
no goals
Theorem: FilterGame.Ultrafilter.compl_not_mem_iff
Proof state before:
α : Type u_1
f : Ultrafilter α
s : Set α
⊢ ¬sᶜ ∈ f ↔ s ∈ f
Tactic:
apply Iff.intro
Proof state after:
case mp
α : Type u_1
f : Ultrafilter α
s : Set α
⊢ ¬sᶜ ∈ f → s ∈ f

case mpr
α : Type u_1
f : Ultrafilter α
s : Set α
⊢ s ∈ f → ¬sᶜ ∈ f
Theorem: FilterGame.Ultrafilter.compl_not_mem_iff
Proof state before:
case mp
α : Type u_1
f : Ultrafilter α
s : Set α
⊢ ¬sᶜ ∈ f → s ∈ f

case mpr
α : Type u_1
f : Ultrafilter α
s : Set α
⊢ s ∈ f → ¬sᶜ ∈ f
Tactic:
. intros hne
  rw [← mem_coe, ← Filter.le_principal_iff]
  apply le_of_inf_ne_bot
  intros h
  rw [← Filter.empty_mem_iff_eq_bot, Filter.mem_inf_principal_iff] at h
  suffices h' : {x | x ∈ s → x ∈ (∅ : Set α)} = sᶜ
  . rw [h'] at h
    exact hne h
  apply Set.ext; intros x
  rw [Set.mem_iff, Set.mem_compl_iff, Set.mem_empty_iff_false]
Proof state after:
case mpr
α : Type u_1
f : Ultrafilter α
s : Set α
⊢ s ∈ f → ¬sᶜ ∈ f
Theorem: FilterGame.Ultrafilter.compl_not_mem_iff
Proof state before:
case mpr
α : Type u_1
f : Ultrafilter α
s : Set α
⊢ s ∈ f → ¬sᶜ ∈ f
Tactic:
. exact Filter.compl_not_mem f.ne_bot
Proof state after:
no goals
Theorem: FilterGame.Ultrafilter.compl_not_mem_iff
Proof state before:
case mp
α : Type u_1
f : Ultrafilter α
s : Set α
⊢ ¬sᶜ ∈ f → s ∈ f
Tactic:
intros hne
Proof state after:
case mp
α : Type u_1
f : Ultrafilter α
s : Set α
hne : ¬sᶜ ∈ f
⊢ s ∈ f
Theorem: FilterGame.Ultrafilter.compl_not_mem_iff
Proof state before:
case mp
α : Type u_1
f : Ultrafilter α
s : Set α
hne : ¬sᶜ ∈ f
⊢ s ∈ f
Tactic:
rw [← mem_coe, ← Filter.le_principal_iff]
Proof state after:
case mp
α : Type u_1
f : Ultrafilter α
s : Set α
hne : ¬sᶜ ∈ f
⊢ f.as_filter ≤ 𝓟 s
Theorem: FilterGame.Ultrafilter.compl_not_mem_iff
Proof state before:
case mp
α : Type u_1
f : Ultrafilter α
s : Set α
hne : ¬sᶜ ∈ f
⊢ f.as_filter ≤ 𝓟 s
Tactic:
apply le_of_inf_ne_bot
Proof state after:
case mp.hg
α : Type u_1
f : Ultrafilter α
s : Set α
hne : ¬sᶜ ∈ f
⊢ f.as_filter ⊓ 𝓟 s ≠ ⊥
Theorem: FilterGame.Ultrafilter.compl_not_mem_iff
Proof state before:
case mp.hg
α : Type u_1
f : Ultrafilter α
s : Set α
hne : ¬sᶜ ∈ f
⊢ f.as_filter ⊓ 𝓟 s ≠ ⊥
Tactic:
intros h
Proof state after:
case mp.hg
α : Type u_1
f : Ultrafilter α
s : Set α
hne : ¬sᶜ ∈ f
h : f.as_filter ⊓ 𝓟 s = ⊥
⊢ False
Theorem: FilterGame.Ultrafilter.compl_not_mem_iff
Proof state before:
case mp.hg
α : Type u_1
f : Ultrafilter α
s : Set α
hne : ¬sᶜ ∈ f
h : f.as_filter ⊓ 𝓟 s = ⊥
⊢ False
Tactic:
rw [← Filter.empty_mem_iff_eq_bot, Filter.mem_inf_principal_iff] at h
Proof state after:
case mp.hg
α : Type u_1
f : Ultrafilter α
s : Set α
hne : ¬sᶜ ∈ f
h : {x | x ∈ s → x ∈ ∅} ∈ f.as_filter
⊢ False
Theorem: FilterGame.Ultrafilter.compl_not_mem_iff
Proof state before:
case mp.hg
α : Type u_1
f : Ultrafilter α
s : Set α
hne : ¬sᶜ ∈ f
h : {x | x ∈ s → x ∈ ∅} ∈ f.as_filter
⊢ False
Tactic:
suffices h' : {x | x ∈ s → x ∈ (∅ : Set α)} = sᶜ
Proof state after:
case mp.hg
α : Type u_1
f : Ultrafilter α
s : Set α
hne : ¬sᶜ ∈ f
h : {x | x ∈ s → x ∈ ∅} ∈ f.as_filter
h' : {x | x ∈ s → x ∈ ∅} = sᶜ
⊢ False

case h'
α : Type u_1
f : Ultrafilter α
s : Set α
hne : ¬sᶜ ∈ f
h : {x | x ∈ s → x ∈ ∅} ∈ f.as_filter
⊢ {x | x ∈ s → x ∈ ∅} = sᶜ
Theorem: FilterGame.Ultrafilter.compl_not_mem_iff
Proof state before:
case mp.hg
α : Type u_1
f : Ultrafilter α
s : Set α
hne : ¬sᶜ ∈ f
h : {x | x ∈ s → x ∈ ∅} ∈ f.as_filter
h' : {x | x ∈ s → x ∈ ∅} = sᶜ
⊢ False

case h'
α : Type u_1
f : Ultrafilter α
s : Set α
hne : ¬sᶜ ∈ f
h : {x | x ∈ s → x ∈ ∅} ∈ f.as_filter
⊢ {x | x ∈ s → x ∈ ∅} = sᶜ
Tactic:
. rw [h'] at h
  exact hne h
Proof state after:
case h'
α : Type u_1
f : Ultrafilter α
s : Set α
hne : ¬sᶜ ∈ f
h : {x | x ∈ s → x ∈ ∅} ∈ f.as_filter
⊢ {x | x ∈ s → x ∈ ∅} = sᶜ
Theorem: FilterGame.Ultrafilter.compl_not_mem_iff
Proof state before:
case h'
α : Type u_1
f : Ultrafilter α
s : Set α
hne : ¬sᶜ ∈ f
h : {x | x ∈ s → x ∈ ∅} ∈ f.as_filter
⊢ {x | x ∈ s → x ∈ ∅} = sᶜ
Tactic:
apply Set.ext
Proof state after:
case h'.h
α : Type u_1
f : Ultrafilter α
s : Set α
hne : ¬sᶜ ∈ f
h : {x | x ∈ s → x ∈ ∅} ∈ f.as_filter
⊢ ∀ (x : α), x ∈ {x | x ∈ s → x ∈ ∅} ↔ x ∈ sᶜ
Theorem: FilterGame.Ultrafilter.compl_not_mem_iff
Proof state before:
case h'.h
α : Type u_1
f : Ultrafilter α
s : Set α
hne : ¬sᶜ ∈ f
h : {x | x ∈ s → x ∈ ∅} ∈ f.as_filter
⊢ ∀ (x : α), x ∈ {x | x ∈ s → x ∈ ∅} ↔ x ∈ sᶜ
Tactic:
intros x
Proof state after:
case h'.h
α : Type u_1
f : Ultrafilter α
s : Set α
hne : ¬sᶜ ∈ f
h : {x | x ∈ s → x ∈ ∅} ∈ f.as_filter
x : α
⊢ x ∈ {x | x ∈ s → x ∈ ∅} ↔ x ∈ sᶜ
Theorem: FilterGame.Ultrafilter.compl_not_mem_iff
Proof state before:
case h'.h
α : Type u_1
f : Ultrafilter α
s : Set α
hne : ¬sᶜ ∈ f
h : {x | x ∈ s → x ∈ ∅} ∈ f.as_filter
x : α
⊢ x ∈ {x | x ∈ s → x ∈ ∅} ↔ x ∈ sᶜ
Tactic:
rw [Set.mem_iff, Set.mem_compl_iff, Set.mem_empty_iff_false]
Proof state after:
no goals
Theorem: FilterGame.Ultrafilter.compl_not_mem_iff
Proof state before:
case mp.hg
α : Type u_1
f : Ultrafilter α
s : Set α
hne : ¬sᶜ ∈ f
h : {x | x ∈ s → x ∈ ∅} ∈ f.as_filter
h' : {x | x ∈ s → x ∈ ∅} = sᶜ
⊢ False
Tactic:
rw [h'] at h
Proof state after:
case mp.hg
α : Type u_1
f : Ultrafilter α
s : Set α
hne : ¬sᶜ ∈ f
h : sᶜ ∈ f.as_filter
h' : {x | x ∈ s → x ∈ ∅} = sᶜ
⊢ False
Theorem: FilterGame.Ultrafilter.compl_not_mem_iff
Proof state before:
case mp.hg
α : Type u_1
f : Ultrafilter α
s : Set α
hne : ¬sᶜ ∈ f
h : sᶜ ∈ f.as_filter
h' : {x | x ∈ s → x ∈ ∅} = sᶜ
⊢ False
Tactic:
exact hne h
Proof state after:
no goals
Theorem: FilterGame.Ultrafilter.compl_not_mem_iff
Proof state before:
case mpr
α : Type u_1
f : Ultrafilter α
s : Set α
⊢ s ∈ f → ¬sᶜ ∈ f
Tactic:
exact Filter.compl_not_mem f.ne_bot
Proof state after:
no goals
Theorem: FilterGame.Ultrafilter.compl_mem_iff
Proof state before:
α : Type u_1
f : Ultrafilter α
s : Set α
⊢ sᶜ ∈ f ↔ ¬s ∈ f
Tactic:
rw [← compl_not_mem_iff, compl_compl]
Proof state after:
no goals
Theorem: FilterGame.Filter.mem_inf_def
Proof state before:
α : Type u_1
f g : Filter α
s : Set α
⊢ s ∈ f ⊓ g ↔ ∃ a, a ∈ f ∧ ∃ b, b ∈ g ∧ s = a ∩ b
Tactic:
exact Iff.rfl
Proof state after:
no goals
Theorem: FilterGame.Filter.inter_mem_inf
Proof state before:
α : Type u_1
f g : Filter α
s t : Set α
hs : s ∈ f
ht : t ∈ g
⊢ s ∩ t ∈ f ⊓ g
Tactic:
exact ⟨s, hs, t, ht, rfl⟩
Proof state after:
no goals
Theorem: FilterGame.Filter.mem_inf_principal_iff
Proof state before:
α : Type u_1
f : Filter α
s t : Set α
⊢ s ∈ f ⊓ 𝓟 t ↔ {x | x ∈ t → x ∈ s} ∈ f
Tactic:
apply Iff.intro
Proof state after:
case mp
α : Type u_1
f : Filter α
s t : Set α
⊢ s ∈ f ⊓ 𝓟 t → {x | x ∈ t → x ∈ s} ∈ f

case mpr
α : Type u_1
f : Filter α
s t : Set α
⊢ {x | x ∈ t → x ∈ s} ∈ f → s ∈ f ⊓ 𝓟 t
Theorem: FilterGame.Filter.mem_inf_principal_iff
Proof state before:
case mp
α : Type u_1
f : Filter α
s t : Set α
⊢ s ∈ f ⊓ 𝓟 t → {x | x ∈ t → x ∈ s} ∈ f

case mpr
α : Type u_1
f : Filter α
s t : Set α
⊢ {x | x ∈ t → x ∈ s} ∈ f → s ∈ f ⊓ 𝓟 t
Tactic:
. intros hs
  rw [mem_inf_def] at hs
  have ⟨a, ha, b, hb, hsab⟩ := hs
  clear hs
  rw [hsab]; clear hsab
  rw [mem_principal_def] at hb
  suffices h : a ⊆ {x | x ∈ t → x ∈ a ∩ b}
  . exact superset_mem ha h
  intros x hxa hxt
  exact ⟨hxa, hb hxt⟩
Proof state after:
case mpr
α : Type u_1
f : Filter α
s t : Set α
⊢ {x | x ∈ t → x ∈ s} ∈ f → s ∈ f ⊓ 𝓟 t
Theorem: FilterGame.Filter.mem_inf_principal_iff
Proof state before:
case mpr
α : Type u_1
f : Filter α
s t : Set α
⊢ {x | x ∈ t → x ∈ s} ∈ f → s ∈ f ⊓ 𝓟 t
Tactic:
. intros h
  have heq : {x | x ∈ t → x ∈ s} = tᶜ ∪ s
  . apply Set.ext; intros x
    rw [Set.mem_iff, Set.mem_union, Set.mem_compl_iff, imp_iff_not_or]
  rw [heq] at h; clear heq
  have heq : s = (tᶜ ∪ s) ∩ (t ∪ s) 
  . rw [← Set.union_distrib_right, Set.compl_inter_self, Set.empty_union]
  rw [heq]; clear heq
  refine inter_mem_inf h ?_
  rw [mem_principal_def]
  exact Set.subset_union_left _ _
Proof state after:
no goals
Theorem: FilterGame.Filter.mem_inf_principal_iff
Proof state before:
case mp
α : Type u_1
f : Filter α
s t : Set α
⊢ s ∈ f ⊓ 𝓟 t → {x | x ∈ t → x ∈ s} ∈ f
Tactic:
intros hs
Proof state after:
case mp
α : Type u_1
f : Filter α
s t : Set α
hs : s ∈ f ⊓ 𝓟 t
⊢ {x | x ∈ t → x ∈ s} ∈ f
Theorem: FilterGame.Filter.mem_inf_principal_iff
Proof state before:
case mp
α : Type u_1
f : Filter α
s t : Set α
hs : s ∈ f ⊓ 𝓟 t
⊢ {x | x ∈ t → x ∈ s} ∈ f
Tactic:
rw [mem_inf_def] at hs
Proof state after:
case mp
α : Type u_1
f : Filter α
s t : Set α
hs : ∃ a, a ∈ f ∧ ∃ b, b ∈ 𝓟 t ∧ s = a ∩ b
⊢ {x | x ∈ t → x ∈ s} ∈ f
Theorem: FilterGame.Filter.mem_inf_principal_iff
Proof state before:
case mp
α : Type u_1
f : Filter α
s t : Set α
hs : ∃ a, a ∈ f ∧ ∃ b, b ∈ 𝓟 t ∧ s = a ∩ b
⊢ {x | x ∈ t → x ∈ s} ∈ f
Tactic:
have ⟨a, ha, b, hb, hsab⟩ := hs
Proof state after:
case mp
α : Type u_1
f : Filter α
s t : Set α
hs : ∃ a, a ∈ f ∧ ∃ b, b ∈ 𝓟 t ∧ s = a ∩ b
a : Set α
ha : a ∈ f
b : Set α
hb : b ∈ 𝓟 t
hsab : s = a ∩ b
⊢ {x | x ∈ t → x ∈ s} ∈ f
Theorem: FilterGame.Filter.mem_inf_principal_iff
Proof state before:
case mp
α : Type u_1
f : Filter α
s t : Set α
hs : ∃ a, a ∈ f ∧ ∃ b, b ∈ 𝓟 t ∧ s = a ∩ b
a : Set α
ha : a ∈ f
b : Set α
hb : b ∈ 𝓟 t
hsab : s = a ∩ b
⊢ {x | x ∈ t → x ∈ s} ∈ f
Tactic:
clear hs
Proof state after:
case mp
α : Type u_1
f : Filter α
s t a : Set α
ha : a ∈ f
b : Set α
hb : b ∈ 𝓟 t
hsab : s = a ∩ b
⊢ {x | x ∈ t → x ∈ s} ∈ f
Theorem: FilterGame.Filter.mem_inf_principal_iff
Proof state before:
case mp
α : Type u_1
f : Filter α
s t a : Set α
ha : a ∈ f
b : Set α
hb : b ∈ 𝓟 t
hsab : s = a ∩ b
⊢ {x | x ∈ t → x ∈ s} ∈ f
Tactic:
rw [hsab]
Proof state after:
case mp
α : Type u_1
f : Filter α
s t a : Set α
ha : a ∈ f
b : Set α
hb : b ∈ 𝓟 t
hsab : s = a ∩ b
⊢ {x | x ∈ t → x ∈ a ∩ b} ∈ f
Theorem: FilterGame.Filter.mem_inf_principal_iff
Proof state before:
case mp
α : Type u_1
f : Filter α
s t a : Set α
ha : a ∈ f
b : Set α
hb : b ∈ 𝓟 t
hsab : s = a ∩ b
⊢ {x | x ∈ t → x ∈ a ∩ b} ∈ f
Tactic:
clear hsab
Proof state after:
case mp
α : Type u_1
f : Filter α
s t a : Set α
ha : a ∈ f
b : Set α
hb : b ∈ 𝓟 t
⊢ {x | x ∈ t → x ∈ a ∩ b} ∈ f
Theorem: FilterGame.Filter.mem_inf_principal_iff
Proof state before:
case mp
α : Type u_1
f : Filter α
s t a : Set α
ha : a ∈ f
b : Set α
hb : b ∈ 𝓟 t
⊢ {x | x ∈ t → x ∈ a ∩ b} ∈ f
Tactic:
rw [mem_principal_def] at hb
Proof state after:
case mp
α : Type u_1
f : Filter α
s t a : Set α
ha : a ∈ f
b : Set α
hb : t ⊆ b
⊢ {x | x ∈ t → x ∈ a ∩ b} ∈ f
Theorem: FilterGame.Filter.mem_inf_principal_iff
Proof state before:
case mp
α : Type u_1
f : Filter α
s t a : Set α
ha : a ∈ f
b : Set α
hb : t ⊆ b
⊢ {x | x ∈ t → x ∈ a ∩ b} ∈ f
Tactic:
suffices h : a ⊆ {x | x ∈ t → x ∈ a ∩ b}
Proof state after:
case mp
α : Type u_1
f : Filter α
s t a : Set α
ha : a ∈ f
b : Set α
hb : t ⊆ b
h : a ⊆ {x | x ∈ t → x ∈ a ∩ b}
⊢ {x | x ∈ t → x ∈ a ∩ b} ∈ f

case h
α : Type u_1
f : Filter α
s t a : Set α
ha : a ∈ f
b : Set α
hb : t ⊆ b
⊢ a ⊆ {x | x ∈ t → x ∈ a ∩ b}
Theorem: FilterGame.Filter.mem_inf_principal_iff
Proof state before:
case mp
α : Type u_1
f : Filter α
s t a : Set α
ha : a ∈ f
b : Set α
hb : t ⊆ b
h : a ⊆ {x | x ∈ t → x ∈ a ∩ b}
⊢ {x | x ∈ t → x ∈ a ∩ b} ∈ f

case h
α : Type u_1
f : Filter α
s t a : Set α
ha : a ∈ f
b : Set α
hb : t ⊆ b
⊢ a ⊆ {x | x ∈ t → x ∈ a ∩ b}
Tactic:
. exact superset_mem ha h
Proof state after:
case h
α : Type u_1
f : Filter α
s t a : Set α
ha : a ∈ f
b : Set α
hb : t ⊆ b
⊢ a ⊆ {x | x ∈ t → x ∈ a ∩ b}
Theorem: FilterGame.Filter.mem_inf_principal_iff
Proof state before:
case h
α : Type u_1
f : Filter α
s t a : Set α
ha : a ∈ f
b : Set α
hb : t ⊆ b
⊢ a ⊆ {x | x ∈ t → x ∈ a ∩ b}
Tactic:
intros x hxa hxt
Proof state after:
case h
α : Type u_1
f : Filter α
s t a : Set α
ha : a ∈ f
b : Set α
hb : t ⊆ b
x : α
hxa : x ∈ a
hxt : x ∈ t
⊢ x ∈ a ∩ b
Theorem: FilterGame.Filter.mem_inf_principal_iff
Proof state before:
case h
α : Type u_1
f : Filter α
s t a : Set α
ha : a ∈ f
b : Set α
hb : t ⊆ b
x : α
hxa : x ∈ a
hxt : x ∈ t
⊢ x ∈ a ∩ b
Tactic:
exact ⟨hxa, hb hxt⟩
Proof state after:
no goals
Theorem: FilterGame.Filter.mem_inf_principal_iff
Proof state before:
case mp
α : Type u_1
f : Filter α
s t a : Set α
ha : a ∈ f
b : Set α
hb : t ⊆ b
h : a ⊆ {x | x ∈ t → x ∈ a ∩ b}
⊢ {x | x ∈ t → x ∈ a ∩ b} ∈ f
Tactic:
exact superset_mem ha h
Proof state after:
no goals
Theorem: FilterGame.Filter.mem_inf_principal_iff
Proof state before:
case mpr
α : Type u_1
f : Filter α
s t : Set α
⊢ {x | x ∈ t → x ∈ s} ∈ f → s ∈ f ⊓ 𝓟 t
Tactic:
intros h
Proof state after:
case mpr
α : Type u_1
f : Filter α
s t : Set α
h : {x | x ∈ t → x ∈ s} ∈ f
⊢ s ∈ f ⊓ 𝓟 t
Theorem: FilterGame.Filter.mem_inf_principal_iff
Proof state before:
case mpr
α : Type u_1
f : Filter α
s t : Set α
h : {x | x ∈ t → x ∈ s} ∈ f
⊢ s ∈ f ⊓ 𝓟 t
Tactic:
have heq : {x | x ∈ t → x ∈ s} = tᶜ ∪ s
Proof state after:
case heq
α : Type u_1
f : Filter α
s t : Set α
h : {x | x ∈ t → x ∈ s} ∈ f
⊢ {x | x ∈ t → x ∈ s} = tᶜ ∪ s

case mpr
α : Type u_1
f : Filter α
s t : Set α
h : {x | x ∈ t → x ∈ s} ∈ f
heq : {x | x ∈ t → x ∈ s} = tᶜ ∪ s
⊢ s ∈ f ⊓ 𝓟 t
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

case mpr
α : Type u_1
f : Filter α
s t : Set α
h : {x | x ∈ t → x ∈ s} ∈ f
heq : {x | x ∈ t → x ∈ s} = tᶜ ∪ s
⊢ s ∈ f ⊓ 𝓟 t
Tactic:
. apply Set.ext; intros x
  rw [Set.mem_iff, Set.mem_union, Set.mem_compl_iff, imp_iff_not_or]
Proof state after:
case mpr
α : Type u_1
f : Filter α
s t : Set α
h : {x | x ∈ t → x ∈ s} ∈ f
heq : {x | x ∈ t → x ∈ s} = tᶜ ∪ s
⊢ s ∈ f ⊓ 𝓟 t
Theorem: FilterGame.Filter.mem_inf_principal_iff
Proof state before:
case mpr
α : Type u_1
f : Filter α
s t : Set α
h : {x | x ∈ t → x ∈ s} ∈ f
heq : {x | x ∈ t → x ∈ s} = tᶜ ∪ s
⊢ s ∈ f ⊓ 𝓟 t
Tactic:
rw [heq] at h
Proof state after:
case mpr
α : Type u_1
f : Filter α
s t : Set α
h : tᶜ ∪ s ∈ f
heq : {x | x ∈ t → x ∈ s} = tᶜ ∪ s
⊢ s ∈ f ⊓ 𝓟 t
Theorem: FilterGame.Filter.mem_inf_principal_iff
Proof state before:
case mpr
α : Type u_1
f : Filter α
s t : Set α
h : tᶜ ∪ s ∈ f
heq : {x | x ∈ t → x ∈ s} = tᶜ ∪ s
⊢ s ∈ f ⊓ 𝓟 t
Tactic:
clear heq
Proof state after:
case mpr
α : Type u_1
f : Filter α
s t : Set α
h : tᶜ ∪ s ∈ f
⊢ s ∈ f ⊓ 𝓟 t
Theorem: FilterGame.Filter.mem_inf_principal_iff
Proof state before:
case mpr
α : Type u_1
f : Filter α
s t : Set α
h : tᶜ ∪ s ∈ f
⊢ s ∈ f ⊓ 𝓟 t
Tactic:
have heq : s = (tᶜ ∪ s) ∩ (t ∪ s)
Proof state after:
case heq
α : Type u_1
f : Filter α
s t : Set α
h : tᶜ ∪ s ∈ f
⊢ s = (tᶜ ∪ s) ∩ (t ∪ s)

case mpr
α : Type u_1
f : Filter α
s t : Set α
h : tᶜ ∪ s ∈ f
heq : s = (tᶜ ∪ s) ∩ (t ∪ s)
⊢ s ∈ f ⊓ 𝓟 t
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)

case mpr
α : Type u_1
f : Filter α
s t : Set α
h : tᶜ ∪ s ∈ f
heq : s = (tᶜ ∪ s) ∩ (t ∪ s)
⊢ s ∈ f ⊓ 𝓟 t
Tactic:
. rw [← Set.union_distrib_right, Set.compl_inter_self, Set.empty_union]
Proof state after:
case mpr
α : Type u_1
f : Filter α
s t : Set α
h : tᶜ ∪ s ∈ f
heq : s = (tᶜ ∪ s) ∩ (t ∪ s)
⊢ s ∈ f ⊓ 𝓟 t
Theorem: FilterGame.Filter.mem_inf_principal_iff
Proof state before:
case mpr
α : Type u_1
f : Filter α
s t : Set α
h : tᶜ ∪ s ∈ f
heq : s = (tᶜ ∪ s) ∩ (t ∪ s)
⊢ s ∈ f ⊓ 𝓟 t
Tactic:
rw [heq]
Proof state after:
case mpr
α : Type u_1
f : Filter α
s t : Set α
h : tᶜ ∪ s ∈ f
heq : s = (tᶜ ∪ s) ∩ (t ∪ s)
⊢ (tᶜ ∪ s) ∩ (t ∪ s) ∈ f ⊓ 𝓟 t
Theorem: FilterGame.Filter.mem_inf_principal_iff
Proof state before:
case mpr
α : Type u_1
f : Filter α
s t : Set α
h : tᶜ ∪ s ∈ f
heq : s = (tᶜ ∪ s) ∩ (t ∪ s)
⊢ (tᶜ ∪ s) ∩ (t ∪ s) ∈ f ⊓ 𝓟 t
Tactic:
clear heq
Proof state after:
case mpr
α : Type u_1
f : Filter α
s t : Set α
h : tᶜ ∪ s ∈ f
⊢ (tᶜ ∪ s) ∩ (t ∪ s) ∈ f ⊓ 𝓟 t
Theorem: FilterGame.Filter.mem_inf_principal_iff
Proof state before:
case mpr
α : Type u_1
f : Filter α
s t : Set α
h : tᶜ ∪ s ∈ f
⊢ (tᶜ ∪ s) ∩ (t ∪ s) ∈ f ⊓ 𝓟 t
Tactic:
refine inter_mem_inf h ?_
Proof state after:
case mpr
α : Type u_1
f : Filter α
s t : Set α
h : tᶜ ∪ s ∈ f
⊢ t ∪ s ∈ 𝓟 t
Theorem: FilterGame.Filter.mem_inf_principal_iff
Proof state before:
case mpr
α : Type u_1
f : Filter α
s t : Set α
h : tᶜ ∪ s ∈ f
⊢ t ∪ s ∈ 𝓟 t
Tactic:
rw [mem_principal_def]
Proof state after:
case mpr
α : Type u_1
f : Filter α
s t : Set α
h : tᶜ ∪ s ∈ f
⊢ t ⊆ t ∪ s
Theorem: FilterGame.Filter.mem_inf_principal_iff
Proof state before:
case mpr
α : Type u_1
f : Filter α
s t : Set α
h : tᶜ ∪ s ∈ f
⊢ t ⊆ t ∪ s
Tactic:
exact Set.subset_union_left _ _
Proof state after:
no goals