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

State before:
α : Type u_1
s : Set α
⊢ s ∈ 𝓟 s
Tactic:
exact (mem_principal_def _ _).mpr subset_rfl
State after:
no goals