awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ErdosGinzburgZiv (hypothesis)
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
k : ℕ
ih :
  ∀ (hk : 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)
hk : k + 1 ≤ 2 * m - 1
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = k
h𝒜disj : (↑𝒜 : Set (Finset ι)).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, a i)
this : 2 * n - 1 ≤ #(s \ 𝒜.biUnion id)
t₀ : Finset ι
ht₀ : t₀ ⊆ s \ 𝒜.biUnion id
ht₀card : #t₀ = n
ht₀sum : Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t₀, a i)
h : t₀ ∈ 𝒜
hn₁ : LE.le (α := ℕ) 2 0
ihn₁ :
  ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ) (hs : HMul.hMul (α := ℕ) 2 0 - 1 ≤ #s),
    ∃ t ⊆ s, #t = 0 ∧ Dvd.dvd (α := ℤ) (↑0 : ℤ) (∑ i ∈ t, a i)
hs₁ : 2 * (m * 0) - 1 ≤ #s
⊢ False
have ih₁ : ∀ (hk : k ≤ 2 * m - 1),
  ∃ (𝒜 : Finset (Finset ι)),
    #𝒜 = k ∧
      (↑𝒜 : Set (Finset ι)).Pairwise Disjoint ∧
        ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = 0 ∧ Dvd.dvd (α := ℤ) (↑0 : ℤ) (∑ i ∈ t, a i)
Tactic: obtain rfl : n = 0 := by
        simpa [← card_eq_zero, ht₀card] using sdiff_disjoint.mono ht₀ <| subset_biUnion_of_mem id h
Cleared hypotheses: n, hn, ihn, hs, ih, h𝒜, this, ht₀card, ht₀sum
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ErdosGinzburgZiv (hypothesis)
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
k : ℕ
ih :
  ∀ (hk : 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)
hk : k + 1 ≤ 2 * m - 1
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = k
h𝒜disj : (↑𝒜 : Set (Finset ι)).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, a i)
this : 2 * n - 1 ≤ #(s \ 𝒜.biUnion id)
t₀ : Finset ι
ht₀ : t₀ ⊆ s \ 𝒜.biUnion id
ht₀card : #t₀ = n
ht₀sum : Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t₀, a i)
h : t₀ ∈ 𝒜
hn₁ : LE.le (α := ℕ) 2 0
ihn₁ :
  ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ) (hs : HMul.hMul (α := ℕ) 2 0 - 1 ≤ #s),
    ∃ t ⊆ s, #t = 0 ∧ Dvd.dvd (α := ℤ) (↑0 : ℤ) (∑ i ∈ t, a i)
hs₁ : 2 * (m * 0) - 1 ≤ #s
ih₁ :
  ∀ (hk : k ≤ 2 * m - 1),
    ∃ (𝒜 : Finset (Finset ι)),
      #𝒜 = k ∧
        (↑𝒜 : Set (Finset ι)).Pairwise Disjoint ∧
          ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = 0 ∧ Dvd.dvd (α := ℤ) (↑0 : ℤ) (∑ i ∈ t, a i)
⊢ False
have h𝒜₁ : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = 0 ∧ Dvd.dvd (α := ℤ) (↑0 : ℤ) (∑ i ∈ t, a i)
Tactic: obtain rfl : n = 0 := by
        simpa [← card_eq_zero, ht₀card] using sdiff_disjoint.mono ht₀ <| subset_biUnion_of_mem id h
Cleared hypotheses: n, hn, ihn, hs, ih, h𝒜, this, ht₀card, ht₀sum
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ErdosGinzburgZiv (hypothesis)
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
k : ℕ
ih :
  ∀ (hk : 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)
hk : k + 1 ≤ 2 * m - 1
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = k
h𝒜disj : (↑𝒜 : Set (Finset ι)).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, a i)
this : 2 * n - 1 ≤ #(s \ 𝒜.biUnion id)
t₀ : Finset ι
ht₀ : t₀ ⊆ s \ 𝒜.biUnion id
ht₀card : #t₀ = n
ht₀sum : Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t₀, a i)
h : t₀ ∈ 𝒜
hn₁ : LE.le (α := ℕ) 2 0
ihn₁ :
  ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ) (hs : HMul.hMul (α := ℕ) 2 0 - 1 ≤ #s),
    ∃ t ⊆ s, #t = 0 ∧ Dvd.dvd (α := ℤ) (↑0 : ℤ) (∑ i ∈ t, a i)
hs₁ : 2 * (m * 0) - 1 ≤ #s
ih₁ :
  ∀ (hk : k ≤ 2 * m - 1),
    ∃ (𝒜 : Finset (Finset ι)),
      #𝒜 = k ∧
        (↑𝒜 : Set (Finset ι)).Pairwise Disjoint ∧
          ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = 0 ∧ Dvd.dvd (α := ℤ) (↑0 : ℤ) (∑ i ∈ t, a i)
h𝒜₁ : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = 0 ∧ Dvd.dvd (α := ℤ) (↑0 : ℤ) (∑ i ∈ t, a i)
⊢ False
have this₁ : HMul.hMul (α := ℕ) 2 0 - 1 ≤ #(s \ 𝒜.biUnion id)
Tactic: obtain rfl : n = 0 := by
        simpa [← card_eq_zero, ht₀card] using sdiff_disjoint.mono ht₀ <| subset_biUnion_of_mem id h
Cleared hypotheses: n, hn, ihn, hs, ih, h𝒜, this, ht₀card, ht₀sum
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ErdosGinzburgZiv (hypothesis)
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
k : ℕ
ih :
  ∀ (hk : 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)
hk : k + 1 ≤ 2 * m - 1
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = k
h𝒜disj : (↑𝒜 : Set (Finset ι)).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, a i)
this : 2 * n - 1 ≤ #(s \ 𝒜.biUnion id)
t₀ : Finset ι
ht₀ : t₀ ⊆ s \ 𝒜.biUnion id
ht₀card : #t₀ = n
ht₀sum : Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t₀, a i)
h : t₀ ∈ 𝒜
hn₁ : LE.le (α := ℕ) 2 0
ihn₁ :
  ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ) (hs : HMul.hMul (α := ℕ) 2 0 - 1 ≤ #s),
    ∃ t ⊆ s, #t = 0 ∧ Dvd.dvd (α := ℤ) (↑0 : ℤ) (∑ i ∈ t, a i)
hs₁ : 2 * (m * 0) - 1 ≤ #s
ih₁ :
  ∀ (hk : k ≤ 2 * m - 1),
    ∃ (𝒜 : Finset (Finset ι)),
      #𝒜 = k ∧
        (↑𝒜 : Set (Finset ι)).Pairwise Disjoint ∧
          ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = 0 ∧ Dvd.dvd (α := ℤ) (↑0 : ℤ) (∑ i ∈ t, a i)
h𝒜₁ : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = 0 ∧ Dvd.dvd (α := ℤ) (↑0 : ℤ) (∑ i ∈ t, a i)
this₁ : HMul.hMul (α := ℕ) 2 0 - 1 ≤ #(s \ 𝒜.biUnion id)
⊢ False
have ht₀card₁ : #t₀ = 0
Tactic: obtain rfl : n = 0 := by
        simpa [← card_eq_zero, ht₀card] using sdiff_disjoint.mono ht₀ <| subset_biUnion_of_mem id h
Cleared hypotheses: n, hn, ihn, hs, ih, h𝒜, this, ht₀card, ht₀sum
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ErdosGinzburgZiv (hypothesis)
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
k : ℕ
ih :
  ∀ (hk : 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)
hk : k + 1 ≤ 2 * m - 1
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = k
h𝒜disj : (↑𝒜 : Set (Finset ι)).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, a i)
this : 2 * n - 1 ≤ #(s \ 𝒜.biUnion id)
t₀ : Finset ι
ht₀ : t₀ ⊆ s \ 𝒜.biUnion id
ht₀card : #t₀ = n
ht₀sum : Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t₀, a i)
h : t₀ ∈ 𝒜
hn₁ : LE.le (α := ℕ) 2 0
ihn₁ :
  ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ) (hs : HMul.hMul (α := ℕ) 2 0 - 1 ≤ #s),
    ∃ t ⊆ s, #t = 0 ∧ Dvd.dvd (α := ℤ) (↑0 : ℤ) (∑ i ∈ t, a i)
hs₁ : 2 * (m * 0) - 1 ≤ #s
ih₁ :
  ∀ (hk : k ≤ 2 * m - 1),
    ∃ (𝒜 : Finset (Finset ι)),
      #𝒜 = k ∧
        (↑𝒜 : Set (Finset ι)).Pairwise Disjoint ∧
          ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = 0 ∧ Dvd.dvd (α := ℤ) (↑0 : ℤ) (∑ i ∈ t, a i)
h𝒜₁ : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = 0 ∧ Dvd.dvd (α := ℤ) (↑0 : ℤ) (∑ i ∈ t, a i)
this₁ : HMul.hMul (α := ℕ) 2 0 - 1 ≤ #(s \ 𝒜.biUnion id)
ht₀card₁ : #t₀ = 0
⊢ False
have ht₀sum₁ : Dvd.dvd (α := ℤ) (↑0 : ℤ) (∑ i ∈ t₀, a i)
Tactic: obtain rfl : n = 0 := by
        simpa [← card_eq_zero, ht₀card] using sdiff_disjoint.mono ht₀ <| subset_biUnion_of_mem id h
Cleared hypotheses: n, hn, ihn, hs, ih, h𝒜, this, ht₀card, ht₀sum
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ErdosGinzburgZiv (hypothesis)
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
k : ℕ
ih :
  ∀ (hk : 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)
hk : k + 1 ≤ 2 * m - 1
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = k
h𝒜disj : (↑𝒜 : Set (Finset ι)).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, a i)
this : 2 * n - 1 ≤ #(s \ 𝒜.biUnion id)
t₀ : Finset ι
ht₀ : t₀ ⊆ s \ 𝒜.biUnion id
ht₀card : #t₀ = n
ht₀sum : Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t₀, a i)
⊢ ∃ (𝒜 : Finset (Finset ι)),
    #𝒜 = k + 1 ∧
      (↑𝒜 : Set (Finset ι)).Pairwise Disjoint ∧
        ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, a i)
