Theorem: FilterGame.Basis.as_filter_le (FilterGame/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:
sorry
State after:
no goals