Theorem: FilterGame.Filter.mem_top_iff_eq_univ (FilterGame/Solutions/Principal.lean)

State before:
α : Type u_1
s : Set α
⊢ s ∈ ⊤ ↔ s = Set.univ
Tactic:
rw [mem_top_def, Set.eq_univ_iff_forall]
State after:
no goals