Theorem: FilterGame.Basis.ext_iff (FilterGame/Basis.lean)

State before:
α : Type u_1
b c : Basis α
⊢ b = c ↔ ∀ (s : Set α), s ∈ b ↔ s ∈ c
Tactic:
simp_rw [eq_def, mem_def, Set.ext_iff]
State after:
no goals