awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
Goal:
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : HMul.hMul (α := ℕ) 2 1 - 1 ≤ #s
⊢ ∃ t ⊆ s, #t = 1 ∧ Dvd.dvd (α := ℤ) (↑1 : ℤ) (∑ i ∈ t, a i)

Tactic:
simpa using exists_subset_card_eq hs

Premises used: Finset.exists_subset_card_eq
-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
Goal:
p : ℕ
hp : Nat.Prime p
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * p - 1 ≤ #s
⊢ Fact (Nat.Prime p)

Tactic:
haveI := Fact.mk hp
-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
Goal:
p : ℕ
hp : Nat.Prime p
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * p - 1 ≤ #s
this : Fact (Nat.Prime p)
prime : ∀ (t : Finset ι) (hts : t ⊆ s) (ht : #t = 2 * p - 1), ∃ t ⊆ s, #t = p ∧ Dvd.dvd (α := ℤ) (↑p : ℤ) (∑ i ∈ t, a i)
⊢ ∃ t ⊆ s, #t = p ∧ Dvd.dvd (α := ℤ) (↑p : ℤ) (∑ i ∈ t, a i)

Tactic:
obtain ⟨t, hts, ht⟩ := exists_subset_card_eq hs

Premises used: Finset.exists_subset_card_eq
-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
Goal:
p : ℕ
hp : Nat.Prime p
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * p - 1 ≤ #s
this : Fact (Nat.Prime p)
t : Finset ι
hts : t ⊆ s
ht : #t = 2 * p - 1
prime :
  ∀ (u : Finset ι) (hut : u ⊆ t) (hu : #u = p ∧ Dvd.dvd (α := ℤ) (↑p : ℤ) (∑ i ∈ u, a i)),
    ∃ t ⊆ s, #t = p ∧ Dvd.dvd (α := ℤ) (↑p : ℤ) (∑ i ∈ t, a i)
⊢ ∃ t ⊆ s, #t = p ∧ Dvd.dvd (α := ℤ) (↑p : ℤ) (∑ i ∈ t, a i)

Tactic:
obtain ⟨u, hut, hu⟩ := Int.erdos_ginzburg_ziv_prime a ht

Premises used: _private.0.Int.erdos_ginzburg_ziv_prime
-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
Goal:
p : ℕ
hp : Nat.Prime p
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * p - 1 ≤ #s
this : Fact (Nat.Prime p)
t : Finset ι
hts : t ⊆ s
ht : #t = 2 * p - 1
u : Finset ι
hut : u ⊆ t
hu : #u = p ∧ Dvd.dvd (α := ℤ) (↑p : ℤ) (∑ i ∈ u, a i)
⊢ ∃ t ⊆ s, #t = p ∧ Dvd.dvd (α := ℤ) (↑p : ℤ) (∑ i ∈ t, a i)

Tactic:
⟨u, hut.trans hts, hu⟩

Premises used: HasSubset.Subset.trans, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
Goal:
p : ℕ
hp : Nat.Prime p
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * p - 1 ≤ #s
this : Fact (Nat.Prime p)
t : Finset ι
hts : t ⊆ s
ht : #t = 2 * p - 1
u : Finset ι
hut : u ⊆ t
hu : #u = p ∧ Dvd.dvd (α := ℤ) (↑p : ℤ) (∑ i ∈ u, a i)
⊢ ∃ t ⊆ s, #t = p ∧ Dvd.dvd (α := ℤ) (↑p : ℤ) (∑ i ∈ t, a i)

Tactic:
exact ⟨u, hut.trans hts, hu⟩
-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
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)
obtain :
  ∀ (𝒜 : 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)),
    ∃ t ⊆ s, #t = m * n ∧ Dvd.dvd (α := ℤ) (↑(m * n) : ℤ) (∑ i ∈ t, a i)
⊢ ∃ t ⊆ s, #t = m * n ∧ Dvd.dvd (α := ℤ) (↑(m * n) : ℤ) (∑ i ∈ t, a i)

Tactic:
obtain ⟨𝒜, h𝒜card, h𝒜disj, h𝒜⟩ := this _ le_rfl

Premises used: le_rfl
-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
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)
obtain :
  ∀ (ℬ : Finset (Finset ι)) (hℬ𝒜 : ℬ ⊆ 𝒜) (hℬcard : #ℬ = m)
    (hℬ : Dvd.dvd (α := ℤ) (↑m : ℤ) (∑ i ∈ ℬ, HDiv.hDiv (α := ℤ) (∑ i ∈ i, a i) (↑n : ℤ))),
    ∃ t ⊆ s, #t = m * n ∧ Dvd.dvd (α := ℤ) (↑(m * n) : ℤ) (∑ i ∈ t, a i)
⊢ ∃ t ⊆ s, #t = m * n ∧ Dvd.dvd (α := ℤ) (↑(m * n) : ℤ) (∑ i ∈ t, a i)

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

Premises used: Eq.ge, HDiv.hDiv, Nat.cast, Finset.sum
-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
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 : ℤ))
⊢ ∃ t ⊆ s, #t = m * n ∧ Dvd.dvd (α := ℤ) (↑(m * n) : ℤ) (∑ i ∈ t, a i)

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

