Theorem: FilterGame.Basis.le_and_le_iff_filter_eq (FilterGame/Order.lean)

State before:
α : Type u_1
b c : Basis α
⊢ b ≤' c ∧ c ≤' b ↔ as_filter b = as_filter c
Tactic:
sorry
State after:
no goals