have this₁ : t₀ ∉ 𝒜
Tactic: have : t₀ ∉ 𝒜 := by
      rintro h
      obtain rfl : n = 0 := by
        simpa [← card_eq_zero, ht₀card] using sdiff_disjoint.mono ht₀ <| subset_biUnion_of_mem id h
      lia
-- 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
k : ℕ
ih :
  ∀ (hk : 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)
hk : k + 1 ≤ 2 * m - 1
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = k
h𝒜disj : (↑𝒜 : Set (Finset ι)).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, a i)
this_1 : 2 * n - 1 ≤ #(s \ 𝒜.biUnion id)
t₀ : Finset ι
ht₀ : t₀ ⊆ s \ 𝒜.biUnion id
ht₀card : #t₀ = n
ht₀sum : Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t₀, a i)
this : t₀ ∉ 𝒜
⊢ #(cons t₀ 𝒜 this) = k + 1
have rw : #𝒜 + 1 = k + 1
Tactic: rw [card_cons, 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
k : ℕ
ih :
  ∀ (hk : 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)
hk : k + 1 ≤ 2 * m - 1
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = k
h𝒜disj : (↑𝒜 : Set (Finset ι)).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, a i)
this_1 : 2 * n - 1 ≤ #(s \ 𝒜.biUnion id)
t₀ : Finset ι
ht₀ : t₀ ⊆ s \ 𝒜.biUnion id
ht₀card : #t₀ = n
ht₀sum : Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t₀, a i)
this : t₀ ∉ 𝒜
rw : #𝒜 + 1 = k + 1
⊢ #(cons t₀ 𝒜 this) = k + 1
have rw₁ : k + 1 = k + 1
Tactic: rw [card_cons, 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
k : ℕ
ih :
  ∀ (hk : 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)
hk : k + 1 ≤ 2 * m - 1
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = k
h𝒜disj : (↑𝒜 : Set (Finset ι)).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, a i)
this_1 : 2 * n - 1 ≤ #(s \ 𝒜.biUnion id)
t₀ : Finset ι
ht₀ : t₀ ⊆ s \ 𝒜.biUnion id
ht₀card : #t₀ = n
ht₀sum : Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t₀, a i)
this : t₀ ∉ 𝒜
⊢ ∃ (𝒜 : Finset (Finset ι)),
    #𝒜 = k + 1 ∧
      (↑𝒜 : Set (Finset ι)).Pairwise Disjoint ∧
        ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, a i)
