awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
Goal:
ι : Type u_1
p : ℕ
inst : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
hs : #s = 2 * p - 1
this : NeZero p
N : ℕ :=
  Fintype.card.{u_1}
    { x : ↥s → ZMod p //
      Eq (α := ZMod p)
          (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₁ s a) :
            ZMod p)
          (0 : ZMod p) ∧
        Eq (α := ZMod p)
          (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₂ s a) :
            ZMod p)
          (0 : ZMod p) }
zero_sol : { x : ↥s → ZMod p //
  Eq (α := ZMod p)
      (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₁ s a) : ZMod p)
      (0 : ZMod p) ∧
    Eq (α := ZMod p)
      (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₂ s a) : ZMod p)
      (0 : ZMod p) } :=
  Subtype.mk (p := fun (x : ↥s → ZMod p) ↦
    Eq (α := ZMod p)
        (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₁ s a) :
          ZMod p)
        (0 : ZMod p) ∧
      Eq (α := ZMod p)
        (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₂ s a) :
          ZMod p)
        (0 : ZMod p))
    0 ⋯
hN₀ : 0 < N
hs' : 2 * p - 1 = Fintype.card.{u_1} ↥s
hpN : p ∣ N
x :
  { x : ↥s → ZMod p //
    Eq (α := ZMod p)
        (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₁ s a) :
          ZMod p)
        (0 : ZMod p) ∧
      Eq (α := ZMod p)
        (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₂ s a) :
          ZMod p)
        (0 : ZMod p) }
hx : x ≠ zero_sol
⊢ Finset.card.{u_1} (α := ↥s) {a_1 : ↥s | (↑x : ↥s → ZMod p) a_1 ≠ 0} = p

Tactic:
Nat.eq_of_dvd_of_lt_two_mul (Finset.card_pos.2 ?_).ne' ?_ <|
      (Finset.card_filter_le _ _).trans_lt ?_

Premises used: Iff.mpr, LT.lt.ne', Nat.eq_of_dvd_of_lt_two_mul, Finset.card_pos, Finset.card_filter_le, LE.le.trans_lt
-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
Goal:
ι : Type u_1
p : ℕ
inst : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
hs : #s = 2 * p - 1
this : NeZero p
N : ℕ :=
  Fintype.card.{u_1}
    { x : ↥s → ZMod p //
      Eq (α := ZMod p)
          (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₁ s a) :
            ZMod p)
          (0 : ZMod p) ∧
        Eq (α := ZMod p)
          (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₂ s a) :
            ZMod p)
          (0 : ZMod p) }
zero_sol : { x : ↥s → ZMod p //
  Eq (α := ZMod p)
      (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₁ s a) : ZMod p)
      (0 : ZMod p) ∧
    Eq (α := ZMod p)
      (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₂ s a) : ZMod p)
      (0 : ZMod p) } :=
  Subtype.mk (p := fun (x : ↥s → ZMod p) ↦
    Eq (α := ZMod p)
        (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₁ s a) :
          ZMod p)
        (0 : ZMod p) ∧
      Eq (α := ZMod p)
        (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₂ s a) :
          ZMod p)
        (0 : ZMod p))
    0 ⋯
hN₀ : 0 < N
hs' : 2 * p - 1 = Fintype.card.{u_1} ↥s
hpN : p ∣ N
x :
  { x : ↥s → ZMod p //
    Eq (α := ZMod p)
        (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₁ s a) :
          ZMod p)
        (0 : ZMod p) ∧
      Eq (α := ZMod p)
        (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₂ s a) :
          ZMod p)
        (0 : ZMod p) }
