awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
refine_2₁ : Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ x ∈ ℬ, ∑ i ∈ x, a i)
⊢ Dvd.dvd (α := ℤ) (↑(m * n) : ℤ) (∑ i ∈ ℬ.biUnion fun (x : Finset ι) ↦ x, a i)
have refine_2₂ : (↑ℬ : Set (Finset ι)).PairwiseDisjoint (α := Finset ι) fun (x : Finset ι) ↦ x
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
⊢ ∃ t ⊆ s, #t = m * n ∧ Dvd.dvd (α := ℤ) (↑(m * n) : ℤ) (∑ i ∈ t, a i)
have composite : ∀ 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)
Tactic: suffices ∀ k ≤ 2 * m - 1, ∃ 𝒜 : Finset (Finset ι), #𝒜 = k ∧
      (𝒜 : Set (Finset ι)).Pairwise _root_.Disjoint ∧
        ∀ ⦃t⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i by
     -- Assume `𝒜` is a family of `2 * m - 1` sets, each of size `n` and sum divisible by `n`.
      obtain ⟨𝒜, h𝒜card, h𝒜disj, h𝒜⟩ := this _ le_rfl
      -- By induction hypothesis on `m`, find a subfamily `ℬ` of size `m` such that the sum over
      -- `t ∈ ℬ` of `(∑ i ∈ t, a i) / n` is divisible by `m`.
      obtain ⟨ℬ, hℬ𝒜, hℬcard, hℬ⟩ := ihm (fun t ↦ (∑ i ∈ t, a i) / n) h𝒜card.ge
      -- We are done.
      refine ⟨ℬ.biUnion fun x ↦ x, biUnion_subset.2 fun t ht ↦ (h𝒜 <| hℬ𝒜 ht).1, ?_, ?_⟩
      · rw [card_biUnion (h𝒜disj.mono hℬ𝒜), sum_const_nat fun t ht ↦ (h𝒜 <| hℬ𝒜 ht).2.1, hℬcard]
      rwa [sum_biUnion, Int.natCast_mul, mul_comm, ← Int.dvd_div_iff_mul_dvd, Int.sum_div]
      · exact fun t ht ↦ (h𝒜 <| hℬ𝒜 ht).2.2
      · exact dvd_sum fun t ht ↦ (h𝒜 <| hℬ𝒜 ht).2.2
      · exact h𝒜disj.mono hℬ𝒜
-- 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 ι)),
    #𝒜 = k + 1 ∧
      (↑𝒜 : Set (Finset ι)).Pairwise Disjoint ∧
        ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, a i)
have composite : ∀ (𝒜 : 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)),
  ∃ (𝒜 : Finset (Finset ι)),
    #𝒜 = k + 1 ∧
      (↑𝒜 : Set (Finset ι)).Pairwise Disjoint ∧
        ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, a i)
