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

State before:
α : Type u_1
s t : Set α
⊢ 𝓟 s = 𝓟 t ↔ s = t
Tactic:
simp only [le_antisymm_iff, le_principal_iff, mem_principal_def]
State after:
α : Type u_1
s t : Set α
⊢ s ⊆ t ∧ t ⊆ s ↔ s ≤ t ∧ t ≤ s

State before:
α : Type u_1
s t : Set α
⊢ s ⊆ t ∧ t ⊆ s ↔ s ≤ t ∧ t ≤ s
Tactic:
rfl
State after:
no goals