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

State before:
α : Type u_1
f : Ultrafilter α
s : Set α
⊢ s ∈ f.as_filter ↔ s ∈ f
Tactic:
exact Iff.rfl
State after:
no goals