awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
hcd : #(𝒜.biUnion id) ≤ ∑ t ∈ 𝒜, #t
⊢ 2 * (m * n) - 1 - ∑ t ∈ 𝒜, #t ≤ #s - #(𝒜.biUnion id)

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)
⊢ #(𝒜.biUnion id) ≤ ∑ t ∈ 𝒜, #t

Tactic:
card_biUnion_le

Premises used: Finset.card_biUnion_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)
⊢ #(𝒜.biUnion id) ≤ ∑ t ∈ 𝒜, #t

Tactic:
exact card_biUnion_le

Premises used: Finset.card_biUnion_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)
⊢ #s - #(𝒜.biUnion id) ≤ #(s \ 𝒜.biUnion id)

Tactic:
le_card_sdiff ..

Premises used: Finset.le_card_sdiff
-- 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 * n - 1 ≤ (2 * m - k) * n - 1
_₁ : (2 * m - k) * n - 1 = 2 * (m * n) - 1 - ∑ t ∈ 𝒜, #t
_₂ : 2 * (m * n) - 1 - ∑ t ∈ 𝒜, #t ≤ #s - #(𝒜.biUnion id)
⊢ 2 * n - 1 ≤ #(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 ..

Premises used: HMul.hMul, HSub.hSub, id, Finset.biUnion, SDiff.sdiff, Finset.le_card_sdiff, OfNat.ofNat
-- 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 * 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 ..
-- 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)
this : 2 * n - 1 ≤ #(s \ 𝒜.biUnion id)
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)
⊢ ∃ (𝒜 : 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
-- 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)
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₀ ∈ 𝒜
⊢ n = 0

Tactic:
simpa [← card_eq_zero, ht₀card] using sdiff_disjoint.mono ht₀ <| subset_biUnion_of_mem id h

Premises used: id, Finset.subset_biUnion_of_mem, Finset.card_eq_zero, Disjoint.mono, Finset.sdiff_disjoint
-- 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)
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₀ ∈ 𝒜
⊢ 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

Premises used: 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
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
⊢ ∀ {ι : 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

Premises used: 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
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)
⊢ 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

Premises used: 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
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)
hs₁ : 2 * (m * 0) - 1 ≤ #s
⊢ ∀ (hk : k ≤ 2 * m - 1),
    ∃ (𝒜 : Finset (Finset ι)),
      #𝒜 = k ∧
        (↑𝒜 : Set (Finset ι)).Pairwise Disjoint ∧
          ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → 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

Premises used: 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
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)
hs₁ : 2 * (m * 0) - 1 ≤ #s
ih₁ :
  ∀ (hk : k ≤ 2 * m - 1),
    ∃ (𝒜 : Finset (Finset ι)),
      #𝒜 = k ∧
        (↑𝒜 : Set (Finset ι)).Pairwise Disjoint ∧
          ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = 0 ∧ Dvd.dvd (α := ℤ) (↑0 : ℤ) (∑ i ∈ t, a i)
⊢ ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → 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

Premises used: 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
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)
hs₁ : 2 * (m * 0) - 1 ≤ #s
ih₁ :
  ∀ (hk : k ≤ 2 * m - 1),
    ∃ (𝒜 : Finset (Finset ι)),
      #𝒜 = k ∧
        (↑𝒜 : Set (Finset ι)).Pairwise Disjoint ∧
          ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = 0 ∧ Dvd.dvd (α := ℤ) (↑0 : ℤ) (∑ i ∈ t, a i)
h𝒜₁ : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = 0 ∧ Dvd.dvd (α := ℤ) (↑0 : ℤ) (∑ i ∈ t, a i)
⊢ HMul.hMul (α := ℕ) 2 0 - 1 ≤ #(s \ 𝒜.biUnion id)

Tactic:
obtain rfl : n = 0 := by
        simpa [← card_eq_zero, ht₀card] using sdiff_disjoint.mono ht₀ <| subset_biUnion_of_mem id h

Premises used: 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
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)
hs₁ : 2 * (m * 0) - 1 ≤ #s
ih₁ :
  ∀ (hk : k ≤ 2 * m - 1),
    ∃ (𝒜 : Finset (Finset ι)),
      #𝒜 = k ∧
        (↑𝒜 : Set (Finset ι)).Pairwise Disjoint ∧
          ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = 0 ∧ Dvd.dvd (α := ℤ) (↑0 : ℤ) (∑ i ∈ t, a i)
h𝒜₁ : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = 0 ∧ Dvd.dvd (α := ℤ) (↑0 : ℤ) (∑ i ∈ t, a i)
this₁ : HMul.hMul (α := ℕ) 2 0 - 1 ≤ #(s \ 𝒜.biUnion id)
⊢ #t₀ = 0

Tactic:
obtain rfl : n = 0 := by
        simpa [← card_eq_zero, ht₀card] using sdiff_disjoint.mono ht₀ <| subset_biUnion_of_mem id h

Premises used: 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
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)
hs₁ : 2 * (m * 0) - 1 ≤ #s
ih₁ :
  ∀ (hk : k ≤ 2 * m - 1),
    ∃ (𝒜 : Finset (Finset ι)),
      #𝒜 = k ∧
        (↑𝒜 : Set (Finset ι)).Pairwise Disjoint ∧
          ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = 0 ∧ Dvd.dvd (α := ℤ) (↑0 : ℤ) (∑ i ∈ t, a i)
h𝒜₁ : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = 0 ∧ Dvd.dvd (α := ℤ) (↑0 : ℤ) (∑ i ∈ t, a i)
this₁ : HMul.hMul (α := ℕ) 2 0 - 1 ≤ #(s \ 𝒜.biUnion id)
ht₀card₁ : #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

Premises used: 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)
ι : Type u_1
s : Finset ι
a : ι → ℤ
k : ℕ
hk : k + 1 ≤ 2 * m - 1
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = k
h𝒜disj : (↑𝒜 : Set (Finset ι)).Pairwise Disjoint
t₀ : Finset ι
ht₀ : t₀ ⊆ s \ 𝒜.biUnion id
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)
hs : 2 * (m * 0) - 1 ≤ #s
ih :
  ∀ (hk : k ≤ 2 * m - 1),
    ∃ (𝒜 : Finset (Finset ι)),
      #𝒜 = k ∧
        (↑𝒜 : Set (Finset ι)).Pairwise Disjoint ∧
          ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = 0 ∧ Dvd.dvd (α := ℤ) (↑0 : ℤ) (∑ i ∈ t, a i)
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = 0 ∧ Dvd.dvd (α := ℤ) (↑0 : ℤ) (∑ i ∈ t, a i)
this : HMul.hMul (α := ℕ) 2 0 - 1 ≤ #(s \ 𝒜.biUnion id)
ht₀card : #t₀ = 0
ht₀sum : Dvd.dvd (α := ℤ) (↑0 : ℤ) (∑ i ∈ t₀, a i)
⊢ False

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)
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)
⊢ t₀ ∉ 𝒜

Tactic:
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