obtain ⟨t, hts, ht⟩ := exists_le_card_eq hs
n p✝ : ℕ
inst✝ : Fact p✝.Prime
s✝ : Multiset (ZMod p✝)
p : ℕ
hp : p.Prime
s : Multiset (ZMod p)
hs : 2 * p - 1 ≤ Multiset.card s
this : Fact p.Prime
⊢ ∃ t ≤ s, Multiset.card t = p ∧ t.sum = 0
case intro.intro
n p✝ : ℕ
inst✝ : Fact p✝.Prime
s✝ : Multiset (ZMod p✝)
p : ℕ
hp : p.Prime
s : Multiset (ZMod p)
hs : 2 * p - 1 ≤ Multiset.card s
this : Fact p.Prime
t : Multiset (ZMod p)
hts : t ≤ s
ht : Multiset.card t = 2 * p - 1
⊢ ∃ t ≤ s, Multiset.card t = p ∧ t.sum = 0