Theorem: FilterGame.Set.mem_iff (FilterGame/Filter.lean)

State before:
α : Type u_1
p : α → Prop
y : α
⊢ y ∈ {x | p x} ↔ p y
Tactic:
exact Iff.rfl
State after:
no goals