α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P✝ P : Finpartition s
⊢ card P.parts ≤ card ⊥.parts
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P✝ P : Finpartition s
⊢ card P.parts ≤ card s
rw [← card_bot s]
no goals
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P✝ P : Finpartition s
⊢ card P.parts ≤ card ⊥.parts
exact card_mono bot_le