awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Additive.Energy
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommGroup α
inst_2 : Fintype α
t : Finset α
f : α × α × α → (α × α) × α × α := fun (x : α × α × α) ↦ ((x.1 * x.2.2, x.1 * x.2.1), x.2)
this : Set.InjOn f (↑(SProd.sprod (α := Finset α) univ (t ×ˢ t)) : Set (α × α × α))
a : (α × α) × α × α
h : (a.2.1 ∈ t ∧ a.2.2 ∈ t) ∧ a.1.1 * a.2.1 = a.1.2 * a.2.2
⊢ f (a.1.1 * a.2.2⁻¹, a.2.1, a.2.2) = a

Tactic:
simp [f, mul_right_comm, h.2]

Premises used: And.right, mul_right_comm
-- Module: Mathlib.Combinatorics.Additive.Energy
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommGroup α
inst_2 : Fintype α
t : Finset α
f : α × α × α → (α × α) × α × α := fun (x : α × α × α) ↦ ((x.1 * x.2.2, x.1 * x.2.1), x.2)
this : Set.InjOn f (↑(SProd.sprod (α := Finset α) univ (t ×ˢ t)) : Set (α × α × α))
a : (α × α) × α × α
e_s :
  (∃ (a_1 : α) (a_2 : α) (b : α), (a_2 ∈ t ∧ b ∈ t) ∧ f (a_1, a_2, b) = a) →
    (a.2.1 ∈ t ∧ a.2.2 ∈ t) ∧ a.1.1 * a.2.1 = a.1.2 * a.2.2
⊢ (a.2.1 ∈ t ∧ a.2.2 ∈ t) ∧ a.1.1 * a.2.1 = a.1.2 * a.2.2 ↔
    ∃ (a_1 : α) (a_2 : α) (b : α), (a_2 ∈ t ∧ b ∈ t) ∧ f (a_1, a_2, b) = a

Tactic:
refine ⟨fun h => ⟨a.1.1 * a.2.2⁻¹, _, _, h.1, by simp [f, mul_right_comm, h.2]⟩, ?_⟩
-- Module: Mathlib.Combinatorics.Additive.Energy
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommGroup α
inst_2 : Fintype α
t : Finset α
f : α × α × α → (α × α) × α × α := fun (x : α × α × α) ↦ ((x.1 * x.2.2, x.1 * x.2.1), x.2)
this : Set.InjOn f (↑(SProd.sprod (α := Finset α) univ (t ×ˢ t)) : Set (α × α × α))
b c d : α
hcd : c ∈ t ∧ d ∈ t
⊢ ((f (b, c, d)).2.1 ∈ t ∧ (f (b, c, d)).2.2 ∈ t) ∧
    (f (b, c, d)).1.1 * (f (b, c, d)).2.1 = (f (b, c, d)).1.2 * (f (b, c, d)).2.2

Tactic:
simpa [f, mul_right_comm]

