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)
this_1 : 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)
this : t₀ ∉ 𝒜
rw : #𝒜 + 1 = k + 1
rw₁ rw₂ : k + 1 = k + 1
⊢ #(cons t₀ 𝒜 this) = k + 1

Tactic:
rw [card_cons, h𝒜card]

Premises used: Finset.card_cons
-- 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_1 : 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)
this : t₀ ∉ 𝒜
composite : (↑(cons t₀ 𝒜 this) : Set (Finset ι)).Pairwise Disjoint
composite₁ : ∀ ⦃t : Finset ι⦄, t ∈ cons t₀ 𝒜 this → 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:
refine ⟨𝒜.cons t₀ this, by rw [card_cons, h𝒜card], ?_, ?_⟩
-- 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_1 : 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)
this : t₀ ∉ 𝒜
composite : (↑𝒜 : Set (Finset ι)).Pairwise Disjoint ∧ ∀ b ∈ 𝒜, ¬t₀ = b → Disjoint t₀ b
⊢ (↑(cons t₀ 𝒜 this) : Set (Finset ι)).Pairwise Disjoint

Tactic:
simp only [cons_eq_insert, coe_insert, Set.pairwise_insert_of_symmetric symmetric_disjoint,
        mem_coe, ne_eq]

Premises used: ne_eq, Set.pairwise_insert_of_symmetric, Finset.cons_eq_insert, symmetric_disjoint, Finset.coe_insert, Finset.mem_coe
-- 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_1 : 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)
this : t₀ ∉ 𝒜
⊢ (↑𝒜 : Set (Finset ι)).Pairwise Disjoint ∧ ∀ b ∈ 𝒜, ¬t₀ = b → Disjoint t₀ b

Tactic:
⟨h𝒜disj, fun t ht _ ↦ sdiff_disjoint.mono ht₀ <| subset_biUnion_of_mem id ht⟩

Premises used: id, Finset.subset_biUnion_of_mem, And.intro, 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_1 : 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)
this : t₀ ∉ 𝒜
⊢ (↑𝒜 : Set (Finset ι)).Pairwise Disjoint ∧ ∀ b ∈ 𝒜, ¬t₀ = b → Disjoint t₀ b

Tactic:
exact ⟨h𝒜disj, fun t ht _ ↦ sdiff_disjoint.mono ht₀ <| subset_biUnion_of_mem id ht⟩
-- 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_1 : 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)
this : t₀ ∉ 𝒜
composite :
  t₀ ⊆ s ∧
    #t₀ = n ∧
      Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t₀, a i) ∧
        ∀ a_1 ∈ 𝒜, a_1 ⊆ s ∧ #a_1 = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ a_1, a i)
⊢ ∀ ⦃t : Finset ι⦄, t ∈ cons t₀ 𝒜 this → t ⊆ s ∧ #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, a i)

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

Premises used: Finset.mem_insert, forall_eq_or_imp, Finset.cons_eq_insert, and_assoc
-- 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_1 : 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)
this : t₀ ∉ 𝒜
⊢ t₀ ⊆ s ∧
    #t₀ = n ∧
      Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t₀, a i) ∧
        ∀ a_1 ∈ 𝒜, a_1 ⊆ s ∧ #a_1 = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ a_1, a i)

Tactic:
⟨ht₀.trans sdiff_subset, ht₀card, ht₀sum, h𝒜⟩

Premises used: HasSubset.Subset.trans, And.intro, Finset.sdiff_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
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_1 : 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)
this : t₀ ∉ 𝒜
⊢ t₀ ⊆ s ∧
    #t₀ = n ∧
      Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t₀, a i) ∧
        ∀ a_1 ∈ 𝒜, a_1 ⊆ s ∧ #a_1 = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ a_1, a i)

Tactic:
exact ⟨ht₀.trans sdiff_subset, ht₀card, ht₀sum, 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
k : ℕ
hk : k ≤ 2 * m - 1
composite :
  ∀ (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)
composite₁ :
  ∀ (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 ι)),
      #𝒜 = k + 1 ∧
        (↑𝒜 : Set (Finset ι)).Pairwise Disjoint ∧
          ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, a i)
⊢ ∃ (𝒜 : Finset (Finset ι)),
    #𝒜 = k ∧
      (↑𝒜 : Set (Finset ι)).Pairwise Disjoint ∧
        ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, a i)

