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

State before:
α : Type u_1
f : Filter α
⊢ ∅ ∈ f ↔ f = ⊥
Tactic:
apply Iff.intro
State after:
case mp
α : Type u_1
f : Filter α
⊢ ∅ ∈ f → f = ⊥

case mpr
α : Type u_1
f : Filter α
⊢ f = ⊥ → ∅ ∈ f

State before:
case mp
α : Type u_1
f : Filter α
⊢ ∅ ∈ f → f = ⊥

case mpr
α : Type u_1
f : Filter α
⊢ f = ⊥ → ∅ ∈ f
Tactic:
. intros h
  apply ext
  intros s
  apply Iff.intro
  . intros _; exact True.intro
  . intros _; exact superset_mem h (Set.empty_subset _)
State after:
case mpr
α : Type u_1
f : Filter α
⊢ f = ⊥ → ∅ ∈ f

State before:
case mpr
α : Type u_1
f : Filter α
⊢ f = ⊥ → ∅ ∈ f
Tactic:
. intros h
  rw [h]
  exact Set.mem_univ _
State after:
no goals

State before:
case mp
α : Type u_1
f : Filter α
⊢ ∅ ∈ f → f = ⊥
Tactic:
intros h
State after:
case mp
α : Type u_1
f : Filter α
h : ∅ ∈ f
⊢ f = ⊥

State before:
case mp
α : Type u_1
f : Filter α
h : ∅ ∈ f
⊢ f = ⊥
Tactic:
apply ext
State after:
case mp.a
α : Type u_1
f : Filter α
h : ∅ ∈ f
⊢ ∀ (s : Set α), s ∈ f ↔ s ∈ ⊥

State before:
case mp.a
α : Type u_1
f : Filter α
h : ∅ ∈ f
⊢ ∀ (s : Set α), s ∈ f ↔ s ∈ ⊥
Tactic:
intros s
State after:
case mp.a
α : Type u_1
f : Filter α
h : ∅ ∈ f
s : Set α
⊢ s ∈ f ↔ s ∈ ⊥

State before:
case mp.a
α : Type u_1
f : Filter α
h : ∅ ∈ f
s : Set α
⊢ s ∈ f ↔ s ∈ ⊥
Tactic:
apply Iff.intro
State after:
case mp.a.mp
α : Type u_1
f : Filter α
h : ∅ ∈ f
s : Set α
⊢ s ∈ f → s ∈ ⊥

case mp.a.mpr
α : Type u_1
f : Filter α
h : ∅ ∈ f
s : Set α
⊢ s ∈ ⊥ → s ∈ f

State before:
case mp.a.mp
α : Type u_1
f : Filter α
h : ∅ ∈ f
s : Set α
⊢ s ∈ f → s ∈ ⊥

case mp.a.mpr
α : Type u_1
f : Filter α
h : ∅ ∈ f
s : Set α
⊢ s ∈ ⊥ → s ∈ f
Tactic:
. intros _; exact True.intro
State after:
case mp.a.mpr
α : Type u_1
f : Filter α
h : ∅ ∈ f
s : Set α
⊢ s ∈ ⊥ → s ∈ f

State before:
case mp.a.mpr
α : Type u_1
f : Filter α
h : ∅ ∈ f
s : Set α
⊢ s ∈ ⊥ → s ∈ f
Tactic:
. intros _; exact superset_mem h (Set.empty_subset _)
State after:
no goals

State before:
case mp.a.mp
α : Type u_1
f : Filter α
h : ∅ ∈ f
s : Set α
⊢ s ∈ f → s ∈ ⊥
Tactic:
intros _
State after:
case mp.a.mp
α : Type u_1
f : Filter α
h : ∅ ∈ f
s : Set α
a✝ : s ∈ f
⊢ s ∈ ⊥

State before:
case mp.a.mp
α : Type u_1
f : Filter α
h : ∅ ∈ f
s : Set α
a✝ : s ∈ f
⊢ s ∈ ⊥
Tactic:
exact True.intro
State after:
no goals

State before:
case mp.a.mpr
α : Type u_1
f : Filter α
h : ∅ ∈ f
s : Set α
⊢ s ∈ ⊥ → s ∈ f
Tactic:
intros _
State after:
case mp.a.mpr
α : Type u_1
f : Filter α
h : ∅ ∈ f
s : Set α
a✝ : s ∈ ⊥
⊢ s ∈ f

State before:
case mp.a.mpr
α : Type u_1
f : Filter α
h : ∅ ∈ f
s : Set α
a✝ : s ∈ ⊥
⊢ s ∈ f
Tactic:
exact superset_mem h (Set.empty_subset _)
State after:
no goals

State before:
case mpr
α : Type u_1
f : Filter α
⊢ f = ⊥ → ∅ ∈ f
Tactic:
intros h
State after:
case mpr
α : Type u_1
f : Filter α
h : f = ⊥
⊢ ∅ ∈ f

State before:
case mpr
α : Type u_1
f : Filter α
h : f = ⊥
⊢ ∅ ∈ f
Tactic:
rw [h]
State after:
case mpr
α : Type u_1
f : Filter α
h : f = ⊥
⊢ ∅ ∈ ⊥

State before:
case mpr
α : Type u_1
f : Filter α
h : f = ⊥
⊢ ∅ ∈ ⊥
Tactic:
exact Set.mem_univ _
State after:
no goals