hx : x ≠ zero_sol
refine_2 : Finset.Nonempty.{u_1} (α := ↥s) {a_1 : ↥s | (↑x : ↥s → ZMod p) a_1 ≠ 0}
refine_2₁ : p ∣ Finset.card.{u_1} (α := ↥s) {a_1 : ↥s | (↑x : ↥s → ZMod p) a_1 ≠ 0}
refine_2₂ : Finset.card.{u_1} (α := ↥s) univ < 2 * p
⊢ Finset.card.{u_1} (α := ↥s) {a_1 : ↥s | (↑x : ↥s → ZMod p) a_1 ≠ 0} = p

Tactic:
refine Nat.eq_of_dvd_of_lt_two_mul (Finset.card_pos.2 ?_).ne' ?_ <|
      (Finset.card_filter_le _ _).trans_lt ?_

Premises used: Iff.mpr, LT.lt.ne', Nat.eq_of_dvd_of_lt_two_mul, Finset.card_pos, Finset.card_filter_le, LE.le.trans_lt
-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
Goal:
ι : Type u_1
p : ℕ
inst : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
hs : #s = 2 * p - 1
this : NeZero p
N : ℕ :=
  Fintype.card.{u_1}
    { x : ↥s → ZMod p //
      Eq (α := ZMod p)
          (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₁ s a) :
            ZMod p)
          (0 : ZMod p) ∧
        Eq (α := ZMod p)
          (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₂ s a) :
            ZMod p)
          (0 : ZMod p) }
zero_sol : { x : ↥s → ZMod p //
  Eq (α := ZMod p)
      (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₁ s a) : ZMod p)
      (0 : ZMod p) ∧
    Eq (α := ZMod p)
      (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₂ s a) : ZMod p)
      (0 : ZMod p) } :=
  Subtype.mk (p := fun (x : ↥s → ZMod p) ↦
    Eq (α := ZMod p)
        (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₁ s a) :
          ZMod p)
        (0 : ZMod p) ∧
      Eq (α := ZMod p)
        (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₂ s a) :
          ZMod p)
        (0 : ZMod p))
    0 ⋯
hN₀ : 0 < N
hs' : 2 * p - 1 = Fintype.card.{u_1} ↥s
hpN : p ∣ N
x :
  { x : ↥s → ZMod p //
    Eq (α := ZMod p)
        (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₁ s a) :
          ZMod p)
        (0 : ZMod p) ∧
      Eq (α := ZMod p)
        (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₂ s a) :
          ZMod p)
        (0 : ZMod p) }
hx : x ≠ zero_sol
⊢ ∃ (a_1 : ↥s), (↑x : ↥s → ZMod p) a_1 ≠ (↑zero_sol : ↥s → ZMod p) a_1

Tactic:
rw [← Subtype.coe_ne_coe, Function.ne_iff] at hx

Premises used: Function.ne_iff, Subtype.coe_ne_coe
-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
Goal:
ι : Type u_1
p : ℕ
inst : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
hs : #s = 2 * p - 1
this : NeZero p
N : ℕ :=
  Fintype.card.{u_1}
    { x : ↥s → ZMod p //
      Eq (α := ZMod p)
          (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₁ s a) :
            ZMod p)
          (0 : ZMod p) ∧
        Eq (α := ZMod p)
          (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₂ s a) :
            ZMod p)
          (0 : ZMod p) }
zero_sol : { x : ↥s → ZMod p //
  Eq (α := ZMod p)
      (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₁ s a) : ZMod p)
      (0 : ZMod p) ∧
    Eq (α := ZMod p)
      (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₂ s a) : ZMod p)
      (0 : ZMod p) } :=
  Subtype.mk (p := fun (x : ↥s → ZMod p) ↦
    Eq (α := ZMod p)
        (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₁ s a) :
          ZMod p)
        (0 : ZMod p) ∧
      Eq (α := ZMod p)
        (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₂ s a) :
          ZMod p)
        (0 : ZMod p))
    0 ⋯
hN₀ : 0 < N
hs' : 2 * p - 1 = Fintype.card.{u_1} ↥s
hpN : p ∣ N
x :
  { x : ↥s → ZMod p //
    Eq (α := ZMod p)
        (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₁ s a) :
          ZMod p)
        (0 : ZMod p) ∧
      Eq (α := ZMod p)
        (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₂ s a) :
          ZMod p)
        (0 : ZMod p) }