have composite : (↑(cons t₀ 𝒜 this) : Set (Finset ι)).Pairwise Disjoint
Tactic: refine ⟨𝒜.cons t₀ this, by rw [card_cons, 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
k : ℕ
ih :
  ∀ (hk : 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)
hk : k + 1 ≤ 2 * m - 1
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = k
h𝒜disj : (↑𝒜 : Set (Finset ι)).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, a i)
this_1 : 2 * n - 1 ≤ #(s \ 𝒜.biUnion id)
t₀ : Finset ι
ht₀ : t₀ ⊆ s \ 𝒜.biUnion id
ht₀card : #t₀ = n
ht₀sum : Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t₀, a i)
this : t₀ ∉ 𝒜
composite : (↑(cons t₀ 𝒜 this) : Set (Finset ι)).Pairwise Disjoint
⊢ ∃ (𝒜 : Finset (Finset ι)),
    #𝒜 = k + 1 ∧
      (↑𝒜 : Set (Finset ι)).Pairwise Disjoint ∧
        ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, a i)
have composite₁ : ∀ ⦃t : Finset ι⦄, t ∈ cons t₀ 𝒜 this → t ⊆ s ∧ #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, a i)
Tactic: refine ⟨𝒜.cons t₀ this, by rw [card_cons, 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
k : ℕ
ih :
  ∀ (hk : 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)
hk : k + 1 ≤ 2 * m - 1
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = k
h𝒜disj : (↑𝒜 : Set (Finset ι)).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, a i)
this_1 : 2 * n - 1 ≤ #(s \ 𝒜.biUnion id)
t₀ : Finset ι
ht₀ : t₀ ⊆ s \ 𝒜.biUnion id
ht₀card : #t₀ = n
ht₀sum : Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t₀, a i)
this : t₀ ∉ 𝒜
⊢ (↑(cons t₀ 𝒜 this) : Set (Finset ι)).Pairwise Disjoint
have composite : (↑𝒜 : Set (Finset ι)).Pairwise Disjoint ∧ ∀ b ∈ 𝒜, ¬t₀ = b → Disjoint t₀ b
Tactic: simp only [cons_eq_insert, coe_insert, Set.pairwise_insert_of_symmetric symmetric_disjoint,
        mem_coe, ne_eq]