Tactic:
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: 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
-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
Goal:
ι : Type u_1
n : ℕ
s : Finset ι
a : ι → ZMod n
hs : 2 * n - 1 ≤ #s
⊢ ∃ t ⊆ s, #t = n ∧ Eq (α := ZMod n) (∑ i ∈ t, a i) 0

Tactic:
simpa [← ZMod.intCast_zmod_eq_zero_iff_dvd] using Int.erdos_ginzburg_ziv (ZMod.cast ∘ a) hs

Premises used: ZMod.cast, Int.erdos_ginzburg_ziv, Function.comp, ZMod.intCast_zmod_eq_zero_iff_dvd
-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
Goal:
n : ℕ
s : Multiset ℤ
hs : 2 * n - 1 ≤ s.card
⊢ 2 * n - 1 ≤ #s.toEnumFinset

Tactic:
simpa using hs
-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
Goal:
n : ℕ
s : Multiset ℤ
hs : 2 * n - 1 ≤ s.card
obtain :
  ∀ (t : Finset (ℤ × ℕ)) (hts : t ⊆ s.toEnumFinset) (ht : #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, i.1)),
    ∃ t ≤ s, t.card = n ∧ (↑n : ℤ) ∣ t.sum
⊢ ∃ t ≤ s, t.card = n ∧ (↑n : ℤ) ∣ t.sum

Tactic:
obtain ⟨t, hts, ht⟩ := Int.erdos_ginzburg_ziv (s := s.toEnumFinset) Prod.fst (by simpa using hs)

Premises used: Int.erdos_ginzburg_ziv, Prod.fst
-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
Goal:
n : ℕ
s : Multiset ℤ
hs : 2 * n - 1 ≤ s.card
t : Finset (ℤ × ℕ)
hts : t ⊆ s.toEnumFinset
ht : #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, i.1)
⊢ (Multiset.map Prod.fst t.val).card = n ∧ (↑n : ℤ) ∣ (Multiset.map Prod.fst t.val).sum

Tactic:
simpa using ht
-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
Goal:
n : ℕ
s : Multiset ℤ
hs : 2 * n - 1 ≤ s.card
t : Finset (ℤ × ℕ)
hts : t ⊆ s.toEnumFinset
ht : #t = n ∧ Dvd.dvd (α := ℤ) (↑n : ℤ) (∑ i ∈ t, i.1)
⊢ ∃ t ≤ s, t.card = n ∧ (↑n : ℤ) ∣ t.sum

Tactic:
exact ⟨t.1.map Prod.fst, Multiset.map_fst_le_of_subset_toEnumFinset hts, by simpa using ht⟩
-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
Goal:
n : ℕ
s : Multiset (ZMod n)
hs : 2 * n - 1 ≤ s.card
⊢ 2 * n - 1 ≤ #s.toEnumFinset

Tactic:
simpa using hs
-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
Goal:
n : ℕ
s : Multiset (ZMod n)
hs : 2 * n - 1 ≤ s.card
obtain :
  ∀ (t : Finset (ZMod n × ℕ)) (hts : t ⊆ s.toEnumFinset) (ht : #t = n ∧ Eq (α := ZMod n) (∑ i ∈ t, i.1) 0),
    ∃ t ≤ s, t.card = n ∧ t.sum = 0
⊢ ∃ t ≤ s, t.card = n ∧ t.sum = 0

Tactic:
obtain ⟨t, hts, ht⟩ := ZMod.erdos_ginzburg_ziv (s := s.toEnumFinset) Prod.fst (by simpa using hs)

Premises used: Prod.fst, ZMod.erdos_ginzburg_ziv
-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
Goal:
n : ℕ
s : Multiset (ZMod n)
hs : 2 * n - 1 ≤ s.card
t : Finset (ZMod n × ℕ)
hts : t ⊆ s.toEnumFinset
ht : #t = n ∧ Eq (α := ZMod n) (∑ i ∈ t, i.1) 0
⊢ (Multiset.map Prod.fst t.val).card = n ∧ (Multiset.map Prod.fst t.val).sum = 0

Tactic:
simpa using ht
-- Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
Goal:
n : ℕ
s : Multiset (ZMod n)
hs : 2 * n - 1 ≤ s.card
t : Finset (ZMod n × ℕ)
hts : t ⊆ s.toEnumFinset
ht : #t = n ∧ Eq (α := ZMod n) (∑ i ∈ t, i.1) 0
⊢ ∃ t ≤ s, t.card = n ∧ t.sum = 0

Tactic:
exact ⟨t.1.map Prod.fst, Multiset.map_fst_le_of_subset_toEnumFinset hts, by simpa using ht⟩
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : CommMonoid β
A : Set α
B : Set β
f₁ f₂ : α → β
n : ℕ
hf₁ : IsMulFreimanHom n A B f₁
h : EqOn f₁ f₂ A
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
h' : s.prod = t.prod
rw : (map f₁ s).prod = (map f₂ t).prod
rw₁ : (map f₁ s).prod = (map f₁ t).prod
rw₂ rw₃ : (map f₁ t).prod = (map f₁ t).prod
⊢ (map f₂ s).prod = (map f₂ t).prod

Tactic:
rw [map_congr rfl fun x hx => (h (hsA hx)).symm, map_congr rfl fun x hx => (h (htA hx)).symm,
      hf₁.map_prod_eq_map_prod hsA htA hs ht h']

Premises used: IsMulFreimanHom.map_prod_eq_map_prod, Multiset.map_congr, Eq.symm, rfl
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : CommMonoid β
A : Set α
B : Set β
f₁ f₂ : α → β
n : ℕ
hf₁ : IsMulFreimanIso n A B f₁
h : EqOn f₁ f₂ A
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
rw : Multiset.prod (map (fun (x : α) ↦ f₁ x) s) = (map f₂ t).prod ↔ s.prod = t.prod
rw₁ :
  Eq.{u_3 + 1} (α := β) (Multiset.prod (map (fun (x : α) ↦ f₁ x) s)) (Multiset.prod (map (fun (x : α) ↦ f₁ x) t)) ↔
    s.prod = t.prod
rw₂ rw₃ : s.prod = t.prod ↔ s.prod = t.prod
⊢ (map f₂ s).prod = (map f₂ t).prod ↔ s.prod = t.prod

Tactic:
rw [map_congr rfl fun x hx => h.symm (hsA hx), map_congr rfl fun x hx => h.symm (htA hx),
      hf₁.map_prod_eq_map_prod hsA htA hs ht]

Premises used: IsMulFreimanIso.map_prod_eq_map_prod, Multiset.map_congr, Set.EqOn.symm, rfl
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
g : β → α
hg₁ : MapsTo g B A
hg₂ : RightInvOn g f B
hf : IsMulFreimanIso n A B f
s t : Multiset β
hsB : ∀ ⦃x : β⦄, x ∈ s → x ∈ B
htB : ∀ ⦃x : β⦄, x ∈ t → x ∈ B
hs : s.card = n
ht : t.card = n
⊢ (map g s).card = n

Tactic:
simp [hs]
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
g : β → α
hg₁ : MapsTo g B A
hg₂ : RightInvOn g f B
hf : IsMulFreimanIso n A B f
s t : Multiset β
hsB : ∀ ⦃x : β⦄, x ∈ s → x ∈ B
htB : ∀ ⦃x : β⦄, x ∈ t → x ∈ B
hs : s.card = n
ht : t.card = n
⊢ (map g t).card = n

Tactic:
simp [ht]
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
g : β → α
hg₁ : MapsTo g B A
hg₂ : RightInvOn g f B
hf : IsMulFreimanIso n A B f
s t : Multiset β
hsB : ∀ ⦃x : β⦄, x ∈ s → x ∈ B
htB : ∀ ⦃x : β⦄, x ∈ t → x ∈ B
hs : s.card = n
ht : t.card = n
rw : ∀ x ∈ t, (f ∘ g) x = id x
rw₁ : ∀ x ∈ s, (f ∘ g) x = id x
rw₂ : ∀ ⦃x : α⦄, x ∈ map g s → x ∈ A
rw₃ : ∀ ⦃x : α⦄, x ∈ map g t → x ∈ A
⊢ (map g s).prod = (map g t).prod ↔ s.prod = t.prod

Tactic:
rw [← hf.map_prod_eq_map_prod _ _ (by simp [hs]) (by simp [ht]), map_map, map_congr rfl, map_id,
      map_map, map_congr rfl, map_id]

Premises used: Multiset.map_id, IsMulFreimanIso.map_prod_eq_map_prod, Multiset.map_congr, Multiset.map_map, rfl
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
g : β → α
hg₁ : MapsTo g B A
hg₂ : RightInvOn g f B
hf : IsMulFreimanIso n A B f
s t : Multiset β
hsB : ∀ ⦃x : β⦄, x ∈ s → x ∈ B
htB : ∀ ⦃x : β⦄, x ∈ t → x ∈ B
hs : s.card = n
ht : t.card = n
⊢ ∀ x ∈ t, (f ∘ g) x = id x

Tactic:
aesop
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
g : β → α
hg₁ : MapsTo g B A
hg₂ : RightInvOn g f B
hf : IsMulFreimanIso n A B f
s t : Multiset β
hsB : ∀ ⦃x : β⦄, x ∈ s → x ∈ B
htB : ∀ ⦃x : β⦄, x ∈ t → x ∈ B
hs : s.card = n
ht : t.card = n
⊢ ∀ x ∈ s, (f ∘ g) x = id x

Tactic:
aesop
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
g : β → α
hg₁ : MapsTo g B A
hg₂ : RightInvOn g f B
hf : IsMulFreimanIso n A B f
s t : Multiset β
hsB : ∀ ⦃x : β⦄, x ∈ s → x ∈ B
htB : ∀ ⦃x : β⦄, x ∈ t → x ∈ B
hs : s.card = n
ht : t.card = n
⊢ ∀ ⦃x : α⦄, x ∈ map g s → x ∈ A

Tactic:
aesop
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
g : β → α
hg₁ : MapsTo g B A
hg₂ : RightInvOn g f B
hf : IsMulFreimanIso n A B f
s t : Multiset β
hsB : ∀ ⦃x : β⦄, x ∈ s → x ∈ B
htB : ∀ ⦃x : β⦄, x ∈ t → x ∈ B
hs : s.card = n
ht : t.card = n
⊢ ∀ ⦃x : α⦄, x ∈ map g t → x ∈ A

Tactic:
aesop
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
g : β → α
h : InvOn g f A B
hf : IsMulFreimanHom n A B f
hg : IsMulFreimanHom n B A g
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
⊢ (map f s).prod = (map f t).prod ↔ s.prod = t.prod

Tactic:
⟨fun h' => ?_, hf.map_prod_eq_map_prod hsA htA hs ht⟩

Premises used: IsMulFreimanHom.map_prod_eq_map_prod, Iff.intro
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
g : β → α
h : InvOn g f A B
hf : IsMulFreimanHom n A B f
hg : IsMulFreimanHom n B A g
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
refine : ∀ (h' : (map f s).prod = (map f t).prod), s.prod = t.prod
⊢ (map f s).prod = (map f t).prod ↔ s.prod = t.prod

Tactic:
refine ⟨fun h' => ?_, hf.map_prod_eq_map_prod hsA htA hs ht⟩
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
g : β → α
h : InvOn g f A B
hf : IsMulFreimanHom n A B f
hg : IsMulFreimanHom n B A g
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
h' : (map f s).prod = (map f t).prod
⊢ MapsTo f A B

Tactic:
have := hf.mapsTo
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
g : β → α
h : InvOn g f A B
hf : IsMulFreimanHom n A B f
hg : IsMulFreimanHom n B A g
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
h' : (map f s).prod = (map f t).prod
this : MapsTo f A B
hsA₁ : ∀ ⦃x : β⦄, x ∈ map f s → x ∈ B
htA₁ : ∀ ⦃x : β⦄, x ∈ map f t → x ∈ B
hs₁ : (map f s).card = n
ht₁ : (map f t).card = n
h₁ : (map f s).prod = (map f t).prod
⊢ (map g (map f s)).prod = (map g (map f t)).prod

Tactic:
apply hg.map_prod_eq_map_prod

Premises used: IsMulFreimanHom.map_prod_eq_map_prod
-- Module: Mathlib.Combinatorics.Additive.FreimanHom
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoid α
inst_1 : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
g : β → α
h : InvOn g f A B
hf : IsMulFreimanHom n A B f
hg : IsMulFreimanHom n B A g
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
h' : (map f s).prod = (map f t).prod
this : MapsTo f A B
⊢ ∀ ⦃x : β⦄, x ∈ map f s → x ∈ B

Tactic:
simp_all [MapsTo]

Premises used: Set.MapsTo