hx : ∃ (a_1 : ↥s), (↑x : ↥s → ZMod p) a_1 ≠ (↑zero_sol : ↥s → ZMod p) a_1
⊢ Finset.Nonempty.{u_1} (α := ↥s) {a_1 : ↥s | (↑x : ↥s → ZMod p) a_1 ≠ 0}

Tactic:
hx.imp (fun a ha ↦ mem_filter.2 ⟨Finset.mem_attach _ _, ha⟩)

Premises used: Iff.mpr, Finset.mem_attach, Exists.imp, And.intro, Finset.Nonempty, Finset.mem_filter
-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
Goal:
ι : Type u_1
p : ℕ
inst : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
hs : #s = 2 * p - 1
this : NeZero p
N : ℕ :=
  Fintype.card.{u_1}
    { x : ↥s → ZMod p //
      Eq (α := ZMod p)
          (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₁ s a) :
            ZMod p)
          (0 : ZMod p) ∧
        Eq (α := ZMod p)
          (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₂ s a) :
            ZMod p)
          (0 : ZMod p) }
zero_sol : { x : ↥s → ZMod p //
  Eq (α := ZMod p)
      (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₁ s a) : ZMod p)
      (0 : ZMod p) ∧
    Eq (α := ZMod p)
      (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₂ s a) : ZMod p)
      (0 : ZMod p) } :=
  Subtype.mk (p := fun (x : ↥s → ZMod p) ↦
    Eq (α := ZMod p)
        (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₁ s a) :
          ZMod p)
        (0 : ZMod p) ∧
      Eq (α := ZMod p)
        (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₂ s a) :
          ZMod p)
        (0 : ZMod p))
    0 ⋯
hN₀ : 0 < N
hs' : 2 * p - 1 = Fintype.card.{u_1} ↥s
hpN : p ∣ N
x :
  { x : ↥s → ZMod p //
    Eq (α := ZMod p)
        (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₁ s a) :
          ZMod p)
        (0 : ZMod p) ∧
      Eq (α := ZMod p)
        (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₂ s a) :
          ZMod p)
        (0 : ZMod p) }
hx : ∃ (a_1 : ↥s), (↑x : ↥s → ZMod p) a_1 ≠ (↑zero_sol : ↥s → ZMod p) a_1
⊢ Finset.Nonempty.{u_1} (α := ↥s) {a_1 : ↥s | (↑x : ↥s → ZMod p) a_1 ≠ 0}

Tactic:
exact hx.imp (fun a ha ↦ mem_filter.2 ⟨Finset.mem_attach _ _, ha⟩)

Premises used: Iff.mpr, Finset.mem_attach, Exists.imp, And.intro, Finset.mem_filter
-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
Goal:
ι : Type u_1
p : ℕ
inst : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
hs : #s = 2 * p - 1
this : NeZero p
N : ℕ :=
  Fintype.card.{u_1}
    { x : ↥s → ZMod p //
      Eq (α := ZMod p)
          (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₁ s a) :
            ZMod p)
          (0 : ZMod p) ∧
        Eq (α := ZMod p)
          (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₂ s a) :
            ZMod p)
          (0 : ZMod p) }
zero_sol : { x : ↥s → ZMod p //
  Eq (α := ZMod p)
      (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₁ s a) : ZMod p)
      (0 : ZMod p) ∧
    Eq (α := ZMod p)
      (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₂ s a) : ZMod p)
      (0 : ZMod p) } :=
  Subtype.mk (p := fun (x : ↥s → ZMod p) ↦
    Eq (α := ZMod p)
        (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₁ s a) :
          ZMod p)
        (0 : ZMod p) ∧
      Eq (α := ZMod p)
        (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₂ s a) :
          ZMod p)
        (0 : ZMod p))
    0 ⋯
