Theorem: ZMod.aux (LeanCamCombi/ErdosGinzburgZiv.lean)

State before:
n p : ℕ
inst✝ : Fact p.Prime
s : Multiset (ZMod p)
hs : Multiset.card s = 2 * p - 1
⊢ ∃ t ≤ s, Multiset.card t = p ∧ t.sum = 0
Tactic:
haveI : NeZero p := inferInstance
State after:
n p : ℕ
inst✝ : Fact p.Prime
s : Multiset (ZMod p)
hs : Multiset.card s = 2 * p - 1
this : NeZero p
⊢ ∃ t ≤ s, Multiset.card t = p ∧ t.sum = 0

State before:
n p : ℕ
inst✝ : Fact p.Prime
s : Multiset (ZMod p)
hs : Multiset.card s = 2 * p - 1
this : NeZero p
⊢ ∃ t ≤ s, Multiset.card t = p ∧ t.sum = 0
Tactic:
set N := Fintype.card {x // eval x (f₁ s) = 0 ∧ eval x (f₂ s) = 0}
State after:
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 }
⊢ ∃ t ≤ s, Multiset.card t = p ∧ t.sum = 0

State before:
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 }
⊢ ∃ t ≤ s, Multiset.card t = p ∧ t.sum = 0
Tactic:
let zero_sol : {x // eval x (f₁ s) = 0 ∧ eval x (f₂ s) = 0} :=
  ⟨0, by simp [f₁, f₂, map_sum, (Fact.out : p.Prime).one_lt, tsub_eq_zero_iff_le]⟩
State after:
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, ⋯⟩
⊢ ∃ t ≤ s, Multiset.card t = p ∧ t.sum = 0

State before:
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, ⋯⟩
⊢ ∃ t ≤ s, Multiset.card t = p ∧ t.sum = 0
Tactic:
have hN₀ : 0 < N := @Fintype.card_pos _ _ ⟨zero_sol⟩
State after:
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

State before:
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
Tactic:
have hs' : 2 * p - 1 = Fintype.card s.toEnumFinset := by simp [hs]
State after:
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

State before:
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
Tactic:
have hpN : p ∣ N := char_dvd_card_solutions_of_add_lt p
  (totalDegree_f₁_add_totalDegree_f₂.trans_eq hs')
State after:
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
⊢ ∃ t ≤ s, Multiset.card t = p ∧ t.sum = 0

State before:
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
⊢ ∃ t ≤ s, Multiset.card t = p ∧ t.sum = 0
Tactic:
obtain ⟨x, hx⟩ := Fintype.exists_ne_of_one_lt_card ((Fact.out : p.Prime).one_lt.trans_le $
  Nat.le_of_dvd hN₀ hpN) zero_sol
State after:
case intro
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
⊢ ∃ t ≤ s, Multiset.card t = p ∧ t.sum = 0

State before:
case intro
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
⊢ ∃ t ≤ s, Multiset.card t = p ∧ t.sum = 0
Tactic:
refine ⟨(s.toEnumFinset.attach.filter $ fun a ↦ x.1 a ≠ 0).1.map
  (Prod.fst ∘ ((↑) : s.toEnumFinset → ZMod p × ℕ)), le_iff_count.2 $ fun a ↦ ?_, ?_, ?_⟩
State after:
case intro.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
a : ZMod p
⊢ count a (Multiset.map (Prod.fst ∘ Subtype.val) (Finset.filter (fun a => ↑x a ≠ 0) s.toEnumFinset.attach).val) ≤
    count a s

case intro.refine_2
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
⊢ Multiset.card (Multiset.map (Prod.fst ∘ Subtype.val) (Finset.filter (fun a => ↑x a ≠ 0) s.toEnumFinset.attach).val) =
    p

case intro.refine_3
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
⊢ (Multiset.map (Prod.fst ∘ Subtype.val) (Finset.filter (fun a => ↑x a ≠ 0) s.toEnumFinset.attach).val).sum = 0

State before:
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 }
⊢ (eval 0) (ZMod.f₁ s) = 0 ∧ (eval 0) (ZMod.f₂ s) = 0
Tactic:
simp [f₁, f₂, map_sum, (Fact.out : p.Prime).one_lt, tsub_eq_zero_iff_le]
State after:
no goals

State before:
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
⊢ 2 * p - 1 = Fintype.card { x // x ∈ s.toEnumFinset }
Tactic:
simp [hs]
State after:
no goals

State before:
case intro.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
a : ZMod p
⊢ count a (Multiset.map (Prod.fst ∘ Subtype.val) (Finset.filter (fun a => ↑x a ≠ 0) s.toEnumFinset.attach).val) ≤
    count a s
Tactic:
simp only [← Finset.filter_val, Finset.card_val, Function.comp_apply, count_map]
State after:
case intro.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
a : ZMod p
⊢ (Finset.filter (fun a_1 => a = (↑a_1).1) (Finset.filter (fun a => ↑x a ≠ 0) s.toEnumFinset.attach)).card ≤ count a s

State before:
case intro.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
a : ZMod p
⊢ (Finset.filter (fun a_1 => a = (↑a_1).1) (Finset.filter (fun a => ↑x a ≠ 0) s.toEnumFinset.attach)).card ≤ count a s
Tactic:
refine (Finset.card_le_card $ Finset.filter_subset_filter _ $
  Finset.filter_subset _ _).trans_eq ?_
State after:
case intro.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
a : ZMod p
⊢ (Finset.filter (fun a_1 => a = (↑a_1).1) s.toEnumFinset.attach).card = count a s

State before:
case intro.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
a : ZMod p
⊢ (Finset.filter (fun a_1 => a = (↑a_1).1) s.toEnumFinset.attach).card = count a s
Tactic:
refine (Finset.card_filter_attach (fun c : ZMod p × ℕ ↦ a = c.1) _).trans ?_
State after:
case intro.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
a : ZMod p
⊢ (Finset.filter (fun c => a = c.1) s.toEnumFinset).card = count a s

State before:
case intro.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
a : ZMod p
⊢ (Finset.filter (fun c => a = c.1) s.toEnumFinset).card = count a s
Tactic:
simp [toEnumFinset_filter_eq]
State after:
no goals

State before:
case intro.refine_2
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
⊢ Multiset.card (Multiset.map (Prod.fst ∘ Subtype.val) (Finset.filter (fun a => ↑x a ≠ 0) s.toEnumFinset.attach).val) =
    p
Tactic:
simp only [card_map, ← Finset.filter_val, Finset.card_val, Function.comp_apply,
  count_map, ← Finset.map_val]
State after:
case intro.refine_2
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).card = p

State before:
case intro.refine_2
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).card = p
Tactic:
refine Nat.eq_of_dvd_of_lt_two_mul (Finset.card_pos.2 ?_).ne' ?_ $
  (Finset.card_filter_le _ _).trans_lt ?_
