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

State before:
α : Type u_1
s t : Set α
⊢ 𝓟 s ≤ 𝓟 t ↔ s ⊆ t
Tactic:
rw [le_principal_iff, mem_principal_def]
State after:
no goals