hN₀ : 0 < N
hs' : 2 * p - 1 = Fintype.card.{u_1} ↥s
hpN : p ∣ N
x :
  { x : ↥s → ZMod p //
    Eq (α := ZMod p)
        (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₁ s a) :
          ZMod p)
        (0 : ZMod p) ∧
      Eq (α := ZMod p)
        (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₂ s a) :
          ZMod p)
        (0 : ZMod p) }
hx : x ≠ zero_sol
refine_2 : Eq (α := ZMod p) (∑ x_1 : ↥s, if (↑x : ↥s → ZMod p) x_1 ≠ 0 then 1 else 0) 0
⊢ p ∣ Finset.card.{u_1} (α := ↥s) {a_1 : ↥s | (↑x : ↥s → ZMod p) a_1 ≠ 0}

Tactic:
rw [← CharP.cast_eq_zero_iff (ZMod p), ← Finset.sum_boole]

Premises used: ZMod, CharP.cast_eq_zero_iff, Finset.sum_boole
-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
Goal:
ι : Type u_1
p : ℕ
inst : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
hs : #s = 2 * p - 1
this : NeZero p
N : ℕ :=
  Fintype.card.{u_1}
    { x : ↥s → ZMod p //
      Eq (α := ZMod p)
          (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₁ s a) :
            ZMod p)
          (0 : ZMod p) ∧
        Eq (α := ZMod p)
          (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₂ s a) :
            ZMod p)
          (0 : ZMod p) }
zero_sol : { x : ↥s → ZMod p //
  Eq (α := ZMod p)
      (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₁ s a) : ZMod p)
      (0 : ZMod p) ∧
    Eq (α := ZMod p)
      (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₂ s a) : ZMod p)
      (0 : ZMod p) } :=
  Subtype.mk (p := fun (x : ↥s → ZMod p) ↦
    Eq (α := ZMod p)
        (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₁ s a) :
          ZMod p)
        (0 : ZMod p) ∧
      Eq (α := ZMod p)
        (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₂ s a) :
          ZMod p)
        (0 : ZMod p))
    0 ⋯
hN₀ : 0 < N
hs' : 2 * p - 1 = Fintype.card.{u_1} ↥s
hpN : p ∣ N
x :
  { x : ↥s → ZMod p //
    Eq (α := ZMod p)
        (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₁ s a) :
          ZMod p)
        (0 : ZMod p) ∧
      Eq (α := ZMod p)
        (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₂ s a) :
          ZMod p)
        (0 : ZMod p) }
hx : x ≠ zero_sol
⊢ Eq (α := ZMod p) (∑ x_1 : ↥s, if (↑x : ↥s → ZMod p) 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

Premises used: ZMod.pow_card_sub_one, _private.0.f₁, map_pow, map_sum, And.left, MvPolynomial.eval_X, Subtype.property
-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
Goal:
ι : Type u_1
p : ℕ
inst : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
hs : #s = 2 * p - 1
this : NeZero p
N : ℕ :=
  Fintype.card.{u_1}
    { x : ↥s → ZMod p //
      Eq (α := ZMod p)
          (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₁ s a) :
            ZMod p)
          (0 : ZMod p) ∧
        Eq (α := ZMod p)
          (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₂ s a) :
            ZMod p)
          (0 : ZMod p) }
zero_sol : { x : ↥s → ZMod p //
  Eq (α := ZMod p)
      (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₁ s a) : ZMod p)
      (0 : ZMod p) ∧
    Eq (α := ZMod p)
      (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₂ s a) : ZMod p)
      (0 : ZMod p) } :=
  Subtype.mk (p := fun (x : ↥s → ZMod p) ↦
    Eq (α := ZMod p)
        (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₁ s a) :
          ZMod p)
        (0 : ZMod p) ∧
      Eq (α := ZMod p)
        (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₂ s a) :
          ZMod p)
        (0 : ZMod p))
    0 ⋯
