awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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}
refine_2₁ : p ∣ Finset.card.{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₂ : Finset.card.{u_1} (α := ↥s) univ < 2 * p
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 (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
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.Nonempty.{u_1} (α := ↥s) {a_1 : ↥s | (↑x : ↥s → ZMod p) a_1 ≠ 0}
have hx₁ : ∃ (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
Cleared hypotheses: hx
-- 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
⊢ p ∣ Finset.card.{u_1} (α := ↥s) {a_1 : ↥s | (↑x : ↥s → ZMod p) a_1 ≠ 0}
have refine_2 : Eq (α := ZMod p) (∑ x_1 : ↥s, if (↑x : ↥s → ZMod p) x_1 ≠ 0 then 1 else 0) 0
Tactic: rw [← CharP.cast_eq_zero_iff (ZMod p), ← Finset.sum_boole]
-- 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) univ < 2 * p
have refine_2 : 2 * p - 1 < 2 * p
Tactic: rw [univ_eq_attach, card_attach, 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
Let Let₁ Let₂ : ∃ t ⊆ s, #t = p ∧ Eq (α := ZMod p) (∑ i ∈ t, a i) 0
⊢ ∃ t ⊆ s, #t = p ∧ Eq (α := ZMod p) (∑ i ∈ t, a i) 0
have Let₃ : let 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) };
∀ (hN₀ : 0 < N), ∃ t ⊆ s, #t = p ∧ Eq (α := ZMod p) (∑ i ∈ t, a i) 0
Tactic: classical
  -- Let `N` be the number of common roots of our polynomials `f₁` and `f₂` (`f s ff` and `f s tt`).
  set N := Fintype.card {x // eval x (f₁ s a) = 0 ∧ eval x (f₂ s a) = 0}
  -- Zero is a common root to `f₁` and `f₂`, so `N` is nonzero
  let zero_sol : {x // eval x (f₁ s a) = 0 ∧ eval x (f₂ s a) = 0} :=
    ⟨0, by simp [f₁, f₂, map_sum, (Fact.out : p.Prime).one_lt, tsub_eq_zero_iff_le]⟩
  have hN₀ : 0 < N := @Fintype.card_pos _ _ ⟨zero_sol⟩
  have hs' : 2 * p - 1 = Fintype.card s := by simp [hs]
  -- Chevalley-Warning gives us that `p ∣ n` because the total degrees of `f₁` and `f₂` are at most
  -- `p - 1`, and we have `2 * p - 1 > 2 * (p - 1)` variables.
  have hpN : p ∣ N := char_dvd_card_solutions_of_add_lt p
    (totalDegree_f₁_add_totalDegree_f₂.trans_eq hs')
  -- Hence, `2 ≤ p ≤ N` and we can make a common root `x ≠ 0`.
  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
  -- This common root gives us the required subsequence, namely the `i ∈ s` such that `x i ≠ 0`.
  refine ⟨({a | x.1 a ≠ 0} : Finset _).map ⟨(↑), Subtype.val_injective⟩, ?_, ?_, ?_⟩
  · simp +contextual [subset_iff]
  -- From `f₁ x = 0`, we get that `p` divides the number of `a` such that `x a ≠ 0`.
  · rw [card_map]
    refine Nat.eq_of_dvd_of_lt_two_mul (Finset.card_pos.2 ?_).ne' ?_ <|
      (Finset.card_filter_le _ _).trans_lt ?_
    -- This number is nonzero because `x ≠ 0`.
    · rw [← Subtype.coe_ne_coe, Function.ne_iff] at hx
      exact hx.imp (fun a ha ↦ mem_filter.2 ⟨Finset.mem_attach _ _, ha⟩)
    · rw [← CharP.cast_eq_zero_iff (ZMod p), ← Finset.sum_boole]
      simpa only [f₁, map_sum, ZMod.pow_card_sub_one, map_pow, eval_X] using x.2.1
    -- And it is at most `2 * p - 1`, so it must be `p`.
    · rw [univ_eq_attach, card_attach, hs]
      exact tsub_lt_self (mul_pos zero_lt_two (Fact.out : p.Prime).pos) zero_lt_one
  -- From `f₂ x = 0`, we get that `p` divides the sum of the `a ∈ s` such that `x a ≠ 0`.
  · simpa [f₂, ZMod.pow_card_sub_one, Finset.sum_filter] using x.2.2
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ErdosGinzburgZiv (hypothesis)
Goal:
p : ℕ
hp : Nat.Prime p
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * p - 1 ≤ #s
⊢ ∃ t ⊆ s, #t = p ∧ Dvd.dvd (α := ℤ) (↑p : ℤ) (∑ i ∈ t, a i)
have this : Fact (Nat.Prime p)
Tactic: haveI := Fact.mk hp
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ErdosGinzburgZiv (goal)
Goal:
p : ℕ
hp : Nat.Prime p
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * p - 1 ≤ #s
this : Fact (Nat.Prime p)
⊢ ∃ t ⊆ s, #t = p ∧ Dvd.dvd (α := ℤ) (↑p : ℤ) (∑ i ∈ t, a i)
have prime : ∀ (t : Finset ι) (hts : t ⊆ s) (ht : #t = 2 * p - 1), ∃ t ⊆ s, #t = p ∧ Dvd.dvd (α := ℤ) (↑p : ℤ) (∑ i ∈ t, a i)
Tactic: obtain ⟨t, hts, ht⟩ := exists_subset_card_eq hs
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ErdosGinzburgZiv (goal)
Goal:
p : ℕ
hp : Nat.Prime p
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * p - 1 ≤ #s
this : Fact (Nat.Prime p)
t : Finset ι
hts : t ⊆ s
ht : #t = 2 * p - 1
⊢ ∃ t ⊆ s, #t = p ∧ Dvd.dvd (α := ℤ) (↑p : ℤ) (∑ i ∈ t, a i)
have prime : ∀ (u : Finset ι) (hut : u ⊆ t) (hu : #u = p ∧ Dvd.dvd (α := ℤ) (↑p : ℤ) (∑ i ∈ u, a i)),
  ∃ t ⊆ s, #t = p ∧ Dvd.dvd (α := ℤ) (↑p : ℤ) (∑ i ∈ t, a i)
Tactic: obtain ⟨u, hut, hu⟩ := Int.erdos_ginzburg_ziv_prime a ht
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ErdosGinzburgZiv (goal)
Goal:
m : ℕ
hm : 2 ≤ m
ihm :
  ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ) (hs : 2 * m - 1 ≤ #s),
    ∃ t ⊆ s, #t = m ∧ Dvd.dvd (α := ℤ) (↑m : ℤ) (∑ i ∈ t, a i)
n : ℕ
hn : 2 ≤ n
ihn :
  ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ) (hs : 2 * n - 1 ≤ #s),
    ∃ t ⊆ s, #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, a i)
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * (m * n) - 1 ≤ #s
this :
  ∀ k ≤ 2 * m - 1,
    ∃ (𝒜 : Finset (Finset ι)),
      #𝒜 = k ∧
        (↑𝒜 : Set (Finset ι)).Pairwise Disjoint ∧
          ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, a i)
⊢ ∃ t ⊆ s, #t = m * n ∧ Dvd.dvd (α := ℤ) (↑(m * n) : ℤ) (∑ i ∈ t, a i)
have obtain : ∀ (𝒜 : Finset (Finset ι)) (h𝒜card : #𝒜 = 2 * m - 1) (h𝒜disj : (↑𝒜 : Set (Finset ι)).Pairwise Disjoint)
  (h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, a i)),
  ∃ t ⊆ s, #t = m * n ∧ Dvd.dvd (α := ℤ) (↑(m * n) : ℤ) (∑ i ∈ t, a i)
Tactic: obtain ⟨𝒜, h𝒜card, h𝒜disj, h𝒜⟩ := this _ le_rfl
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ErdosGinzburgZiv (goal)
Goal:
m : ℕ
hm : 2 ≤ m
ihm :
  ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ) (hs : 2 * m - 1 ≤ #s),
    ∃ t ⊆ s, #t = m ∧ Dvd.dvd (α := ℤ) (↑m : ℤ) (∑ i ∈ t, a i)
n : ℕ
hn : 2 ≤ n
ihn :
  ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ) (hs : 2 * n - 1 ≤ #s),
    ∃ t ⊆ s, #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, a i)
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * (m * n) - 1 ≤ #s
this :
  ∀ k ≤ 2 * m - 1,
    ∃ (𝒜 : Finset (Finset ι)),
      #𝒜 = k ∧
        (↑𝒜 : Set (Finset ι)).Pairwise Disjoint ∧
          ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, a i)
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = 2 * m - 1
h𝒜disj : (↑𝒜 : Set (Finset ι)).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, a i)
⊢ ∃ t ⊆ s, #t = m * n ∧ Dvd.dvd (α := ℤ) (↑(m * n) : ℤ) (∑ i ∈ t, a i)
have obtain : ∀ (ℬ : Finset (Finset ι)) (hℬ𝒜 : ℬ ⊆ 𝒜) (hℬcard : #ℬ = m)
  (hℬ : Dvd.dvd (α := ℤ) (↑m : ℤ) (∑ i ∈ ℬ, HDiv.hDiv (α := ℤ) (∑ i ∈ i, a i) (↑n : ℤ))),
  ∃ t ⊆ s, #t = m * n ∧ Dvd.dvd (α := ℤ) (↑(m * n) : ℤ) (∑ i ∈ t, a i)
Tactic: obtain ⟨ℬ, hℬ𝒜, hℬcard, hℬ⟩ := ihm (fun t ↦ (∑ i ∈ t, a i) / n) h𝒜card.ge
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ErdosGinzburgZiv (goal)
Goal:
m : ℕ
hm : 2 ≤ m
ihm :
  ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ) (hs : 2 * m - 1 ≤ #s),
    ∃ t ⊆ s, #t = m ∧ Dvd.dvd (α := ℤ) (↑m : ℤ) (∑ i ∈ t, a i)
n : ℕ
hn : 2 ≤ n
ihn :
  ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ) (hs : 2 * n - 1 ≤ #s),
    ∃ t ⊆ s, #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, a i)
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * (m * n) - 1 ≤ #s
this :
  ∀ k ≤ 2 * m - 1,
    ∃ (𝒜 : Finset (Finset ι)),
      #𝒜 = k ∧
        (↑𝒜 : Set (Finset ι)).Pairwise Disjoint ∧
          ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, a i)
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = 2 * m - 1
h𝒜disj : (↑𝒜 : Set (Finset ι)).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, a i)
ℬ : Finset (Finset ι)
hℬ𝒜 : ℬ ⊆ 𝒜
hℬcard : #ℬ = m
hℬ : Dvd.dvd (α := ℤ) (↑m : ℤ) (∑ i ∈ ℬ, HDiv.hDiv (α := ℤ) (∑ i ∈ i, a i) (↑n : ℤ))
⊢ ∃ t ⊆ s, #t = m * n ∧ Dvd.dvd (α := ℤ) (↑(m * n) : ℤ) (∑ i ∈ t, a i)
have refine_1 : card (α := ι) (ℬ.biUnion fun (x : Finset ι) ↦ x) = m * n
Tactic: refine ⟨ℬ.biUnion fun x ↦ x, biUnion_subset.2 fun t ht ↦ (h𝒜 <| hℬ𝒜 ht).1, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ErdosGinzburgZiv (goal)
Goal:
m : ℕ
hm : 2 ≤ m
ihm :
  ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ) (hs : 2 * m - 1 ≤ #s),
    ∃ t ⊆ s, #t = m ∧ Dvd.dvd (α := ℤ) (↑m : ℤ) (∑ i ∈ t, a i)
n : ℕ
hn : 2 ≤ n
ihn :
  ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ) (hs : 2 * n - 1 ≤ #s),
    ∃ t ⊆ s, #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, a i)
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * (m * n) - 1 ≤ #s
this :
  ∀ k ≤ 2 * m - 1,
    ∃ (𝒜 : Finset (Finset ι)),
      #𝒜 = k ∧
        (↑𝒜 : Set (Finset ι)).Pairwise Disjoint ∧
          ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, a i)
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = 2 * m - 1
h𝒜disj : (↑𝒜 : Set (Finset ι)).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, a i)
ℬ : Finset (Finset ι)
hℬ𝒜 : ℬ ⊆ 𝒜
hℬcard : #ℬ = m
hℬ : Dvd.dvd (α := ℤ) (↑m : ℤ) (∑ i ∈ ℬ, HDiv.hDiv (α := ℤ) (∑ i ∈ i, a i) (↑n : ℤ))
refine_1 : card (α := ι) (ℬ.biUnion fun (x : Finset ι) ↦ x) = m * n
⊢ ∃ t ⊆ s, #t = m * n ∧ Dvd.dvd (α := ℤ) (↑(m * n) : ℤ) (∑ i ∈ t, a i)
have refine_2 : Dvd.dvd (α := ℤ) (↑(m * n) : ℤ) (∑ i ∈ ℬ.biUnion fun (x : Finset ι) ↦ x, a i)
Tactic: refine ⟨ℬ.biUnion fun x ↦ x, biUnion_subset.2 fun t ht ↦ (h𝒜 <| hℬ𝒜 ht).1, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ErdosGinzburgZiv (goal)
Goal:
m : ℕ
hm : 2 ≤ m
ihm :
  ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ) (hs : 2 * m - 1 ≤ #s),
    ∃ t ⊆ s, #t = m ∧ Dvd.dvd (α := ℤ) (↑m : ℤ) (∑ i ∈ t, a i)
n : ℕ
hn : 2 ≤ n
ihn :
  ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ) (hs : 2 * n - 1 ≤ #s),
    ∃ t ⊆ s, #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, a i)
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * (m * n) - 1 ≤ #s
this :
  ∀ k ≤ 2 * m - 1,
    ∃ (𝒜 : Finset (Finset ι)),
      #𝒜 = k ∧
        (↑𝒜 : Set (Finset ι)).Pairwise Disjoint ∧
          ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, a i)
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = 2 * m - 1
h𝒜disj : (↑𝒜 : Set (Finset ι)).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, a i)
ℬ : Finset (Finset ι)
hℬ𝒜 : ℬ ⊆ 𝒜
hℬcard : #ℬ = m
hℬ : Dvd.dvd (α := ℤ) (↑m : ℤ) (∑ i ∈ ℬ, HDiv.hDiv (α := ℤ) (∑ i ∈ i, a i) (↑n : ℤ))
⊢ card (α := ι) (ℬ.biUnion fun (x : Finset ι) ↦ x) = m * n
have refine_1 : ∑ u ∈ ℬ, #u = m * n
Tactic: rw [card_biUnion (h𝒜disj.mono hℬ𝒜), sum_const_nat fun t ht ↦ (h𝒜 <| hℬ𝒜 ht).2.1, hℬcard]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ErdosGinzburgZiv (goal)
Goal:
m : ℕ
hm : 2 ≤ m
ihm :
  ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ) (hs : 2 * m - 1 ≤ #s),
    ∃ t ⊆ s, #t = m ∧ Dvd.dvd (α := ℤ) (↑m : ℤ) (∑ i ∈ t, a i)
n : ℕ
hn : 2 ≤ n
ihn :
  ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ) (hs : 2 * n - 1 ≤ #s),
    ∃ t ⊆ s, #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, a i)
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * (m * n) - 1 ≤ #s
this :
  ∀ k ≤ 2 * m - 1,
    ∃ (𝒜 : Finset (Finset ι)),
      #𝒜 = k ∧
        (↑𝒜 : Set (Finset ι)).Pairwise Disjoint ∧
          ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, a i)
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = 2 * m - 1
h𝒜disj : (↑𝒜 : Set (Finset ι)).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, a i)
ℬ : Finset (Finset ι)
hℬ𝒜 : ℬ ⊆ 𝒜
hℬcard : #ℬ = m
hℬ : Dvd.dvd (α := ℤ) (↑m : ℤ) (∑ i ∈ ℬ, HDiv.hDiv (α := ℤ) (∑ i ∈ i, a i) (↑n : ℤ))
refine_1 : ∑ u ∈ ℬ, #u = m * n
⊢ card (α := ι) (ℬ.biUnion fun (x : Finset ι) ↦ x) = m * n
have refine_1₁ : #ℬ * n = m * n
Tactic: rw [card_biUnion (h𝒜disj.mono hℬ𝒜), sum_const_nat fun t ht ↦ (h𝒜 <| hℬ𝒜 ht).2.1, hℬcard]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ErdosGinzburgZiv (goal)
Goal:
m : ℕ
hm : 2 ≤ m
ihm :
  ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ) (hs : 2 * m - 1 ≤ #s),
    ∃ t ⊆ s, #t = m ∧ Dvd.dvd (α := ℤ) (↑m : ℤ) (∑ i ∈ t, a i)
n : ℕ
hn : 2 ≤ n
ihn :
  ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ) (hs : 2 * n - 1 ≤ #s),
    ∃ t ⊆ s, #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, a i)
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * (m * n) - 1 ≤ #s
this :
  ∀ k ≤ 2 * m - 1,
    ∃ (𝒜 : Finset (Finset ι)),
      #𝒜 = k ∧
        (↑𝒜 : Set (Finset ι)).Pairwise Disjoint ∧
          ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, a i)
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = 2 * m - 1
h𝒜disj : (↑𝒜 : Set (Finset ι)).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, a i)
ℬ : Finset (Finset ι)
hℬ𝒜 : ℬ ⊆ 𝒜
hℬcard : #ℬ = m
hℬ : Dvd.dvd (α := ℤ) (↑m : ℤ) (∑ i ∈ ℬ, HDiv.hDiv (α := ℤ) (∑ i ∈ i, a i) (↑n : ℤ))
refine_1 : ∑ u ∈ ℬ, #u = m * n
refine_1₁ : #ℬ * n = m * n
⊢ card (α := ι) (ℬ.biUnion fun (x : Finset ι) ↦ x) = m * n
have refine_1₂ : m * n = m * n
Tactic: rw [card_biUnion (h𝒜disj.mono hℬ𝒜), sum_const_nat fun t ht ↦ (h𝒜 <| hℬ𝒜 ht).2.1, hℬcard]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ErdosGinzburgZiv (goal)
Goal:
m : ℕ
hm : 2 ≤ m
ihm :
  ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ) (hs : 2 * m - 1 ≤ #s),
    ∃ t ⊆ s, #t = m ∧ Dvd.dvd (α := ℤ) (↑m : ℤ) (∑ i ∈ t, a i)
n : ℕ
hn : 2 ≤ n
ihn :
  ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ) (hs : 2 * n - 1 ≤ #s),
    ∃ t ⊆ s, #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, a i)
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * (m * n) - 1 ≤ #s
this :
  ∀ k ≤ 2 * m - 1,
    ∃ (𝒜 : Finset (Finset ι)),
      #𝒜 = k ∧
        (↑𝒜 : Set (Finset ι)).Pairwise Disjoint ∧
          ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, a i)
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = 2 * m - 1
h𝒜disj : (↑𝒜 : Set (Finset ι)).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, a i)
ℬ : Finset (Finset ι)
hℬ𝒜 : ℬ ⊆ 𝒜
hℬcard : #ℬ = m
hℬ : Dvd.dvd (α := ℤ) (↑m : ℤ) (∑ i ∈ ℬ, HDiv.hDiv (α := ℤ) (∑ i ∈ i, a i) (↑n : ℤ))
⊢ Dvd.dvd (α := ℤ) (↑(m * n) : ℤ) (∑ i ∈ ℬ.biUnion fun (x : Finset ι) ↦ x, a i)
have refine_2 : ∀ i ∈ ℬ, Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ i, a i)
Tactic: rwa [sum_biUnion, Int.natCast_mul, mul_comm, ← Int.dvd_div_iff_mul_dvd, Int.sum_div]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ErdosGinzburgZiv (goal)
Goal:
m : ℕ
hm : 2 ≤ m
ihm :
  ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ) (hs : 2 * m - 1 ≤ #s),
    ∃ t ⊆ s, #t = m ∧ Dvd.dvd (α := ℤ) (↑m : ℤ) (∑ i ∈ t, a i)
n : ℕ
hn : 2 ≤ n
ihn :
  ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ) (hs : 2 * n - 1 ≤ #s),
    ∃ t ⊆ s, #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, a i)
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * (m * n) - 1 ≤ #s
this :
  ∀ k ≤ 2 * m - 1,
    ∃ (𝒜 : Finset (Finset ι)),
      #𝒜 = k ∧
        (↑𝒜 : Set (Finset ι)).Pairwise Disjoint ∧
          ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, a i)
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = 2 * m - 1
h𝒜disj : (↑𝒜 : Set (Finset ι)).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, a i)
ℬ : Finset (Finset ι)
hℬ𝒜 : ℬ ⊆ 𝒜
hℬcard : #ℬ = m
hℬ : Dvd.dvd (α := ℤ) (↑m : ℤ) (∑ i ∈ ℬ, HDiv.hDiv (α := ℤ) (∑ i ∈ i, a i) (↑n : ℤ))
refine_2 : ∀ i ∈ ℬ, Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ i, a i)
⊢ Dvd.dvd (α := ℤ) (↑(m * n) : ℤ) (∑ i ∈ ℬ.biUnion fun (x : Finset ι) ↦ x, a i)
have refine_2₁ : Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ x ∈ ℬ, ∑ i ∈ x, a i)
Tactic: rwa [sum_biUnion, Int.natCast_mul, mul_comm, ← Int.dvd_div_iff_mul_dvd, Int.sum_div]