-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
Goal:
ι : Type u_1
n : ℕ
s : Finset ι
a : ι → ℤ
hs : 2 * n - 1 ≤ #s
zero :
  ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ) (hs : HMul.hMul (α := ℕ) 2 0 - 1 ≤ #s),
    ∃ t ⊆ s, #t = 0 ∧ Dvd.dvd (α := ℤ) (↑0 : ℤ) (∑ i ∈ t, a i)
one :
  ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ) (hs : HMul.hMul (α := ℕ) 2 1 - 1 ≤ #s),
    ∃ t ⊆ s, #t = 1 ∧ Dvd.dvd (α := ℤ) (↑1 : ℤ) (∑ i ∈ t, a i)
prime :
  ∀ (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)
composite :
  ∀ (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)
⊢ ∃ t ⊆ s, #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, a i)

Tactic:
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
  -- When `n := p` is prime, we use the prime case `Int.erdos_ginzburg_ziv_prime`.
  | 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
      -- 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ℬ𝒜
    -- Now, let's find those `2 * m - 1` sets.
    rintro k hk
    -- We induct on the size `k ≤ 2 * m - 1` of the family we are constructing.
    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𝒜⟩

Premises used: Nat.prime_composite_induction, Finset.exists_subset_card_eq, Finset.mem_insert, forall_eq_or_imp, ne_eq, Set.pairwise_insert_of_symmetric, Finset.cons_eq_insert, and_assoc, Int.succ, symmetric_disjoint, Finset.coe_insert, Finset.mem_coe