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

State before:
α : Type u_1
inst✝ : CompleteLattice α
s x y z : α
P✝ P : Partition s
hs : s ≠ ⊥
hP : ↑P = ∅
⊢ False
Tactic:
simp [← P.sSup_eq, hP, sSup_empty] at hs
State after:
no goals