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

State before:
α : Type u_1
s : Set α
f : Filter α
⊢ f ≤ 𝓟 s ↔ s ∈ f
Tactic:
apply Iff.intro
State after:
case mp
α : Type u_1
s : Set α
f : Filter α
⊢ f ≤ 𝓟 s → s ∈ f

case mpr
α : Type u_1
s : Set α
f : Filter α
⊢ s ∈ f → f ≤ 𝓟 s

State before:
case mp
α : Type u_1
s : Set α
f : Filter α
⊢ f ≤ 𝓟 s → s ∈ f

case mpr
α : Type u_1
s : Set α
f : Filter α
⊢ s ∈ f → f ≤ 𝓟 s
Tactic:
. intros h
  exact h _ (mem_principal_self s)
State after:
case mpr
α : Type u_1
s : Set α
f : Filter α
⊢ s ∈ f → f ≤ 𝓟 s

State before:
case mpr
α : Type u_1
s : Set α
f : Filter α
⊢ s ∈ f → f ≤ 𝓟 s
Tactic:
. intros h t ht
  rw [mem_principal_def] at ht
  exact superset_mem h ht
State after:
no goals

State before:
case mp
α : Type u_1
s : Set α
f : Filter α
⊢ f ≤ 𝓟 s → s ∈ f
Tactic:
intros h
State after:
case mp
α : Type u_1
s : Set α
f : Filter α
h : f ≤ 𝓟 s
⊢ s ∈ f

State before:
case mp
α : Type u_1
s : Set α
f : Filter α
h : f ≤ 𝓟 s
⊢ s ∈ f
Tactic:
exact h _ (mem_principal_self s)
State after:
no goals

State before:
case mpr
α : Type u_1
s : Set α
f : Filter α
⊢ s ∈ f → f ≤ 𝓟 s
Tactic:
intros h t ht
State after:
case mpr
α : Type u_1
s : Set α
f : Filter α
h : s ∈ f
t : Set α
ht : t ∈ 𝓟 s
⊢ t ∈ f

State before:
case mpr
α : Type u_1
s : Set α
f : Filter α
h : s ∈ f
t : Set α
ht : t ∈ 𝓟 s
⊢ t ∈ f
Tactic:
rw [mem_principal_def] at ht
State after:
case mpr
α : Type u_1
s : Set α
f : Filter α
h : s ∈ f
t : Set α
ht : s ⊆ t
⊢ t ∈ f

State before:
case mpr
α : Type u_1
s : Set α
f : Filter α
h : s ∈ f
t : Set α
ht : s ⊆ t
⊢ t ∈ f
Tactic:
exact superset_mem h ht
State after:
no goals