Premises used: Iff.mpr, Finset.biUnion, And.left, And.intro, Exists.intro, Finset.biUnion_subset
-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
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_1 : card (α := ι) (ℬ.biUnion fun (x : Finset ι) ↦ x) = m * n
refine_2 : Dvd.dvd (α := ℤ) (↑(m * n) : ℤ) (∑ i ∈ ℬ.biUnion fun (x : Finset ι) ↦ x, a i)
⊢ ∃ t ⊆ s, #t = m * n ∧ Dvd.dvd (α := ℤ) (↑(m * n) : ℤ) (∑ i ∈ t, a i)

Tactic:
refine ⟨ℬ.biUnion fun x ↦ x, biUnion_subset.2 fun t ht ↦ (h𝒜 <| hℬ𝒜 ht).1, ?_, ?_⟩
-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
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_1 : ∑ u ∈ ℬ, #u = m * n
refine_1₁ : #ℬ * n = m * n
refine_1₂ refine_1₃ : m * n = m * n
⊢ card (α := ι) (ℬ.biUnion fun (x : Finset ι) ↦ x) = m * n

Tactic:
rw [card_biUnion (h𝒜disj.mono hℬ𝒜), sum_const_nat fun t ht ↦ (h𝒜 <| hℬ𝒜 ht).2.1, hℬcard]

Premises used: Set.Pairwise.mono, Finset.card_biUnion, Finset.sum_const_nat, And.right, And.left
-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
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)
refine_2₂ : (↑ℬ : Set (Finset ι)).PairwiseDisjoint (α := Finset ι) fun (x : Finset ι) ↦ x
⊢ Dvd.dvd (α := ℤ) (↑(m * n) : ℤ) (∑ i ∈ ℬ.biUnion fun (x : Finset ι) ↦ x, a i)

Tactic:
rwa [sum_biUnion, Int.natCast_mul, mul_comm, ← Int.dvd_div_iff_mul_dvd, Int.sum_div]

Premises used: Int.natCast_mul, Int.dvd_div_iff_mul_dvd, mul_comm, Finset.sum_biUnion, Int.sum_div
-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
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 : ℤ))
⊢ ∀ i ∈ ℬ, Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ i, a i)

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

Premises used: And.right
-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
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 : ℤ))
⊢ ∀ i ∈ ℬ, Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ i, a i)

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

Premises used: And.right
-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
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 : ℤ))
⊢ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ x ∈ ℬ, ∑ i ∈ x, a i)

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

Premises used: Finset.dvd_sum, And.right
-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
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 : ℤ))
⊢ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ x ∈ ℬ, ∑ i ∈ x, a i)

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

Premises used: Finset.dvd_sum, And.right
-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
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 : ℤ))
⊢ (↑ℬ : Set (Finset ι)).PairwiseDisjoint (α := Finset ι) fun (x : Finset ι) ↦ x

Tactic:
h𝒜disj.mono hℬ𝒜

Premises used: Set.PairwiseDisjoint, Set.Pairwise.mono
-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
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 : ℤ))
⊢ (↑ℬ : Set (Finset ι)).PairwiseDisjoint (α := Finset ι) fun (x : Finset ι) ↦ x

Tactic:
exact h𝒜disj.mono hℬ𝒜

Premises used: Set.Pairwise.mono
-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
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
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)
⊢ ∃ t ⊆ s, #t = m * n ∧ Dvd.dvd (α := ℤ) (↑(m * 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ℬ𝒜
-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
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
hk : 0 ≤ 2 * m - 1
⊢ card.{u_1} (α := Finset ι) ∅ = 0 ∧
    (↑∅ : Set (Finset ι)).Pairwise Disjoint ∧
      ∀ ⦃t : Finset ι⦄,
        Membership.mem (γ := Finset (Finset ι)) ∅ t → t ⊆ s ∧ #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, a i)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
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
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:
exact ⟨∅, by simp⟩
-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
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
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)
⊢ ∃ (𝒜 : 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)

Premises used: Nat.le_of_succ_le
-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
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)
h : 2 ≤ 2 * m - k
⊢ 2 * n - 1 ≤ (2 * m - k) * n - 1

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
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 ≤ 2 * m - k

Tactic:
lia
-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
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
rw₄ rw₅ : 2 * (m * n) - 1 - k * n = 2 * (m * n) - 1 - k * n
⊢ (2 * m - 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]

Premises used: mul_assoc, tsub_right_comm, Finset.sum_const_nat, And.right, And.left, tsub_mul