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

State before:
α : Type u_1
b c : Basis α
⊢ (∀ (s : Set α), s ∈ b ↔ s ∈ c) → b = c
Tactic:
exact (ext_iff _ _).mpr
State after:
no goals