exact ⟨u, hut.trans hts, hu⟩
case intro.intro.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
u : Multiset (ZMod p)
hut : u ≤ t
hu : Multiset.card u = p ∧ u.sum = 0
⊢ ∃ t ≤ s, Multiset.card t = p ∧ t.sum = 0
no goals