Theorem: FilterGame.Ultrafilter.compl_mem_iff (FilterGame/Solutions/Ultrafilter.lean)

State before:
α : Type u_1
f : Ultrafilter α
s : Set α
⊢ sᶜ ∈ f ↔ ¬s ∈ f
Tactic:
rw [← compl_not_mem_iff, compl_compl]
State after:
no goals