State after:
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_2
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
⊢ p ∣ (Finset.filter (fun a => ↑x a ≠ 0) s.toEnumFinset.attach).card

case intro.refine_2.refine_3
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
⊢ s.toEnumFinset.attach.card < 2 * p

State before:
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
Tactic:
rw [← Subtype.coe_ne_coe, Function.ne_iff] at hx
State after:
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

State before:
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
Tactic:
exact hx.imp (fun a ha ↦ mem_filter.2 ⟨Finset.mem_attach _ _, ha⟩)
State after:
no goals

State before:
case intro.refine_2.refine_2
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
⊢ p ∣ (Finset.filter (fun a => ↑x a ≠ 0) s.toEnumFinset.attach).card
Tactic:
rw [← CharP.cast_eq_zero_iff (ZMod p), ← Finset.sum_boole]
State after:
case intro.refine_2.refine_2
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
⊢ (∑ x_1 ∈ s.toEnumFinset.attach, if ↑x x_1 ≠ 0 then 1 else 0) = 0

State before:
case intro.refine_2.refine_2
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
⊢ (∑ x_1 ∈ s.toEnumFinset.attach, if ↑x x_1 ≠ 0 then 1 else 0) = 0
Tactic:
simpa only [f₁, map_sum, ZMod.pow_card_sub_one, map_pow, eval_X] using x.2.1
State after:
no goals

State before:
case intro.refine_2.refine_3
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
⊢ s.toEnumFinset.attach.card < 2 * p
Tactic:
rw [Finset.card_attach, card_toEnumFinset, hs]
State after:
case intro.refine_2.refine_3
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
⊢ 2 * p - 1 < 2 * p

State before:
case intro.refine_2.refine_3
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
⊢ 2 * p - 1 < 2 * p
Tactic:
exact tsub_lt_self (mul_pos zero_lt_two (Fact.out : p.Prime).pos) zero_lt_one
State after:
no goals

State before:
case intro.refine_3
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
⊢ (Multiset.map (Prod.fst ∘ Subtype.val) (Finset.filter (fun a => ↑x a ≠ 0) s.toEnumFinset.attach).val).sum = 0
Tactic:
simpa only [f₂, map_sum, ZMod.pow_card_sub_one, Finset.sum_map_val, Finset.sum_filter,
  smul_eval, map_pow, eval_X, mul_ite, mul_zero, mul_one] using x.2.2
State after:
no goals