Theorem: FilterGame.Filter.as_basis_le_iff (FilterGame/Solutions/Order.lean)

State before:
α : Type u_1
f : Filter α
b : Basis α
⊢ as_basis f ≤' b ↔ f ≤ Basis.as_filter b
Tactic:
apply Iff.intro
State after:
case mp
α : Type u_1
f : Filter α
b : Basis α
⊢ as_basis f ≤' b → f ≤ Basis.as_filter b

case mpr
α : Type u_1
f : Filter α
b : Basis α
⊢ f ≤ Basis.as_filter b → as_basis f ≤' b

State before:
case mp
α : Type u_1
f : Filter α
b : Basis α
⊢ as_basis f ≤' b → f ≤ Basis.as_filter b

case mpr
α : Type u_1
f : Filter α
b : Basis α
⊢ f ≤ Basis.as_filter b → as_basis f ≤' b
Tactic:
. intros h
  rw [← as_basis_as_filter_eq_self f]
  exact Basis.as_filter_le h
State after:
case mpr
α : Type u_1
f : Filter α
b : Basis α
⊢ f ≤ Basis.as_filter b → as_basis f ≤' b

State before:
case mpr
α : Type u_1
f : Filter α
b : Basis α
⊢ f ≤ Basis.as_filter b → as_basis f ≤' b
Tactic:
. intros h
  rw [Basis.le_def]
  intros s hs
  have hs' := h s (Basis.mem_as_filter_of_mem hs)
  exact ⟨s, hs', subset_rfl⟩
State after:
no goals

State before:
case mp
α : Type u_1
f : Filter α
b : Basis α
⊢ as_basis f ≤' b → f ≤ Basis.as_filter b
Tactic:
intros h
State after:
case mp
α : Type u_1
f : Filter α
b : Basis α
h : as_basis f ≤' b
⊢ f ≤ Basis.as_filter b

State before:
case mp
α : Type u_1
f : Filter α
b : Basis α
h : as_basis f ≤' b
⊢ f ≤ Basis.as_filter b
Tactic:
rw [← as_basis_as_filter_eq_self f]
State after:
case mp
α : Type u_1
f : Filter α
b : Basis α
h : as_basis f ≤' b
⊢ Basis.as_filter (as_basis f) ≤ Basis.as_filter b

State before:
case mp
α : Type u_1
f : Filter α
b : Basis α
h : as_basis f ≤' b
⊢ Basis.as_filter (as_basis f) ≤ Basis.as_filter b
Tactic:
exact Basis.as_filter_le h
State after:
no goals

State before:
case mpr
α : Type u_1
f : Filter α
b : Basis α
⊢ f ≤ Basis.as_filter b → as_basis f ≤' b
Tactic:
intros h
State after:
case mpr
α : Type u_1
f : Filter α
b : Basis α
h : f ≤ Basis.as_filter b
⊢ as_basis f ≤' b

State before:
case mpr
α : Type u_1
f : Filter α
b : Basis α
h : f ≤ Basis.as_filter b
⊢ as_basis f ≤' b
Tactic:
rw [Basis.le_def]
State after:
case mpr
α : Type u_1
f : Filter α
b : Basis α
h : f ≤ Basis.as_filter b
⊢ ∀ (s : Set α), s ∈ b → ∃ t, t ∈ as_basis f ∧ t ⊆ s

State before:
case mpr
α : Type u_1
f : Filter α
b : Basis α
h : f ≤ Basis.as_filter b
⊢ ∀ (s : Set α), s ∈ b → ∃ t, t ∈ as_basis f ∧ t ⊆ s
Tactic:
intros s hs
State after:
case mpr
α : Type u_1
f : Filter α
b : Basis α
h : f ≤ Basis.as_filter b
s : Set α
hs : s ∈ b
⊢ ∃ t, t ∈ as_basis f ∧ t ⊆ s

State before:
case mpr
α : Type u_1
f : Filter α
b : Basis α
h : f ≤ Basis.as_filter b
s : Set α
hs : s ∈ b
⊢ ∃ t, t ∈ as_basis f ∧ t ⊆ s
Tactic:
have hs' := h s (Basis.mem_as_filter_of_mem hs)
State after:
case mpr
α : Type u_1
f : Filter α
b : Basis α
h : f ≤ Basis.as_filter b
s : Set α
hs : s ∈ b
hs' : s ∈ f
⊢ ∃ t, t ∈ as_basis f ∧ t ⊆ s

State before:
case mpr
α : Type u_1
f : Filter α
b : Basis α
h : f ≤ Basis.as_filter b
s : Set α
hs : s ∈ b
hs' : s ∈ f
⊢ ∃ t, t ∈ as_basis f ∧ t ⊆ s
Tactic:
exact ⟨s, hs', subset_rfl⟩
State after:
no goals