Theorem: FilterGame.Basis.as_filter_le (FilterGame/Solutions/Order.lean)

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

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

State before:
α : Type u_1
b c : Basis α
h : ∀ (s : Set α), s ∈ c → ∃ t, t ∈ b ∧ t ⊆ s
s : Set α
hs : s ∈ as_filter c
⊢ s ∈ as_filter b
Tactic:
have ⟨t, ht⟩ := hs
State after:
α : Type u_1
b c : Basis α
h : ∀ (s : Set α), s ∈ c → ∃ t, t ∈ b ∧ t ⊆ s
s : Set α
hs : s ∈ as_filter c
t : Set α
ht : t ∈ c ∧ t ⊆ s
⊢ s ∈ as_filter b

State before:
α : Type u_1
b c : Basis α
h : ∀ (s : Set α), s ∈ c → ∃ t, t ∈ b ∧ t ⊆ s
s : Set α
hs : s ∈ as_filter c
t : Set α
ht : t ∈ c ∧ t ⊆ s
⊢ s ∈ as_filter b
Tactic:
have ⟨u, hu⟩ := h t ht.1
State after:
α : Type u_1
b c : Basis α
h : ∀ (s : Set α), s ∈ c → ∃ t, t ∈ b ∧ t ⊆ s
s : Set α
hs : s ∈ as_filter c
t : Set α
ht : t ∈ c ∧ t ⊆ s
u : Set α
hu : u ∈ b ∧ u ⊆ t
⊢ s ∈ as_filter b

State before:
α : Type u_1
b c : Basis α
h : ∀ (s : Set α), s ∈ c → ∃ t, t ∈ b ∧ t ⊆ s
s : Set α
hs : s ∈ as_filter c
t : Set α
ht : t ∈ c ∧ t ⊆ s
u : Set α
hu : u ∈ b ∧ u ⊆ t
⊢ s ∈ as_filter b
Tactic:
exact ⟨u, hu.1, subset_trans hu.2 ht.2⟩
State after:
no goals