Theorem: FilterGame.Filter.compl_not_mem (FilterGame/Solutions/Principal.lean)

State before:
α : Type u_1
f : Filter α
s : Set α
hf : f ≠ ⊥
h : s ∈ f
⊢ ¬sᶜ ∈ f
Tactic:
intros h'
State after:
α : Type u_1
f : Filter α
s : Set α
hf : f ≠ ⊥
h : s ∈ f
h' : sᶜ ∈ f
⊢ False

State before:
α : Type u_1
f : Filter α
s : Set α
hf : f ≠ ⊥
h : s ∈ f
h' : sᶜ ∈ f
⊢ False
Tactic:
apply hf
State after:
α : Type u_1
f : Filter α
s : Set α
hf : f ≠ ⊥
h : s ∈ f
h' : sᶜ ∈ f
⊢ f = ⊥

State before:
α : Type u_1
f : Filter α
s : Set α
hf : f ≠ ⊥
h : s ∈ f
h' : sᶜ ∈ f
⊢ f = ⊥
Tactic:
rw [← empty_mem_iff_eq_bot, ← Set.compl_inter_self s]
State after:
α : Type u_1
f : Filter α
s : Set α
hf : f ≠ ⊥
h : s ∈ f
h' : sᶜ ∈ f
⊢ sᶜ ∩ s ∈ f

State before:
α : Type u_1
f : Filter α
s : Set α
hf : f ≠ ⊥
h : s ∈ f
h' : sᶜ ∈ f
⊢ sᶜ ∩ s ∈ f
Tactic:
exact inter_mem h' h
State after:
no goals