Tactic: obtain ⟨𝒜, h𝒜card, h𝒜disj, h𝒜⟩ := ih (Nat.le_of_succ_le 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 : ℕ
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)
⊢ 2 * n - 1 ≤ (2 * m - k) * n - 1
have h : 2 ≤ 2 * m - k
Tactic: gcongr
-- 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)
⊢ (2 * m - k) * n - 1 = 2 * (m * n) - 1 - ∑ t ∈ 𝒜, #t
have rw : 2 * m * n - k * n - 1 = 2 * (m * n) - 1 - ∑ t ∈ 𝒜, #t
Tactic: rw [tsub_mul, mul_assoc, tsub_right_comm, sum_const_nat fun t ht ↦ (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
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)
rw : 2 * m * n - k * n - 1 = 2 * (m * n) - 1 - ∑ t ∈ 𝒜, #t
⊢ (2 * m - k) * n - 1 = 2 * (m * n) - 1 - ∑ t ∈ 𝒜, #t
have rw₁ : 2 * (m * n) - k * n - 1 = 2 * (m * n) - 1 - ∑ t ∈ 𝒜, #t
Tactic: rw [tsub_mul, mul_assoc, tsub_right_comm, sum_const_nat fun t ht ↦ (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
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)
rw : 2 * m * n - k * n - 1 = 2 * (m * n) - 1 - ∑ t ∈ 𝒜, #t
rw₁ : 2 * (m * n) - k * n - 1 = 2 * (m * n) - 1 - ∑ t ∈ 𝒜, #t
⊢ (2 * m - k) * n - 1 = 2 * (m * n) - 1 - ∑ t ∈ 𝒜, #t
have rw₂ : 2 * (m * n) - 1 - k * n = 2 * (m * n) - 1 - ∑ t ∈ 𝒜, #t
Tactic: rw [tsub_mul, mul_assoc, tsub_right_comm, sum_const_nat fun t ht ↦ (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
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)
rw : 2 * m * n - k * n - 1 = 2 * (m * n) - 1 - ∑ t ∈ 𝒜, #t
rw₁ : 2 * (m * n) - k * n - 1 = 2 * (m * n) - 1 - ∑ t ∈ 𝒜, #t
rw₂ : 2 * (m * n) - 1 - k * n = 2 * (m * n) - 1 - ∑ t ∈ 𝒜, #t
⊢ (2 * m - k) * n - 1 = 2 * (m * n) - 1 - ∑ t ∈ 𝒜, #t
have rw₃ : 2 * (m * n) - 1 - k * n = 2 * (m * n) - 1 - #𝒜 * n
Tactic: rw [tsub_mul, mul_assoc, tsub_right_comm, sum_const_nat fun t ht ↦ (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
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)
rw : 2 * m * n - k * n - 1 = 2 * (m * n) - 1 - ∑ t ∈ 𝒜, #t
rw₁ : 2 * (m * n) - k * n - 1 = 2 * (m * n) - 1 - ∑ t ∈ 𝒜, #t
rw₂ : 2 * (m * n) - 1 - k * n = 2 * (m * n) - 1 - ∑ t ∈ 𝒜, #t
rw₃ : 2 * (m * n) - 1 - k * n = 2 * (m * n) - 1 - #𝒜 * n
⊢ (2 * m - k) * n - 1 = 2 * (m * n) - 1 - ∑ t ∈ 𝒜, #t
have rw₄ : 2 * (m * n) - 1 - k * n = 2 * (m * n) - 1 - k * n
Tactic: rw [tsub_mul, mul_assoc, tsub_right_comm, sum_const_nat fun t ht ↦ (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
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)
⊢ 2 * (m * n) - 1 - ∑ t ∈ 𝒜, #t ≤ #s - #(𝒜.biUnion id)
have hcd : #(𝒜.biUnion id) ≤ ∑ t ∈ 𝒜, #t
Tactic: gcongr
-- 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)
⊢ 2 * n - 1 ≤ #(s \ 𝒜.biUnion id)
have _ : 2 * n - 1 ≤ (2 * m - k) * n - 1
Tactic: 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 ..
-- 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)
_ : 2 * n - 1 ≤ (2 * m - k) * n - 1
⊢ 2 * n - 1 ≤ #(s \ 𝒜.biUnion id)
have _₁ : (2 * m - k) * n - 1 = 2 * (m * n) - 1 - ∑ t ∈ 𝒜, #t
Tactic: 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 ..
-- 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)
_ : 2 * n - 1 ≤ (2 * m - k) * n - 1
_₁ : (2 * m - k) * n - 1 = 2 * (m * n) - 1 - ∑ t ∈ 𝒜, #t
⊢ 2 * n - 1 ≤ #(s \ 𝒜.biUnion id)
have _₂ : 2 * (m * n) - 1 - ∑ t ∈ 𝒜, #t ≤ #s - #(𝒜.biUnion id)
Tactic: 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 ..
-- 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)
⊢ ∃ (𝒜 : Finset (Finset ι)),
    #𝒜 = k + 1 ∧
      (↑𝒜 : Set (Finset ι)).Pairwise Disjoint ∧
        ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, a i)
have this : 2 * n - 1 ≤ #(s \ 𝒜.biUnion id)
Tactic: 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 ..
-- 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 : 2 * n - 1 ≤ #(s \ 𝒜.biUnion id)
⊢ ∃ (𝒜 : 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 ι) (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)
Tactic: obtain ⟨t₀, ht₀, ht₀card, ht₀sum⟩ := ihn a this
-- 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₀ ∈ 𝒜
⊢ False
have hn₁ : LE.le (α := ℕ) 2 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
⊢ False
have 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)
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)
⊢ False
have hs₁ : 2 * (m * 0) - 1 ≤ #s
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