hN₀ : 0 < N
hs' : 2 * p - 1 = Fintype.card.{u_1} ↥s
hpN : p ∣ N
x :
  { x : ↥s → ZMod p //
    Eq (α := ZMod p)
        (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₁ s a) :
          ZMod p)
        (0 : ZMod p) ∧
      Eq (α := ZMod p)
        (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₂ s a) :
          ZMod p)
        (0 : ZMod p) }
hx : x ≠ zero_sol
refine_2 : 2 * p - 1 < 2 * p
⊢ Finset.card.{u_1} (α := ↥s) univ < 2 * p

Tactic:
rw [univ_eq_attach, card_attach, hs]

Premises used: Finset.card_attach, Finset.univ_eq_attach
-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
Goal:
ι : Type u_1
p : ℕ
inst : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
hs : #s = 2 * p - 1
this : NeZero p
N : ℕ :=
  Fintype.card.{u_1}
    { x : ↥s → ZMod p //
      Eq (α := ZMod p)
          (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₁ s a) :
            ZMod p)
          (0 : ZMod p) ∧
        Eq (α := ZMod p)
          (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₂ s a) :
            ZMod p)
          (0 : ZMod p) }
zero_sol : { x : ↥s → ZMod p //
  Eq (α := ZMod p)
      (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₁ s a) : ZMod p)
      (0 : ZMod p) ∧
    Eq (α := ZMod p)
      (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₂ s a) : ZMod p)
      (0 : ZMod p) } :=
  Subtype.mk (p := fun (x : ↥s → ZMod p) ↦
    Eq (α := ZMod p)
        (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₁ s a) :
          ZMod p)
        (0 : ZMod p) ∧
      Eq (α := ZMod p)
        (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₂ s a) :
          ZMod p)
        (0 : ZMod p))
    0 ⋯
hN₀ : 0 < N
hs' : 2 * p - 1 = Fintype.card.{u_1} ↥s
hpN : p ∣ N
x :
  { x : ↥s → ZMod p //
    Eq (α := ZMod p)
        (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₁ s a) :
          ZMod p)
        (0 : ZMod p) ∧
      Eq (α := ZMod p)
        (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₂ s a) :
          ZMod p)
        (0 : ZMod p) }
hx : x ≠ zero_sol
⊢ 2 * p - 1 < 2 * p

Tactic:
tsub_lt_self (mul_pos zero_lt_two (Fact.out : p.Prime).pos) zero_lt_one

Premises used: Nat.Prime.pos, zero_lt_one, mul_pos, zero_lt_two, tsub_lt_self, Fact.out
-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
Goal:
ι : Type u_1
p : ℕ
inst : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
hs : #s = 2 * p - 1
this : NeZero p
N : ℕ :=
  Fintype.card.{u_1}
    { x : ↥s → ZMod p //
      Eq (α := ZMod p)
          (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₁ s a) :
            ZMod p)
          (0 : ZMod p) ∧
        Eq (α := ZMod p)
          (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₂ s a) :
            ZMod p)
          (0 : ZMod p) }
zero_sol : { x : ↥s → ZMod p //
  Eq (α := ZMod p)
      (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₁ s a) : ZMod p)
      (0 : ZMod p) ∧
    Eq (α := ZMod p)
      (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₂ s a) : ZMod p)
      (0 : ZMod p) } :=
  Subtype.mk (p := fun (x : ↥s → ZMod p) ↦
    Eq (α := ZMod p)
        (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₁ s a) :
          ZMod p)
        (0 : ZMod p) ∧
      Eq (α := ZMod p)
        (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₂ s a) :
          ZMod p)
        (0 : ZMod p))
    0 ⋯