-- 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
k : ℕ
ih :
  ∀ (hk : 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)
hk : k + 1 ≤ 2 * m - 1
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = k
h𝒜disj : (↑𝒜 : Set (Finset ι)).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, a i)
this_1 : 2 * n - 1 ≤ #(s \ 𝒜.biUnion id)
t₀ : Finset ι
ht₀ : t₀ ⊆ s \ 𝒜.biUnion id
ht₀card : #t₀ = n
ht₀sum : Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t₀, a i)
this : t₀ ∉ 𝒜
⊢ ∀ ⦃t : Finset ι⦄, t ∈ cons t₀ 𝒜 this → t ⊆ s ∧ #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, a i)
have composite : t₀ ⊆ s ∧
  #t₀ = n ∧
    Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t₀, a i) ∧
      ∀ a_1 ∈ 𝒜, a_1 ⊆ s ∧ #a_1 = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ a_1, a i)
Tactic: simp only [cons_eq_insert, mem_insert, forall_eq_or_imp, and_assoc]
-- 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
k : ℕ
hk : 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)
have composite : ∀ (hk : 0 ≤ 2 * m - 1),
  ∃ (𝒜 : Finset (Finset ι)),
    #𝒜 = 0 ∧
      (↑𝒜 : Set (Finset ι)).Pairwise Disjoint ∧
        ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, a i)
Tactic: induction k with
    -- For `k = 0`, the empty family trivially works.
    | zero => exact ⟨∅, by simp⟩
    | succ k ih =>
    -- At `k + 1`, call `𝒜` the existing family of size `k ≤ 2 * m - 2`.
    obtain ⟨𝒜, h𝒜card, h𝒜disj, h𝒜⟩ := ih (Nat.le_of_succ_le hk)
    -- There are at least `2 * (m * n) - 1 - k * n ≥ 2 * m - 1` elements in `s` that have not been
    -- taken in any element of `𝒜`.
    have : 2 * n - 1 ≤ #(s \ 𝒜.biUnion id) := by
      calc
        _ ≤ (2 * m - k) * n - 1 := by gcongr; lia
        _ = (2 * (m * n) - 1) - ∑ t ∈ 𝒜, #t := by
          rw [tsub_mul, mul_assoc, tsub_right_comm, sum_const_nat fun t ht ↦ (h𝒜 ht).2.1, h𝒜card]
        _ ≤ #s - #(𝒜.biUnion id) := by gcongr; exact card_biUnion_le
        _ ≤ #(s \ 𝒜.biUnion id) := le_card_sdiff ..
    -- So by the induction hypothesis on `n` we can find a new set `t` of size `n` and sum divisible
    -- by `n`.
    obtain ⟨t₀, ht₀, ht₀card, ht₀sum⟩ := ihn a this
    -- This set is distinct and disjoint from the previous ones, so we are done.
    have : t₀ ∉ 𝒜 := by
      rintro h
      obtain rfl : n = 0 := by
        simpa [← card_eq_zero, ht₀card] using sdiff_disjoint.mono ht₀ <| subset_biUnion_of_mem id h
      lia
    refine ⟨𝒜.cons t₀ this, by rw [card_cons, h𝒜card], ?_, ?_⟩
    · simp only [cons_eq_insert, coe_insert, Set.pairwise_insert_of_symmetric symmetric_disjoint,
        mem_coe, ne_eq]
      exact ⟨h𝒜disj, fun t ht _ ↦ sdiff_disjoint.mono ht₀ <| subset_biUnion_of_mem id ht⟩
    · simp only [cons_eq_insert, mem_insert, forall_eq_or_imp, and_assoc]
      exact ⟨ht₀.trans sdiff_subset, ht₀card, ht₀sum, h𝒜⟩
