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

State before:
α : Type u_1
⊢ 𝓟 Set.univ = ⊤
Tactic:
apply top_unique
State after:
case h
α : Type u_1
⊢ ⊤ ≤ 𝓟 Set.univ

State before:
case h
α : Type u_1
⊢ ⊤ ≤ 𝓟 Set.univ
Tactic:
rw [le_principal_iff, mem_top_def]
State after:
case h
α : Type u_1
⊢ ∀ (x : α), x ∈ Set.univ

State before:
case h
α : Type u_1
⊢ ∀ (x : α), x ∈ Set.univ
Tactic:
intros x
State after:
case h
α : Type u_1
x : α
⊢ x ∈ Set.univ

State before:
case h
α : Type u_1
x : α
⊢ x ∈ Set.univ
Tactic:
exact True.intro
State after:
no goals