-- Mathlib/Combinatorics/Additive/ErdosGinzburgZiv.lean
theorem Int.erdos_ginzburg_ziv (a : ι → ℤ) (hs : 2 * n - 1 ≤ #s) :
    ∃ t ⊆ s, #t = n ∧ ↑n ∣ ∑ i ∈ t, a i

Proof state:
m : ℕ
hm : 2 ≤ m
ihm : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * m - 1 ≤ #s → ∃ t ⊆ s, #t = m ∧ ↑m ∣ ∑ i ∈ t, a i
n : ℕ
hn : 2 ≤ n
ihn : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * n - 1 ≤ #s → ∃ t ⊆ s, #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * (m * n) - 1 ≤ #s
hk : 0 ≤ 2 * m - 1
⊢ #∅ = 0 ∧ (↑∅).Pairwise Disjoint ∧ ∀ ⦃t : Finset ι⦄, t ∈ ∅ → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i

Tactic:
simp

Result:
no goals

Proof state:
case composite.succ.intro.intro.intro.intro.intro.intro.refine_2
m : ℕ
hm : 2 ≤ m
ihm : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * m - 1 ≤ #s → ∃ t ⊆ s, #t = m ∧ ↑m ∣ ∑ i ∈ t, a i
n : ℕ
hn : 2 ≤ n
ihn : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * n - 1 ≤ #s → ∃ t ⊆ s, #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * (m * n) - 1 ≤ #s
k : ℕ
ih : k ≤ 2 * m - 1 → ∃ 𝒜, #𝒜 = k ∧ (↑𝒜).Pairwise Disjoint ∧ ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
hk : k + 1 ≤ 2 * m - 1
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = k
h𝒜disj : (↑𝒜).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑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 : ↑n ∣ ∑ i ∈ t₀, a i
this : t₀ ∉ 𝒜
⊢ ∀ ⦃t : Finset ι⦄, t ∈ cons t₀ 𝒜 this → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i

Tactic:
simp only [cons_eq_insert, mem_insert, forall_eq_or_imp, and_assoc]

Result:
case composite.succ.intro.intro.intro.intro.intro.intro.refine_2
m : ℕ
hm : 2 ≤ m
ihm : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * m - 1 ≤ #s → ∃ t ⊆ s, #t = m ∧ ↑m ∣ ∑ i ∈ t, a i
n : ℕ
hn : 2 ≤ n
ihn : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * n - 1 ≤ #s → ∃ t ⊆ s, #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * (m * n) - 1 ≤ #s
k : ℕ
ih : k ≤ 2 * m - 1 → ∃ 𝒜, #𝒜 = k ∧ (↑𝒜).Pairwise Disjoint ∧ ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
hk : k + 1 ≤ 2 * m - 1
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = k
h𝒜disj : (↑𝒜).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑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 : ↑n ∣ ∑ i ∈ t₀, a i
this : t₀ ∉ 𝒜
⊢ t₀ ⊆ s ∧ #t₀ = n ∧ ↑n ∣ ∑ i ∈ t₀, a i ∧ ∀ a_1 ∈ 𝒜, a_1 ⊆ s ∧ #a_1 = n ∧ ↑n ∣ ∑ i ∈ a_1, a i

Proof state:
case intro.intro.intro.intro.intro.intro.refine_2
m : ℕ
hm : 2 ≤ m
ihm : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * m - 1 ≤ #s → ∃ t ⊆ s, #t = m ∧ ↑m ∣ ∑ i ∈ t, a i
n : ℕ
hn : 2 ≤ n
ihn : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * n - 1 ≤ #s → ∃ t ⊆ s, #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * (m * n) - 1 ≤ #s
this :
  ∀ k ≤ 2 * m - 1, ∃ 𝒜, #𝒜 = k ∧ (↑𝒜).Pairwise Disjoint ∧ ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = 2 * m - 1
h𝒜disj : (↑𝒜).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ℬ : Finset (Finset ι)
hℬ𝒜 : ℬ ⊆ 𝒜
hℬcard : #ℬ = m
hℬ : ↑m ∣ ∑ i ∈ ℬ, (∑ i ∈ i, a i) / ↑n
⊢ ∀ i ∈ ℬ, ↑n ∣ ∑ i ∈ i, a i

Tactic:
exact fun t ht ↦ (h𝒜 <| hℬ𝒜 ht).2.2

Result:
no goals

Proof state:
case intro.intro.intro
m : ℕ
hm : 2 ≤ m
ihm : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * m - 1 ≤ #s → ∃ t ⊆ s, #t = m ∧ ↑m ∣ ∑ i ∈ t, a i
n : ℕ
hn : 2 ≤ n
ihn : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * n - 1 ≤ #s → ∃ t ⊆ s, #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * (m * n) - 1 ≤ #s
this :
  ∀ k ≤ 2 * m - 1, ∃ 𝒜, #𝒜 = k ∧ (↑𝒜).Pairwise Disjoint ∧ ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = 2 * m - 1
h𝒜disj : (↑𝒜).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
⊢ ∃ t ⊆ s, #t = m * n ∧ ↑(m * n) ∣ ∑ i ∈ t, a i

Tactic:
obtain ⟨ℬ, hℬ𝒜, hℬcard, hℬ⟩ := ihm (fun t ↦ (∑ i ∈ t, a i) / n) h𝒜card.ge

Result:
case intro.intro.intro.intro.intro.intro
m : ℕ
hm : 2 ≤ m
ihm : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * m - 1 ≤ #s → ∃ t ⊆ s, #t = m ∧ ↑m ∣ ∑ i ∈ t, a i
n : ℕ
hn : 2 ≤ n
ihn : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * n - 1 ≤ #s → ∃ t ⊆ s, #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * (m * n) - 1 ≤ #s
this :
  ∀ k ≤ 2 * m - 1, ∃ 𝒜, #𝒜 = k ∧ (↑𝒜).Pairwise Disjoint ∧ ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = 2 * m - 1
h𝒜disj : (↑𝒜).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ℬ : Finset (Finset ι)
hℬ𝒜 : ℬ ⊆ 𝒜
hℬcard : #ℬ = m
hℬ : ↑m ∣ ∑ i ∈ ℬ, (∑ i ∈ i, a i) / ↑n
⊢ ∃ t ⊆ s, #t = m * n ∧ ↑(m * n) ∣ ∑ i ∈ t, a i

Proof state:
case intro.intro.intro.intro.intro.intro
m : ℕ
hm : 2 ≤ m
ihm : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * m - 1 ≤ #s → ∃ t ⊆ s, #t = m ∧ ↑m ∣ ∑ i ∈ t, a i
n : ℕ
hn : 2 ≤ n
ihn : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * n - 1 ≤ #s → ∃ t ⊆ s, #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * (m * n) - 1 ≤ #s
this :
  ∀ k ≤ 2 * m - 1, ∃ 𝒜, #𝒜 = k ∧ (↑𝒜).Pairwise Disjoint ∧ ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = 2 * m - 1
h𝒜disj : (↑𝒜).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ℬ : Finset (Finset ι)
hℬ𝒜 : ℬ ⊆ 𝒜
hℬcard : #ℬ = m
hℬ : ↑m ∣ ∑ i ∈ ℬ, (∑ i ∈ i, a i) / ↑n
⊢ ∃ t ⊆ s, #t = m * n ∧ ↑(m * n) ∣ ∑ i ∈ t, a i

Tactic:
refine ⟨ℬ.biUnion fun x ↦ x, biUnion_subset.2 fun t ht ↦ (h𝒜 <| hℬ𝒜 ht).1, ?_, ?_⟩

Result:
case intro.intro.intro.intro.intro.intro.refine_1
m : ℕ
hm : 2 ≤ m
ihm : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * m - 1 ≤ #s → ∃ t ⊆ s, #t = m ∧ ↑m ∣ ∑ i ∈ t, a i
n : ℕ
hn : 2 ≤ n
ihn : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * n - 1 ≤ #s → ∃ t ⊆ s, #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * (m * n) - 1 ≤ #s
this :
  ∀ k ≤ 2 * m - 1, ∃ 𝒜, #𝒜 = k ∧ (↑𝒜).Pairwise Disjoint ∧ ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = 2 * m - 1
h𝒜disj : (↑𝒜).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ℬ : Finset (Finset ι)
hℬ𝒜 : ℬ ⊆ 𝒜
hℬcard : #ℬ = m
hℬ : ↑m ∣ ∑ i ∈ ℬ, (∑ i ∈ i, a i) / ↑n
⊢ #(ℬ.biUnion fun x => x) = m * n

case intro.intro.intro.intro.intro.intro.refine_2
m : ℕ
hm : 2 ≤ m
ihm : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * m - 1 ≤ #s → ∃ t ⊆ s, #t = m ∧ ↑m ∣ ∑ i ∈ t, a i
n : ℕ
hn : 2 ≤ n
ihn : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * n - 1 ≤ #s → ∃ t ⊆ s, #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * (m * n) - 1 ≤ #s
this :
  ∀ k ≤ 2 * m - 1, ∃ 𝒜, #𝒜 = k ∧ (↑𝒜).Pairwise Disjoint ∧ ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = 2 * m - 1
h𝒜disj : (↑𝒜).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ℬ : Finset (Finset ι)
hℬ𝒜 : ℬ ⊆ 𝒜
hℬcard : #ℬ = m
hℬ : ↑m ∣ ∑ i ∈ ℬ, (∑ i ∈ i, a i) / ↑n
⊢ ↑(m * n) ∣ ∑ i ∈ ℬ.biUnion fun x => x, a i

Proof state:
case composite.zero
m : ℕ
hm : 2 ≤ m
ihm : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * m - 1 ≤ #s → ∃ t ⊆ s, #t = m ∧ ↑m ∣ ∑ i ∈ t, a i
n : ℕ
hn : 2 ≤ n
ihn : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * n - 1 ≤ #s → ∃ t ⊆ s, #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * (m * n) - 1 ≤ #s
hk : 0 ≤ 2 * m - 1
⊢ ∃ 𝒜, #𝒜 = 0 ∧ (↑𝒜).Pairwise Disjoint ∧ ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i

Tactic:
exact ⟨∅, by simp⟩

Result:
no goals