Theorem: FilterGame.Ultrafilter.compl_not_mem_iff (FilterGame/Solutions/Ultrafilter.lean)

State before:
α : Type u_1
f : Ultrafilter α
s : Set α
⊢ ¬sᶜ ∈ f ↔ s ∈ f
Tactic:
apply Iff.intro
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

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]
State after:
case mpr
α : Type u_1
f : Ultrafilter α
s : Set α
⊢ s ∈ f → ¬sᶜ ∈ f

State before:
case mpr
α : Type u_1
f : Ultrafilter α
s : Set α
⊢ s ∈ f → ¬sᶜ ∈ f
Tactic:
. exact Filter.compl_not_mem f.ne_bot
State after:
no goals

State before:
case mp
α : Type u_1
f : Ultrafilter α
s : Set α
⊢ ¬sᶜ ∈ f → s ∈ f
Tactic:
intros hne
State after:
case mp
α : Type u_1
f : Ultrafilter α
s : Set α
hne : ¬sᶜ ∈ f
⊢ s ∈ f

State before:
case mp
α : Type u_1
f : Ultrafilter α
s : Set α
hne : ¬sᶜ ∈ f
⊢ s ∈ f
Tactic:
rw [← mem_coe, ← Filter.le_principal_iff]
State after:
case mp
α : Type u_1
f : Ultrafilter α
s : Set α
hne : ¬sᶜ ∈ f
⊢ f.as_filter ≤ 𝓟 s

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
State after:
case mp.hg
α : Type u_1
f : Ultrafilter α
s : Set α
hne : ¬sᶜ ∈ f
⊢ f.as_filter ⊓ 𝓟 s ≠ ⊥

State before:
case mp.hg
α : Type u_1
f : Ultrafilter α
s : Set α
hne : ¬sᶜ ∈ f
⊢ f.as_filter ⊓ 𝓟 s ≠ ⊥
Tactic:
intros h
State after:
case mp.hg
α : Type u_1
f : Ultrafilter α
s : Set α
hne : ¬sᶜ ∈ f
h : f.as_filter ⊓ 𝓟 s = ⊥
⊢ False

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
State after:
case mp.hg
α : Type u_1
f : Ultrafilter α
s : Set α
hne : ¬sᶜ ∈ f
h : {x | x ∈ s → x ∈ ∅} ∈ f.as_filter
⊢ False

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ᶜ
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ᶜ

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
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ᶜ

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
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ᶜ

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
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ᶜ

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]
State after:
no goals

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
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

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
State after:
no goals

State before:
case mpr
α : Type u_1
f : Ultrafilter α
s : Set α
⊢ s ∈ f → ¬sᶜ ∈ f
Tactic:
exact Filter.compl_not_mem f.ne_bot
State after:
no goals