Cleared hypotheses: k, hk
-- 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
k : ℕ
hk : k ≤ 2 * m - 1
composite :
  ∀ (hk : 0 ≤ 2 * m - 1),
    ∃ (𝒜 : Finset (Finset ι)),
      #𝒜 = 0 ∧
        (↑𝒜 : Set (Finset ι)).Pairwise Disjoint ∧
          ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, a i)
⊢ ∃ (𝒜 : Finset (Finset ι)),
    #𝒜 = k ∧
      (↑𝒜 : Set (Finset ι)).Pairwise Disjoint ∧
        ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, a i)
have composite₁ : ∀ (k : ℕ)
  (ih :
    ∀ (hk : 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))
  (hk : k + 1 ≤ 2 * m - 1),
  ∃ (𝒜 : Finset (Finset ι)),
    #𝒜 = k + 1 ∧
      (↑𝒜 : Set (Finset ι)).Pairwise Disjoint ∧
        ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, a i)
Tactic: induction k with
    -- For `k = 0`, the empty family trivially works.
    | zero => exact ⟨∅, by simp⟩
    | succ k ih =>
    -- At `k + 1`, call `𝒜` the existing family of size `k ≤ 2 * m - 2`.
    obtain ⟨𝒜, h𝒜card, h𝒜disj, h𝒜⟩ := ih (Nat.le_of_succ_le hk)
    -- There are at least `2 * (m * n) - 1 - k * n ≥ 2 * m - 1` elements in `s` that have not been
    -- taken in any element of `𝒜`.
    have : 2 * n - 1 ≤ #(s \ 𝒜.biUnion id) := by
      calc
        _ ≤ (2 * m - k) * n - 1 := by gcongr; lia
        _ = (2 * (m * n) - 1) - ∑ t ∈ 𝒜, #t := by
          rw [tsub_mul, mul_assoc, tsub_right_comm, sum_const_nat fun t ht ↦ (h𝒜 ht).2.1, h𝒜card]
        _ ≤ #s - #(𝒜.biUnion id) := by gcongr; exact card_biUnion_le
        _ ≤ #(s \ 𝒜.biUnion id) := le_card_sdiff ..
    -- So by the induction hypothesis on `n` we can find a new set `t` of size `n` and sum divisible
    -- by `n`.
    obtain ⟨t₀, ht₀, ht₀card, ht₀sum⟩ := ihn a this
    -- This set is distinct and disjoint from the previous ones, so we are done.
    have : t₀ ∉ 𝒜 := by
      rintro h
      obtain rfl : n = 0 := by
        simpa [← card_eq_zero, ht₀card] using sdiff_disjoint.mono ht₀ <| subset_biUnion_of_mem id h
      lia
    refine ⟨𝒜.cons t₀ this, by rw [card_cons, h𝒜card], ?_, ?_⟩
    · simp only [cons_eq_insert, coe_insert, Set.pairwise_insert_of_symmetric symmetric_disjoint,
        mem_coe, ne_eq]
      exact ⟨h𝒜disj, fun t ht _ ↦ sdiff_disjoint.mono ht₀ <| subset_biUnion_of_mem id ht⟩
    · simp only [cons_eq_insert, mem_insert, forall_eq_or_imp, and_assoc]
      exact ⟨ht₀.trans sdiff_subset, ht₀card, ht₀sum, h𝒜⟩
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ErdosGinzburgZiv (goal)
Goal:
n : ℕ
s : Multiset ℤ
hs : 2 * n - 1 ≤ s.card
⊢ ∃ t ≤ s, t.card = n ∧ (↑n : ℤ) ∣ t.sum
have obtain : ∀ (t : Finset (ℤ × ℕ)) (hts : t ⊆ s.toEnumFinset) (ht : #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, i.1)),
  ∃ t ≤ s, t.card = n ∧ (↑n : ℤ) ∣ t.sum
Tactic: obtain ⟨t, hts, ht⟩ := Int.erdos_ginzburg_ziv (s := s.toEnumFinset) Prod.fst (by simpa using hs)