internlm/Lean-Github huggingface dataset:
Theorem: ZMod.aux
Proof 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
Proof 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
Theorem: ZMod.aux
Proof 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 ↦ ?_, ?_, ?_⟩
Proof 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
Theorem: ZMod.aux
Proof 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]
Proof state after:
no goals
Theorem: ZMod.aux
Proof 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]
Proof state after:
no goals
Theorem: ZMod.aux
Proof 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]
Proof 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
Theorem: ZMod.aux
Proof 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 ?_
Proof 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
Theorem: ZMod.aux
Proof 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 ?_
Proof 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
Theorem: ZMod.aux
Proof 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]
Proof state after:
no goals
Theorem: ZMod.aux
Proof 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]
Proof 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
Theorem: ZMod.aux
Proof 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 ?_
Proof 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
Theorem: ZMod.aux
Proof 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
Proof 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
Theorem: ZMod.aux
Proof 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⟩)
Proof state after:
no goals
Theorem: ZMod.aux
Proof 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]
Proof 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
Theorem: ZMod.aux
Proof 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
Proof state after:
no goals
Theorem: ZMod.aux
Proof 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]
Proof 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
Theorem: ZMod.aux
Proof 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
Proof state after:
no goals
Theorem: ZMod.aux
Proof 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
Proof state after:
no goals
Theorem: ZMod.exists_submultiset_eq_zero
Proof state before:
n p : ℕ
inst✝ : Fact p.Prime
s✝ : Multiset (ZMod p)
s : Multiset (ZMod n)
hs : 2 * n - 1 ≤ Multiset.card s
⊢ ∃ t ≤ s, Multiset.card t = n ∧ t.sum = 0
Tactic:
induction n using Nat.prime_composite_induction
Proof state after:
case zero
n p : ℕ
inst✝ : Fact p.Prime
s✝ : Multiset (ZMod p)
s : Multiset (ZMod 0)
hs : 2 * 0 - 1 ≤ Multiset.card s
⊢ ∃ t ≤ s, Multiset.card t = 0 ∧ t.sum = 0

case one
n p : ℕ
inst✝ : Fact p.Prime
s✝ : Multiset (ZMod p)
s : Multiset (ZMod 1)
hs : 2 * 1 - 1 ≤ Multiset.card s
⊢ ∃ t ≤ s, Multiset.card t = 1 ∧ t.sum = 0

case prime
n p : ℕ
inst✝ : Fact p.Prime
s✝ : Multiset (ZMod p)
p✝ : ℕ
a✝ : p✝.Prime
s : Multiset (ZMod p✝)
hs : 2 * p✝ - 1 ≤ Multiset.card s
⊢ ∃ t ≤ s, Multiset.card t = p✝ ∧ t.sum = 0

case composite
n p : ℕ
inst✝ : Fact p.Prime
s✝ : Multiset (ZMod p)
a✝⁴ : ℕ
a✝³ : 2 ≤ a✝⁴
a✝² : ∀ {s : Multiset (ZMod a✝⁴)}, 2 * a✝⁴ - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = a✝⁴ ∧ t.sum = 0
b✝ : ℕ
a✝¹ : 2 ≤ b✝
a✝ : ∀ {s : Multiset (ZMod b✝)}, 2 * b✝ - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = b✝ ∧ t.sum = 0
s : Multiset (ZMod (a✝⁴ * b✝))
hs : 2 * (a✝⁴ * b✝) - 1 ≤ Multiset.card s
⊢ ∃ t ≤ s, Multiset.card t = a✝⁴ * b✝ ∧ t.sum = 0
Theorem: ZMod.exists_submultiset_eq_zero
Proof state before:
n p : ℕ
inst✝ : Fact p.Prime
s✝ : Multiset (ZMod p)
s : Multiset (ZMod 0)
hs : 2 * 0 - 1 ≤ Multiset.card s
⊢ ∃ t ≤ s, Multiset.card t = 0 ∧ t.sum = 0
Tactic:
case zero => exact ⟨0, s.zero_le, card_zero, sum_zero⟩
Proof state after:
no goals
Theorem: ZMod.exists_submultiset_eq_zero
Proof state before:
n p : ℕ
inst✝ : Fact p.Prime
s✝ : Multiset (ZMod p)
s : Multiset (ZMod 1)
hs : 2 * 1 - 1 ≤ Multiset.card s
⊢ ∃ t ≤ s, Multiset.card t = 1 ∧ t.sum = 0
Tactic:
case one => obtain ⟨t, ht, hn⟩ := exists_le_card_eq hs; exact ⟨t, ht, hn, Subsingleton.elim _ _⟩
Proof state after:
no goals
Theorem: ZMod.exists_submultiset_eq_zero
Proof state before:
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
⊢ ∃ t ≤ s, Multiset.card t = p ∧ t.sum = 0
Tactic:
case prime p hp =>
  haveI := Fact.mk hp
  obtain ⟨t, hts, ht⟩ := exists_le_card_eq hs
  obtain ⟨u, hut, hu⟩ := aux ht
  exact ⟨u, hut.trans hts, hu⟩