hN₀ : 0 < N
hs' : 2 * p - 1 = Fintype.card.{u_1} ↥s
hpN : p ∣ N
x :
  { x : ↥s → ZMod p //
    Eq (α := ZMod p)
        (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₁ s a) :
          ZMod p)
        (0 : ZMod p) ∧
      Eq (α := ZMod p)
        (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₂ s a) :
          ZMod p)
        (0 : ZMod p) }
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

Premises used: Nat.Prime.pos, zero_lt_one, mul_pos, tsub_lt_self, Fact.out
-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
Goal:
ι : Type u_1
p : ℕ
inst : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
hs : #s = 2 * p - 1
this : NeZero p
N : ℕ :=
  Fintype.card.{u_1}
    { x : ↥s → ZMod p //
      Eq (α := ZMod p)
          (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₁ s a) :
            ZMod p)
          (0 : ZMod p) ∧
        Eq (α := ZMod p)
          (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₂ s a) :
            ZMod p)
          (0 : ZMod p) }
zero_sol : { x : ↥s → ZMod p //
  Eq (α := ZMod p)
      (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₁ s a) : ZMod p)
      (0 : ZMod p) ∧
    Eq (α := ZMod p)
      (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₂ s a) : ZMod p)
      (0 : ZMod p) } :=
  Subtype.mk (p := fun (x : ↥s → ZMod p) ↦
    Eq (α := ZMod p)
        (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₁ s a) :
          ZMod p)
        (0 : ZMod p) ∧
      Eq (α := ZMod p)
        (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₂ s a) :
          ZMod p)
        (0 : ZMod p))
    0 ⋯
hN₀ : 0 < N
hs' : 2 * p - 1 = Fintype.card.{u_1} ↥s
hpN : p ∣ N
x :
  { x : ↥s → ZMod p //
    Eq (α := ZMod p)
        (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₁ s a) :
          ZMod p)
        (0 : ZMod p) ∧
      Eq (α := ZMod p)
        (((eval x : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₂ s a) :
          ZMod p)
        (0 : ZMod p) }
hx : x ≠ zero_sol
⊢ Eq (α := ZMod p)
    (∑
      i ∈
        Finset.map (α := ↥s) { toFun := Subtype.val (p := fun (x : ι) ↦ x ∈ s), inj' := ⋯ }
          {a_1 : ↥s | (↑x : ↥s → ZMod p) a_1 ≠ 0},
      a i)
    0

Tactic:
simpa [f₂, ZMod.pow_card_sub_one, Finset.sum_filter] using x.2.2

Premises used: ZMod.pow_card_sub_one, And.right, _private.0.f₂, Finset.sum_filter, Subtype.property
-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
Goal:
ι : Type u_1
p : ℕ
inst : Fact (Nat.Prime p)
s : Finset ι
a : ι → ℤ
hs : #s = 2 * p - 1
⊢ ∃ t ⊆ s, #t = p ∧ Dvd.dvd (α := ℤ) (↑p : ℤ) (∑ i ∈ t, a i)

Tactic:
simpa [← Int.cast_sum, ZMod.intCast_zmod_eq_zero_iff_dvd]
    using ZMod.erdos_ginzburg_ziv_prime (Int.cast ∘ a) hs

Premises used: Int.cast, Function.comp, Int.cast_sum, _private.0.ZMod.erdos_ginzburg_ziv_prime, ZMod.intCast_zmod_eq_zero_iff_dvd
-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
Goal:
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : HMul.hMul (α := ℕ) 2 0 - 1 ≤ #s
⊢ ∅ ⊆ s ∧ card.{u_1} (α := ι) ∅ = 0 ∧ Dvd.dvd (α := ℤ) (↑0 : ℤ) (∑ i ∈ ∅, a i)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
Goal:
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : HMul.hMul (α := ℕ) 2 0 - 1 ≤ #s
⊢ ∃ t ⊆ s, #t = 0 ∧ Dvd.dvd (α := ℤ) (↑0 : ℤ) (∑ i ∈ t, a i)

Tactic:
exact ⟨∅, by simp⟩