Lean4
/-- The **Erdős–Ginzburg–Ziv theorem** for `ℤ`.
Any sequence of at least `2 * n - 1` elements of `ℤ` contains a subsequence of `n` elements whose
sum is divisible by `n`. -/
theorem erdos_ginzburg_ziv (a : ι → ℤ) (hs : 2 * n - 1 ≤ #s) : ∃ t ⊆ s, #t = n ∧ ↑n ∣ ∑ i ∈ t, a i := by
classical
-- Do induction on the prime factorisation of `n`. Note that we will apply the induction
-- hypothesis with `ι := Finset ι`, so we need to generalise.
induction n using Nat.prime_composite_induction generalizing ι with
-- When `n := 0`, we can set `t := ∅`.
| zero =>
exact
⟨∅, by simp⟩
-- When `n := 1`, we can take `t` to be any subset of `s` of size `2 * n - 1`.
| one => simpa using exists_subset_card_eq hs
| prime p hp =>
haveI := Fact.mk hp
obtain ⟨t, hts, ht⟩ := exists_subset_card_eq hs
obtain ⟨u, hut, hu⟩ := Int.erdos_ginzburg_ziv_prime a ht
exact
⟨u, hut.trans hts, hu⟩
-- When `n := m * n` is composite, we pick (by induction hypothesis on `n`) `2 * m - 1` sets of
-- size `n` and sums divisible by `n`. Then by induction hypothesis (on `m`) we can pick `m` of
-- these sets whose sum is divisible by `m * n`.
| composite m hm ihm n hn ihn =>
-- First, show that it is enough to have those `2 * m - 1` sets.
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
obtain ⟨ℬ, hℬ𝒜, hℬcard, hℬ⟩ := ihm (fun t ↦ (∑ i ∈ t, a i) / n) h𝒜card.ge
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ℬ𝒜
rintro k hk
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; cutsat
_ = (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
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
omega
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𝒜⟩
