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

State before:
α : Type u_1
⊢ 𝓟 ∅ = ⊥
Tactic:
apply bot_unique
State after:
case h
α : Type u_1
⊢ 𝓟 ∅ ≤ ⊥

State before:
case h
α : Type u_1
⊢ 𝓟 ∅ ≤ ⊥
Tactic:
intros s hs
State after:
case h
α : Type u_1
s : Set α
hs : s ∈ ⊥
⊢ s ∈ 𝓟 ∅

State before:
case h
α : Type u_1
s : Set α
hs : s ∈ ⊥
⊢ s ∈ 𝓟 ∅
Tactic:
exact Set.empty_subset s
State after:
no goals