rw [← Subtype.coe_ne_coe, Function.ne_iff] at hx
case intro.refine_2.refine_1
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 }
hpN : p ∣ N
x : { x // (eval x) (ZMod.f₁ s) = 0 ∧ (eval x) (ZMod.f₂ s) = 0 }
hx : x ≠ zero_sol
⊢ (Finset.filter (fun a => ↑x a ≠ 0) s.toEnumFinset.attach).Nonempty
case intro.refine_2.refine_1
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 }
hpN : p ∣ N
x : { x // (eval x) (ZMod.f₁ s) = 0 ∧ (eval x) (ZMod.f₂ s) = 0 }
hx : ∃ a, ↑x a ≠ ↑zero_sol a
⊢ (Finset.filter (fun a => ↑x a ≠ 0) s.toEnumFinset.attach).Nonempty