Proof state after:
no goals
Theorem: ZMod.exists_submultiset_eq_zero
Proof state before:
n p : ℕ
inst✝ : Fact p.Prime
s✝ : Multiset (ZMod p)
s : Multiset (ZMod 0)
hs : 2 * 0 - 1 ≤ Multiset.card s
⊢ ∃ t ≤ s, Multiset.card t = 0 ∧ t.sum = 0
Tactic:
exact ⟨0, s.zero_le, card_zero, sum_zero⟩
Proof state after:
no goals
Theorem: ZMod.exists_submultiset_eq_zero
Proof state before:
n p : ℕ
inst✝ : Fact p.Prime
s✝ : Multiset (ZMod p)
s : Multiset (ZMod 1)
hs : 2 * 1 - 1 ≤ Multiset.card s
⊢ ∃ t ≤ s, Multiset.card t = 1 ∧ t.sum = 0
Tactic:
obtain ⟨t, ht, hn⟩ := exists_le_card_eq hs
Proof state after:
case intro.intro
n p : ℕ
inst✝ : Fact p.Prime
s✝ : Multiset (ZMod p)
s : Multiset (ZMod 1)
hs : 2 * 1 - 1 ≤ Multiset.card s
t : Multiset (ZMod 1)
ht : t ≤ s
hn : Multiset.card t = 2 * 1 - 1
⊢ ∃ t ≤ s, Multiset.card t = 1 ∧ t.sum = 0
Theorem: ZMod.exists_submultiset_eq_zero
Proof state before:
case intro.intro
n p : ℕ
inst✝ : Fact p.Prime
s✝ : Multiset (ZMod p)
s : Multiset (ZMod 1)
hs : 2 * 1 - 1 ≤ Multiset.card s
t : Multiset (ZMod 1)
ht : t ≤ s
hn : Multiset.card t = 2 * 1 - 1
⊢ ∃ t ≤ s, Multiset.card t = 1 ∧ t.sum = 0
Tactic:
exact ⟨t, ht, hn, Subsingleton.elim _ _⟩
Proof state after:
no goals
Theorem: ZMod.exists_submultiset_eq_zero
Proof state before:
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
⊢ ∃ t ≤ s, Multiset.card t = p ∧ t.sum = 0
Tactic:
haveI := Fact.mk hp
Proof state after:
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
Theorem: ZMod.exists_submultiset_eq_zero
Proof state before:
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
Tactic:
obtain ⟨t, hts, ht⟩ := exists_le_card_eq hs
Proof state after:
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
Theorem: ZMod.exists_submultiset_eq_zero
Proof state before:
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
Tactic:
obtain ⟨u, hut, hu⟩ := aux ht
Proof state after:
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
Theorem: ZMod.exists_submultiset_eq_zero
Proof state before:
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
Tactic:
exact ⟨u, hut.trans hts, hu⟩
Proof state after:
no goals