awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Energy (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommGroup α
inst_2 : Fintype α
s : Finset α
⊢ Eₘ[s, univ] = Fintype.card α * HPow.hPow (β := ℕ) (#s) 2
have rw : Eₘ[univ, s] = Fintype.card α * HPow.hPow (β := ℕ) (#s) 2
Tactic: rw [mulEnergy_comm, mulEnergy_univ_left]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Energy (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommGroup α
inst_2 : Fintype α
s : Finset α
rw : Eₘ[univ, s] = Fintype.card α * HPow.hPow (β := ℕ) (#s) 2
⊢ Eₘ[s, univ] = Fintype.card α * HPow.hPow (β := ℕ) (#s) 2
have rw₁ : Fintype.card α * HPow.hPow (β := ℕ) (#s) 2 = Fintype.card α * HPow.hPow (β := ℕ) (#s) 2
Tactic: rw [mulEnergy_comm, mulEnergy_univ_left]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ErdosGinzburgZiv (goal)
Goal:
ι : Type u_1
p : ℕ
inst : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
⊢ totalDegree (f₁ s a) + totalDegree (f₂ s a) ≤ p - 1 + (p - 1)
have h₁ : totalDegree (f₁ s a) ≤ p - 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ErdosGinzburgZiv (goal)
Goal:
ι : Type u_1
p : ℕ
inst : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
h₁ : totalDegree (f₁ s a) ≤ p - 1
⊢ totalDegree (f₁ s a) + totalDegree (f₂ s a) ≤ p - 1 + (p - 1)
have h₂ : totalDegree (f₂ s a) ≤ p - 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ErdosGinzburgZiv (goal)
Goal:
ι : Type u_1
p : ℕ
inst : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
⊢ totalDegree (f₁ s a) ≤ p - 1
have h₁ : ∀ (i : ↥s),
  Membership.mem (γ := Finset ↥s) univ i →
    (HPow.hPow (α := MvPolynomial (↥s) (ZMod p)) (X i) (p - 1)).totalDegree ≤ p - 1
Tactic: apply totalDegree_finsetSum_le
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ErdosGinzburgZiv (goal)
Goal:
ι : Type u_1
p : ℕ
inst : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
⊢ totalDegree (f₂ s a) ≤ p - 1
have h₂ : ∀ (i : ↥s),
  Membership.mem (γ := Finset ↥s) univ i →
    (a (↑i : ι) • HPow.hPow (α := MvPolynomial (↥s) (ZMod p)) (X i) (p - 1)).totalDegree ≤ p - 1
Tactic: apply totalDegree_finsetSum_le
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ErdosGinzburgZiv (hypothesis)
Goal:
ι : Type u_1
p : ℕ
inst : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
⊢ p - 1 + (p - 1) < 2 * p - 1
have this : 2 ≤ p
Tactic: have := (Fact.out : p.Prime).two_le
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ErdosGinzburgZiv (goal)
Goal:
ι : Type u_1
p : ℕ
inst : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
⊢ totalDegree (f₁ s a) + totalDegree (f₂ s a) < 2 * p - 1
have _ : totalDegree (f₁ s a) + totalDegree (f₂ s a) ≤ p - 1 + (p - 1)
Tactic: calc
    _ ≤ (p - 1) + (p - 1) := by
      gcongr <;> apply totalDegree_finsetSum_le <;> rintro i _
      · exact (totalDegree_X_pow ..).le
      · exact (totalDegree_smul_le ..).trans (totalDegree_X_pow ..).le
    _ < 2 * p - 1 := by have := (Fact.out : p.Prime).two_le; lia
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ErdosGinzburgZiv (goal)
Goal:
ι : Type u_1
p : ℕ
inst : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
_ : totalDegree (f₁ s a) + totalDegree (f₂ s a) ≤ p - 1 + (p - 1)
⊢ totalDegree (f₁ s a) + totalDegree (f₂ s a) < 2 * p - 1
have _₁ : p - 1 + (p - 1) < 2 * p - 1
Tactic: calc
    _ ≤ (p - 1) + (p - 1) := by
      gcongr <;> apply totalDegree_finsetSum_le <;> rintro i _
      · exact (totalDegree_X_pow ..).le
      · exact (totalDegree_smul_le ..).trans (totalDegree_X_pow ..).le
    _ < 2 * p - 1 := by have := (Fact.out : p.Prime).two_le; lia
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ErdosGinzburgZiv (hypothesis)
Goal:
ι : Type u_1
p : ℕ
inst : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
hs : #s = 2 * p - 1
⊢ ∃ t ⊆ s, #t = p ∧ Eq (α := ZMod p) (∑ i ∈ t, a i) 0
have this : NeZero p
Tactic: haveI : NeZero p := inferInstance
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ErdosGinzburgZiv (hypothesis)
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 ⋯
⊢ ∃ t ⊆ s, #t = p ∧ Eq (α := ZMod p) (∑ i ∈ t, a i) 0
have hN₀ : 0 < N
Tactic: have hN₀ : 0 < N := @Fintype.card_pos _ _ ⟨zero_sol⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ErdosGinzburgZiv (hypothesis)
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
⊢ ∃ t ⊆ s, #t = p ∧ Eq (α := ZMod p) (∑ i ∈ t, a i) 0
have hs' : 2 * p - 1 = Fintype.card.{u_1} ↥s
Tactic: have hs' : 2 * p - 1 = Fintype.card s := by simp [hs]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ErdosGinzburgZiv (hypothesis)
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
⊢ ∃ t ⊆ s, #t = p ∧ Eq (α := ZMod p) (∑ i ∈ t, a i) 0
have hpN : p ∣ N
Tactic: have hpN : p ∣ N := char_dvd_card_solutions_of_add_lt p
    (totalDegree_f₁_add_totalDegree_f₂.trans_eq hs')
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ErdosGinzburgZiv (goal)
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
⊢ ∃ t ⊆ s, #t = p ∧ Eq (α := ZMod p) (∑ i ∈ t, a i) 0
have obtain : ∀
  (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), ∃ t ⊆ s, #t = p ∧ Eq (α := ZMod p) (∑ i ∈ t, a i) 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
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ErdosGinzburgZiv (goal)
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
⊢ ∃ t ⊆ s, #t = p ∧ Eq (α := ZMod p) (∑ i ∈ t, a i) 0
have refine_1 : Finset.map (α := ↥s) { toFun := Subtype.val (p := fun (x : ι) ↦ x ∈ s), inj' := sorry }
    {a_1 : ↥s | (↑x : ↥s → ZMod p) a_1 ≠ 0} ⊆
  s
Tactic: refine ⟨({a | x.1 a ≠ 0} : Finset _).map ⟨(↑), Subtype.val_injective⟩, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ErdosGinzburgZiv (goal)
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_1 :
  Finset.map (α := ↥s) { toFun := Subtype.val (p := fun (x : ι) ↦ x ∈ s), inj' := ⋯ }
      {a_1 : ↥s | (↑x : ↥s → ZMod p) a_1 ≠ 0} ⊆
    s
⊢ ∃ t ⊆ s, #t = p ∧ Eq (α := ZMod p) (∑ i ∈ t, a i) 0
have refine_2 : Finset.card.{u_1} (α := ι)
    (Finset.map (α := ↥s) { toFun := Subtype.val (p := fun (x : ι) ↦ x ∈ s), inj' := sorry : ↥s ↪ ι }
      {a_1 : ↥s | (↑x : ↥s → ZMod p) a_1 ≠ 0}) =
  p
Tactic: refine ⟨({a | x.1 a ≠ 0} : Finset _).map ⟨(↑), Subtype.val_injective⟩, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ErdosGinzburgZiv (goal)
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_1 :
  Finset.map (α := ↥s) { toFun := Subtype.val (p := fun (x : ι) ↦ x ∈ s), inj' := ⋯ }
      {a_1 : ↥s | (↑x : ↥s → ZMod p) a_1 ≠ 0} ⊆
    s
refine_2 :
  Finset.card.{u_1} (α := ι)
      (Finset.map (α := ↥s) { toFun := Subtype.val (p := fun (x : ι) ↦ x ∈ s), inj' := ⋯ : ↥s ↪ ι }
        {a_1 : ↥s | (↑x : ↥s → ZMod p) a_1 ≠ 0}) =
    p
⊢ ∃ t ⊆ s, #t = p ∧ Eq (α := ZMod p) (∑ i ∈ t, a i) 0
have refine_3 : Eq (α := ZMod p)
  (∑
    i ∈
      Finset.map (α := ↥s) { toFun := Subtype.val (p := fun (x : ι) ↦ x ∈ s), inj' := sorry }
        {a_1 : ↥s | (↑x : ↥s → ZMod p) a_1 ≠ 0},
    a i)
  0
Tactic: refine ⟨({a | x.1 a ≠ 0} : Finset _).map ⟨(↑), Subtype.val_injective⟩, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ErdosGinzburgZiv (goal)
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} (α := ι)
      (Finset.map (α := ↥s) { toFun := Subtype.val (p := fun (x : ι) ↦ x ∈ s), inj' := ⋯ : ↥s ↪ ι }
        {a_1 : ↥s | (↑x : ↥s → ZMod p) a_1 ≠ 0}) =
    p
have refine_2 : Finset.card.{u_1} (α := ↥s) {a_1 : ↥s | (↑x : ↥s → ZMod p) a_1 ≠ 0} = p
Tactic: rw [card_map]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ErdosGinzburgZiv (goal)
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
have refine_2 : Finset.Nonempty.{u_1} (α := ↥s) {a_1 : ↥s | (↑x : ↥s → ZMod p) a_1 ≠ 0}
Tactic: refine Nat.eq_of_dvd_of_lt_two_mul (Finset.card_pos.2 ?_).ne' ?_ <|
      (Finset.card_filter_le _ _).trans_lt ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ErdosGinzburgZiv (goal)
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}
⊢ Finset.card.{u_1} (α := ↥s) {a_1 : ↥s | (↑x : ↥s → ZMod p) a_1 ≠ 0} = p
have refine_2₁ : p ∣ Finset.card.{u_1} (α := ↥s) {a_1 : ↥s | (↑x : ↥s → ZMod p) a_1 ≠ 0}
Tactic: refine Nat.eq_of_dvd_of_lt_two_mul (Finset.card_pos.2 ?_).ne' ?_ <|
      (Finset.card_filter_le _ _).trans_lt ?_