Theorem: Multiset.exists_le_card_eq (LeanCamCombi/Mathlib/Data/Multiset/Basic.lean)

State before:
α : Type u_1
s t : Multiset α
n : ℕ
hn : n ≤ card s
⊢ ∃ t ≤ s, card t = n
Tactic:
simpa using exists_intermediate (zero_le _) (Nat.zero_le _) hn
State after:
no goals