have hs' : 2 * p - 1 = Fintype.card s.toEnumFinset := by simp [hs]
n p : ℕ
inst✝ : Fact p.Prime
s : Multiset (ZMod p)
hs : Multiset.card s = 2 * p - 1
this : NeZero p
N : ℕ := Fintype.card { x // (eval x) (ZMod.f₁ s) = 0 ∧ (eval x) (ZMod.f₂ s) = 0 }
zero_sol : { x // (eval x) (ZMod.f₁ s) = 0 ∧ (eval x) (ZMod.f₂ s) = 0 } := ⟨0, ⋯⟩
hN₀ : 0 < N
⊢ ∃ t ≤ s, Multiset.card t = p ∧ t.sum = 0
n p : ℕ
inst✝ : Fact p.Prime
s : Multiset (ZMod p)
hs : Multiset.card s = 2 * p - 1
this : NeZero p
N : ℕ := Fintype.card { x // (eval x) (ZMod.f₁ s) = 0 ∧ (eval x) (ZMod.f₂ s) = 0 }
zero_sol : { x // (eval x) (ZMod.f₁ s) = 0 ∧ (eval x) (ZMod.f₂ s) = 0 } := ⟨0, ⋯⟩
hN₀ : 0 < N
hs' : 2 * p - 1 = Fintype.card { x // x ∈ s.toEnumFinset }
⊢ ∃ t ≤ s, Multiset.card t = p ∧ t.sum = 0