Theorem: Partition.parts_top_subset (Matroid/ForMathlib/SetPartition.lean)

State before:
α✝ : Type u_1
inst✝¹ : CompleteLattice α✝
s✝ x y z : α✝
α : Type u_2
inst✝ : CompleteLattice α
s : α
⊢ ↑⊤ ⊆ {s}
Tactic:
simp
State after:
no goals