Premises used: mul_right_comm
-- Module: Mathlib.Combinatorics.Additive.Energy
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommGroup α
inst_2 : Fintype α
s : Finset α
rw : Eₘ[univ, s] = Fintype.card α * HPow.hPow (β := ℕ) (#s) 2
rw₁ rw₂ : Fintype.card α * HPow.hPow (β := ℕ) (#s) 2 = Fintype.card α * HPow.hPow (β := ℕ) (#s) 2
⊢ Eₘ[s, univ] = Fintype.card α * HPow.hPow (β := ℕ) (#s) 2

Tactic:
rw [mulEnergy_comm, mulEnergy_univ_left]

Premises used: Finset.mulEnergy_univ_left, Finset.mulEnergy_comm
-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
Goal:
ι : Type u_1
p : ℕ
inst : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
h₁ : totalDegree (f₁ s a) ≤ p - 1
h₂ : totalDegree (f₂ s a) ≤ p - 1
⊢ totalDegree (f₁ s a) + totalDegree (f₂ s a) ≤ p - 1 + (p - 1)

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
Goal:
ι : Type u_1
p : ℕ
inst : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
h₁ :
  ∀ (i : ↥s),
    Membership.mem (γ := Finset ↥s) univ i →
      (HPow.hPow (α := MvPolynomial (↥s) (ZMod p)) (X i) (p - 1)).totalDegree ≤ p - 1
⊢ totalDegree (f₁ s a) ≤ p - 1

Tactic:
apply totalDegree_finsetSum_le

Premises used: MvPolynomial.totalDegree_finsetSum_le
-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
Goal:
ι : Type u_1
p : ℕ
inst : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
h₂ :
  ∀ (i : ↥s),
    Membership.mem (γ := Finset ↥s) univ i →
      (a (↑i : ι) • HPow.hPow (α := MvPolynomial (↥s) (ZMod p)) (X i) (p - 1)).totalDegree ≤ p - 1
⊢ totalDegree (f₂ s a) ≤ p - 1

Tactic:
apply totalDegree_finsetSum_le

Premises used: MvPolynomial.totalDegree_finsetSum_le
-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
Goal:
ι : Type u_1
p : ℕ
inst : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
i : ↥s
h : Membership.mem (γ := Finset ↥s) univ i
⊢ (HPow.hPow (α := MvPolynomial (↥s) (ZMod p)) (X i) (p - 1)).totalDegree ≤ p - 1

Tactic:
(totalDegree_X_pow ..).le

Premises used: MvPolynomial.totalDegree_X_pow, Eq.le
-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
Goal:
ι : Type u_1
p : ℕ
inst : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
i : ↥s
h : Membership.mem (γ := Finset ↥s) univ i
⊢ (HPow.hPow (α := MvPolynomial (↥s) (ZMod p)) (X i) (p - 1)).totalDegree ≤ p - 1

Tactic:
exact (totalDegree_X_pow ..).le

Premises used: MvPolynomial.totalDegree_X_pow, Eq.le
-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
Goal:
ι : Type u_1
p : ℕ
inst : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
i : ↥s
h : Membership.mem (γ := Finset ↥s) univ i
⊢ (a (↑i : ι) • HPow.hPow (α := MvPolynomial (↥s) (ZMod p)) (X i) (p - 1)).totalDegree ≤ p - 1

Tactic:
(totalDegree_smul_le ..).trans (totalDegree_X_pow ..).le

Premises used: MvPolynomial.totalDegree_X_pow, Eq.le, MvPolynomial.totalDegree_smul_le, LE.le.trans
-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
Goal:
ι : Type u_1
p : ℕ
inst : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
i : ↥s
h : Membership.mem (γ := Finset ↥s) univ i
⊢ (a (↑i : ι) • HPow.hPow (α := MvPolynomial (↥s) (ZMod p)) (X i) (p - 1)).totalDegree ≤ p - 1

Tactic:
exact (totalDegree_smul_le ..).trans (totalDegree_X_pow ..).le

Premises used: MvPolynomial.totalDegree_X_pow, Eq.le, MvPolynomial.totalDegree_smul_le, LE.le.trans
-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
Goal:
ι : Type u_1
p : ℕ
inst : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
⊢ 2 ≤ p

Tactic:
have := (Fact.out : p.Prime).two_le
-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
Goal:
ι : Type u_1
p : ℕ
inst : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
this : 2 ≤ p
⊢ p - 1 + (p - 1) < 2 * p - 1

Tactic:
lia
-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
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)
_₁ : p - 1 + (p - 1) < 2 * p - 1
⊢ totalDegree (f₁ s a) + totalDegree (f₂ s a) < 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

Premises used: HSub.hSub, OfNat.ofNat
-- 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
⊢ NeZero p

Tactic:
haveI : NeZero p := inferInstance
-- 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) }
⊢ Eq (α := ZMod p)
      (((eval 0 : 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 0 : MvPolynomial (↥s) (ZMod p) →+* ZMod p) : (a : MvPolynomial (↥s) (ZMod p)) → ZMod p) (f₂ s a) : ZMod p)
      (0 : ZMod p)

Tactic:
simp [f₁, f₂, map_sum, (Fact.out : p.Prime).one_lt, tsub_eq_zero_iff_le]

Premises used: Nat.Prime.one_lt, _private.0.f₁, tsub_eq_zero_iff_le, map_sum, _private.0.f₂, 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 ⋯
⊢ 0 < N

Tactic:
have hN₀ : 0 < N := @Fintype.card_pos _ _ ⟨zero_sol⟩
-- 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
⊢ 2 * p - 1 = Fintype.card.{u_1} ↥s

Tactic:
simp [hs]
-- 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
⊢ 2 * p - 1 = Fintype.card.{u_1} ↥s

Tactic:
have hs' : 2 * p - 1 = Fintype.card s := by simp [hs]
-- 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
⊢ p ∣ N

Tactic:
have hpN : p ∣ N := char_dvd_card_solutions_of_add_lt p
    (totalDegree_f₁_add_totalDegree_f₂.trans_eq hs')
-- 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
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
⊢ ∃ 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

Premises used: Nat.Prime.one_lt, Fintype.exists_ne_of_one_lt_card, LT.lt.trans_le, Nat.le_of_dvd, 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
⊢ ∃ t ⊆ s, #t = p ∧ Eq (α := ZMod p) (∑ i ∈ t, a i) 0

Tactic:
⟨({a | x.1 a ≠ 0} : Finset _).map ⟨(↑), Subtype.val_injective⟩, ?_, ?_, ?_⟩

Premises used: Finset.univ, Finset.map, Function.Embedding.mk, Ne, And.intro, Exists.intro, OfNat.ofNat, Subtype.val, Finset.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_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
refine_3 :
  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
⊢ ∃ t ⊆ s, #t = p ∧ Eq (α := ZMod p) (∑ i ∈ t, a i) 0

Tactic:
refine ⟨({a | x.1 a ≠ 0} : Finset _).map ⟨(↑), Subtype.val_injective⟩, ?_, ?_, ?_⟩
-- 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.map (α := ↥s) { toFun := Subtype.val (p := fun (x : ι) ↦ x ∈ s), inj' := ⋯ }
      {a_1 : ↥s | (↑x : ↥s → ZMod p) a_1 ≠ 0} ⊆
    s

Tactic:
simp +contextual [subset_iff]

Premises used: Finset.subset_iff
-- 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.card.{u_1} (α := ↥s) {a_1 : ↥s | (↑x : ↥s → ZMod p) a_1 ≠ 0} = p
⊢ 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

Tactic:
rw [card_map]

Premises used: Finset.card_map