internlm/Lean-Github huggingface dataset:
Theorem: ZMod.exists_submultiset_eq_zero
Proof state before:
n p : ℕ
inst✝ : Fact p.Prime
s✝ : Multiset (ZMod p)
a : ℕ
ha : 2 ≤ a
iha : ∀ {s : Multiset (ZMod a)}, 2 * a - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = a ∧ t.sum = 0
b : ℕ
hb : 2 ≤ b
ihb : ∀ {s : Multiset (ZMod b)}, 2 * b - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = b ∧ t.sum = 0
s : Multiset (ZMod (a * b))
hs : 2 * (a * b) - 1 ≤ Multiset.card s
⊢ ∃ t ≤ s, Multiset.card t = a * b ∧ t.sum = 0
Tactic:
suffices ∀ n ≤ 2 * b - 1, ∃ m : Multiset (Multiset $ ZMod $ a * b), Multiset.card m = n ∧
  m.Pairwise _root_.Disjoint ∧ ∀ ⦃u : Multiset $ ZMod $ a * b⦄, u ∈ m →
    Multiset.card u = 2 * a + 1 ∧ u.sum ∈ AddSubgroup.zmultiples (a : ZMod $ a * b) by
  obtain ⟨m, hm⟩ := this _ le_rfl
  sorry
Proof state after:
n p : ℕ
inst✝ : Fact p.Prime
s✝ : Multiset (ZMod p)
a : ℕ
ha : 2 ≤ a
iha : ∀ {s : Multiset (ZMod a)}, 2 * a - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = a ∧ t.sum = 0
b : ℕ
hb : 2 ≤ b
ihb : ∀ {s : Multiset (ZMod b)}, 2 * b - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = b ∧ t.sum = 0
s : Multiset (ZMod (a * b))
hs : 2 * (a * b) - 1 ≤ Multiset.card s
⊢ ∀ n ≤ 2 * b - 1,
    ∃ m,
      Multiset.card m = n ∧
        Multiset.Pairwise _root_.Disjoint m ∧
          ∀ ⦃u : Multiset (ZMod (a * b))⦄, u ∈ m → Multiset.card u = 2 * a + 1 ∧ u.sum ∈ AddSubgroup.zmultiples ↑a
Theorem: ZMod.exists_submultiset_eq_zero
Proof state before:
n p : ℕ
inst✝ : Fact p.Prime
s✝ : Multiset (ZMod p)
a : ℕ
ha : 2 ≤ a
iha : ∀ {s : Multiset (ZMod a)}, 2 * a - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = a ∧ t.sum = 0
b : ℕ
hb : 2 ≤ b
ihb : ∀ {s : Multiset (ZMod b)}, 2 * b - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = b ∧ t.sum = 0
s : Multiset (ZMod (a * b))
hs : 2 * (a * b) - 1 ≤ Multiset.card s
⊢ ∀ n ≤ 2 * b - 1,
    ∃ m,
      Multiset.card m = n ∧
        Multiset.Pairwise _root_.Disjoint m ∧
          ∀ ⦃u : Multiset (ZMod (a * b))⦄, u ∈ m → Multiset.card u = 2 * a + 1 ∧ u.sum ∈ AddSubgroup.zmultiples ↑a
Tactic:
rintro n hn
Proof state after:
n✝ p : ℕ
inst✝ : Fact p.Prime
s✝ : Multiset (ZMod p)
a : ℕ
ha : 2 ≤ a
iha : ∀ {s : Multiset (ZMod a)}, 2 * a - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = a ∧ t.sum = 0
b : ℕ
hb : 2 ≤ b
ihb : ∀ {s : Multiset (ZMod b)}, 2 * b - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = b ∧ t.sum = 0
s : Multiset (ZMod (a * b))
hs : 2 * (a * b) - 1 ≤ Multiset.card s
n : ℕ
hn : n ≤ 2 * b - 1
⊢ ∃ m,
    Multiset.card m = n ∧
      Multiset.Pairwise _root_.Disjoint m ∧
        ∀ ⦃u : Multiset (ZMod (a * b))⦄, u ∈ m → Multiset.card u = 2 * a + 1 ∧ u.sum ∈ AddSubgroup.zmultiples ↑a
Theorem: ZMod.exists_submultiset_eq_zero
Proof state before:
n✝ p : ℕ
inst✝ : Fact p.Prime
s✝ : Multiset (ZMod p)
a : ℕ
ha : 2 ≤ a
iha : ∀ {s : Multiset (ZMod a)}, 2 * a - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = a ∧ t.sum = 0
b : ℕ
hb : 2 ≤ b
ihb : ∀ {s : Multiset (ZMod b)}, 2 * b - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = b ∧ t.sum = 0
s : Multiset (ZMod (a * b))
hs : 2 * (a * b) - 1 ≤ Multiset.card s
n : ℕ
hn : n ≤ 2 * b - 1
⊢ ∃ m,
    Multiset.card m = n ∧
      Multiset.Pairwise _root_.Disjoint m ∧
        ∀ ⦃u : Multiset (ZMod (a * b))⦄, u ∈ m → Multiset.card u = 2 * a + 1 ∧ u.sum ∈ AddSubgroup.zmultiples ↑a
Tactic:
induction' n with n ih
Proof state after:
case zero
n p : ℕ
inst✝ : Fact p.Prime
s✝ : Multiset (ZMod p)
a : ℕ
ha : 2 ≤ a
iha : ∀ {s : Multiset (ZMod a)}, 2 * a - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = a ∧ t.sum = 0
b : ℕ
hb : 2 ≤ b
ihb : ∀ {s : Multiset (ZMod b)}, 2 * b - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = b ∧ t.sum = 0
s : Multiset (ZMod (a * b))
hs : 2 * (a * b) - 1 ≤ Multiset.card s
hn : 0 ≤ 2 * b - 1
⊢ ∃ m,
    Multiset.card m = 0 ∧
      Multiset.Pairwise _root_.Disjoint m ∧
        ∀ ⦃u : Multiset (ZMod (a * b))⦄, u ∈ m → Multiset.card u = 2 * a + 1 ∧ u.sum ∈ AddSubgroup.zmultiples ↑a

case succ
n✝ p : ℕ
inst✝ : Fact p.Prime
s✝ : Multiset (ZMod p)
a : ℕ
ha : 2 ≤ a
iha : ∀ {s : Multiset (ZMod a)}, 2 * a - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = a ∧ t.sum = 0
b : ℕ
hb : 2 ≤ b
ihb : ∀ {s : Multiset (ZMod b)}, 2 * b - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = b ∧ t.sum = 0
s : Multiset (ZMod (a * b))
hs : 2 * (a * b) - 1 ≤ Multiset.card s
n : ℕ
ih :
  n ≤ 2 * b - 1 →
    ∃ m,
      Multiset.card m = n ∧
        Multiset.Pairwise _root_.Disjoint m ∧
          ∀ ⦃u : Multiset (ZMod (a * b))⦄, u ∈ m → Multiset.card u = 2 * a + 1 ∧ u.sum ∈ AddSubgroup.zmultiples ↑a
hn : n + 1 ≤ 2 * b - 1
⊢ ∃ m,
    Multiset.card m = n + 1 ∧
      Multiset.Pairwise _root_.Disjoint m ∧
        ∀ ⦃u : Multiset (ZMod (a * b))⦄, u ∈ m → Multiset.card u = 2 * a + 1 ∧ u.sum ∈ AddSubgroup.zmultiples ↑a
Theorem: ZMod.exists_submultiset_eq_zero
Proof state before:
case succ
n✝ p : ℕ
inst✝ : Fact p.Prime
s✝ : Multiset (ZMod p)
a : ℕ
ha : 2 ≤ a
iha : ∀ {s : Multiset (ZMod a)}, 2 * a - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = a ∧ t.sum = 0
b : ℕ
hb : 2 ≤ b
ihb : ∀ {s : Multiset (ZMod b)}, 2 * b - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = b ∧ t.sum = 0
s : Multiset (ZMod (a * b))
hs : 2 * (a * b) - 1 ≤ Multiset.card s
n : ℕ
ih :
  n ≤ 2 * b - 1 →
    ∃ m,
      Multiset.card m = n ∧
        Multiset.Pairwise _root_.Disjoint m ∧
          ∀ ⦃u : Multiset (ZMod (a * b))⦄, u ∈ m → Multiset.card u = 2 * a + 1 ∧ u.sum ∈ AddSubgroup.zmultiples ↑a
hn : n + 1 ≤ 2 * b - 1
⊢ ∃ m,
    Multiset.card m = n + 1 ∧
      Multiset.Pairwise _root_.Disjoint m ∧
        ∀ ⦃u : Multiset (ZMod (a * b))⦄, u ∈ m → Multiset.card u = 2 * a + 1 ∧ u.sum ∈ AddSubgroup.zmultiples ↑a
Tactic:
obtain ⟨m, hm⟩ := ih (Nat.le_of_succ_le hn)
Proof state after:
case succ.intro
n✝ p : ℕ
inst✝ : Fact p.Prime
s✝ : Multiset (ZMod p)
a : ℕ
ha : 2 ≤ a
iha : ∀ {s : Multiset (ZMod a)}, 2 * a - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = a ∧ t.sum = 0
b : ℕ
hb : 2 ≤ b
ihb : ∀ {s : Multiset (ZMod b)}, 2 * b - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = b ∧ t.sum = 0
s : Multiset (ZMod (a * b))
hs : 2 * (a * b) - 1 ≤ Multiset.card s
n : ℕ
ih :
  n ≤ 2 * b - 1 →
    ∃ m,
      Multiset.card m = n ∧
        Multiset.Pairwise _root_.Disjoint m ∧
          ∀ ⦃u : Multiset (ZMod (a * b))⦄, u ∈ m → Multiset.card u = 2 * a + 1 ∧ u.sum ∈ AddSubgroup.zmultiples ↑a
hn : n + 1 ≤ 2 * b - 1
m : Multiset (Multiset (ZMod (a * b)))
hm :
  Multiset.card m = n ∧
    Multiset.Pairwise _root_.Disjoint m ∧
      ∀ ⦃u : Multiset (ZMod (a * b))⦄, u ∈ m → Multiset.card u = 2 * a + 1 ∧ u.sum ∈ AddSubgroup.zmultiples ↑a
⊢ ∃ m,
    Multiset.card m = n + 1 ∧
      Multiset.Pairwise _root_.Disjoint m ∧
        ∀ ⦃u : Multiset (ZMod (a * b))⦄, u ∈ m → Multiset.card u = 2 * a + 1 ∧ u.sum ∈ AddSubgroup.zmultiples ↑a
Theorem: ZMod.exists_submultiset_eq_zero
Proof state before:
case succ.intro
n✝ p : ℕ
inst✝ : Fact p.Prime
s✝ : Multiset (ZMod p)
a : ℕ
ha : 2 ≤ a
iha : ∀ {s : Multiset (ZMod a)}, 2 * a - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = a ∧ t.sum = 0
b : ℕ
hb : 2 ≤ b
ihb : ∀ {s : Multiset (ZMod b)}, 2 * b - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = b ∧ t.sum = 0
s : Multiset (ZMod (a * b))
hs : 2 * (a * b) - 1 ≤ Multiset.card s
n : ℕ
ih :
  n ≤ 2 * b - 1 →
    ∃ m,
      Multiset.card m = n ∧
        Multiset.Pairwise _root_.Disjoint m ∧
          ∀ ⦃u : Multiset (ZMod (a * b))⦄, u ∈ m → Multiset.card u = 2 * a + 1 ∧ u.sum ∈ AddSubgroup.zmultiples ↑a
hn : n + 1 ≤ 2 * b - 1
m : Multiset (Multiset (ZMod (a * b)))
hm :
  Multiset.card m = n ∧
    Multiset.Pairwise _root_.Disjoint m ∧
      ∀ ⦃u : Multiset (ZMod (a * b))⦄, u ∈ m → Multiset.card u = 2 * a + 1 ∧ u.sum ∈ AddSubgroup.zmultiples ↑a
⊢ ∃ m,
    Multiset.card m = n + 1 ∧
      Multiset.Pairwise _root_.Disjoint m ∧
        ∀ ⦃u : Multiset (ZMod (a * b))⦄, u ∈ m → Multiset.card u = 2 * a + 1 ∧ u.sum ∈ AddSubgroup.zmultiples ↑a
Tactic:
have : 2 * a - 1 ≤ Multiset.card ((s - m.sum).map $ castHom (dvd_mul_right _ _) $ ZMod a) := by
  rw [card_map]
  refine (le_tsub_of_add_le_left $ le_trans ?_ hs).trans le_card_sub
  have : m.map Multiset.card = replicate (2 * a - 1) n := sorry
  rw [map_multiset_sum, this, sum_replicate, ← le_tsub_iff_right, tsub_tsub_tsub_cancel_right,
    ← mul_tsub, ← mul_tsub_one]
  sorry
  sorry
  sorry
Proof state after:
case succ.intro
n✝ p : ℕ
inst✝ : Fact p.Prime
s✝ : Multiset (ZMod p)
a : ℕ
ha : 2 ≤ a
iha : ∀ {s : Multiset (ZMod a)}, 2 * a - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = a ∧ t.sum = 0
b : ℕ
hb : 2 ≤ b
ihb : ∀ {s : Multiset (ZMod b)}, 2 * b - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = b ∧ t.sum = 0
s : Multiset (ZMod (a * b))
hs : 2 * (a * b) - 1 ≤ Multiset.card s
n : ℕ
ih :
  n ≤ 2 * b - 1 →
    ∃ m,
      Multiset.card m = n ∧
        Multiset.Pairwise _root_.Disjoint m ∧
          ∀ ⦃u : Multiset (ZMod (a * b))⦄, u ∈ m → Multiset.card u = 2 * a + 1 ∧ u.sum ∈ AddSubgroup.zmultiples ↑a
hn : n + 1 ≤ 2 * b - 1
m : Multiset (Multiset (ZMod (a * b)))
hm :
  Multiset.card m = n ∧
    Multiset.Pairwise _root_.Disjoint m ∧
      ∀ ⦃u : Multiset (ZMod (a * b))⦄, u ∈ m → Multiset.card u = 2 * a + 1 ∧ u.sum ∈ AddSubgroup.zmultiples ↑a
this : 2 * a - 1 ≤ Multiset.card (Multiset.map (⇑(castHom ⋯ (ZMod a))) (s - m.sum))
⊢ ∃ m,
    Multiset.card m = n + 1 ∧
      Multiset.Pairwise _root_.Disjoint m ∧
        ∀ ⦃u : Multiset (ZMod (a * b))⦄, u ∈ m → Multiset.card u = 2 * a + 1 ∧ u.sum ∈ AddSubgroup.zmultiples ↑a
Theorem: ZMod.exists_submultiset_eq_zero
Proof state before:
case succ.intro
n✝ p : ℕ
inst✝ : Fact p.Prime
s✝ : Multiset (ZMod p)
a : ℕ
ha : 2 ≤ a
iha : ∀ {s : Multiset (ZMod a)}, 2 * a - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = a ∧ t.sum = 0
b : ℕ
hb : 2 ≤ b
ihb : ∀ {s : Multiset (ZMod b)}, 2 * b - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = b ∧ t.sum = 0
s : Multiset (ZMod (a * b))
hs : 2 * (a * b) - 1 ≤ Multiset.card s
n : ℕ
ih :
  n ≤ 2 * b - 1 →
    ∃ m,
      Multiset.card m = n ∧
        Multiset.Pairwise _root_.Disjoint m ∧
          ∀ ⦃u : Multiset (ZMod (a * b))⦄, u ∈ m → Multiset.card u = 2 * a + 1 ∧ u.sum ∈ AddSubgroup.zmultiples ↑a
hn : n + 1 ≤ 2 * b - 1
m : Multiset (Multiset (ZMod (a * b)))
hm :
  Multiset.card m = n ∧
    Multiset.Pairwise _root_.Disjoint m ∧
      ∀ ⦃u : Multiset (ZMod (a * b))⦄, u ∈ m → Multiset.card u = 2 * a + 1 ∧ u.sum ∈ AddSubgroup.zmultiples ↑a
this : 2 * a - 1 ≤ Multiset.card (Multiset.map (⇑(castHom ⋯ (ZMod a))) (s - m.sum))
⊢ ∃ m,
    Multiset.card m = n + 1 ∧
      Multiset.Pairwise _root_.Disjoint m ∧
        ∀ ⦃u : Multiset (ZMod (a * b))⦄, u ∈ m → Multiset.card u = 2 * a + 1 ∧ u.sum ∈ AddSubgroup.zmultiples ↑a
Tactic:
sorry
Proof state after:
no goals
Theorem: ZMod.exists_submultiset_eq_zero
Proof state before:
n p : ℕ
inst✝ : Fact p.Prime
s✝ : Multiset (ZMod p)
a : ℕ
ha : 2 ≤ a
iha : ∀ {s : Multiset (ZMod a)}, 2 * a - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = a ∧ t.sum = 0
b : ℕ
hb : 2 ≤ b
ihb : ∀ {s : Multiset (ZMod b)}, 2 * b - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = b ∧ t.sum = 0
s : Multiset (ZMod (a * b))
hs : 2 * (a * b) - 1 ≤ Multiset.card s
this :
  ∀ n ≤ 2 * b - 1,
    ∃ m,
      Multiset.card m = n ∧
        Multiset.Pairwise _root_.Disjoint m ∧
          ∀ ⦃u : Multiset (ZMod (a * b))⦄, u ∈ m → Multiset.card u = 2 * a + 1 ∧ u.sum ∈ AddSubgroup.zmultiples ↑a
⊢ ∃ t ≤ s, Multiset.card t = a * b ∧ t.sum = 0
Tactic:
obtain ⟨m, hm⟩ := this _ le_rfl
Proof state after:
case intro
n p : ℕ
inst✝ : Fact p.Prime
s✝ : Multiset (ZMod p)
a : ℕ
ha : 2 ≤ a
iha : ∀ {s : Multiset (ZMod a)}, 2 * a - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = a ∧ t.sum = 0
b : ℕ
hb : 2 ≤ b
ihb : ∀ {s : Multiset (ZMod b)}, 2 * b - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = b ∧ t.sum = 0
s : Multiset (ZMod (a * b))
hs : 2 * (a * b) - 1 ≤ Multiset.card s
this :
  ∀ n ≤ 2 * b - 1,
    ∃ m,
      Multiset.card m = n ∧
        Multiset.Pairwise _root_.Disjoint m ∧
          ∀ ⦃u : Multiset (ZMod (a * b))⦄, u ∈ m → Multiset.card u = 2 * a + 1 ∧ u.sum ∈ AddSubgroup.zmultiples ↑a
m : Multiset (Multiset (ZMod (a * b)))
hm :
  Multiset.card m = 2 * b - 1 ∧
    Multiset.Pairwise _root_.Disjoint m ∧
      ∀ ⦃u : Multiset (ZMod (a * b))⦄, u ∈ m → Multiset.card u = 2 * a + 1 ∧ u.sum ∈ AddSubgroup.zmultiples ↑a
⊢ ∃ t ≤ s, Multiset.card t = a * b ∧ t.sum = 0
Theorem: ZMod.exists_submultiset_eq_zero
Proof state before:
case intro
n p : ℕ
inst✝ : Fact p.Prime
s✝ : Multiset (ZMod p)
a : ℕ
ha : 2 ≤ a
iha : ∀ {s : Multiset (ZMod a)}, 2 * a - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = a ∧ t.sum = 0
b : ℕ
hb : 2 ≤ b
ihb : ∀ {s : Multiset (ZMod b)}, 2 * b - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = b ∧ t.sum = 0
s : Multiset (ZMod (a * b))
hs : 2 * (a * b) - 1 ≤ Multiset.card s
this :
  ∀ n ≤ 2 * b - 1,
    ∃ m,
      Multiset.card m = n ∧
        Multiset.Pairwise _root_.Disjoint m ∧
          ∀ ⦃u : Multiset (ZMod (a * b))⦄, u ∈ m → Multiset.card u = 2 * a + 1 ∧ u.sum ∈ AddSubgroup.zmultiples ↑a
m : Multiset (Multiset (ZMod (a * b)))
hm :
  Multiset.card m = 2 * b - 1 ∧
    Multiset.Pairwise _root_.Disjoint m ∧
      ∀ ⦃u : Multiset (ZMod (a * b))⦄, u ∈ m → Multiset.card u = 2 * a + 1 ∧ u.sum ∈ AddSubgroup.zmultiples ↑a
⊢ ∃ t ≤ s, Multiset.card t = a * b ∧ t.sum = 0
Tactic:
sorry
Proof state after:
no goals
Theorem: ZMod.exists_submultiset_eq_zero
Proof state before:
case zero
n p : ℕ
inst✝ : Fact p.Prime
s✝ : Multiset (ZMod p)
a : ℕ
ha : 2 ≤ a
iha : ∀ {s : Multiset (ZMod a)}, 2 * a - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = a ∧ t.sum = 0
b : ℕ
hb : 2 ≤ b
ihb : ∀ {s : Multiset (ZMod b)}, 2 * b - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = b ∧ t.sum = 0
s : Multiset (ZMod (a * b))
hs : 2 * (a * b) - 1 ≤ Multiset.card s
hn : 0 ≤ 2 * b - 1
⊢ ∃ m,
    Multiset.card m = 0 ∧
      Multiset.Pairwise _root_.Disjoint m ∧
        ∀ ⦃u : Multiset (ZMod (a * b))⦄, u ∈ m → Multiset.card u = 2 * a + 1 ∧ u.sum ∈ AddSubgroup.zmultiples ↑a
Tactic:
exact ⟨0, by simp⟩
Proof state after:
no goals
Theorem: ZMod.exists_submultiset_eq_zero
Proof state before:
n p : ℕ
inst✝ : Fact p.Prime
s✝ : Multiset (ZMod p)
a : ℕ
ha : 2 ≤ a
iha : ∀ {s : Multiset (ZMod a)}, 2 * a - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = a ∧ t.sum = 0
b : ℕ
hb : 2 ≤ b
ihb : ∀ {s : Multiset (ZMod b)}, 2 * b - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = b ∧ t.sum = 0
s : Multiset (ZMod (a * b))
hs : 2 * (a * b) - 1 ≤ Multiset.card s
hn : 0 ≤ 2 * b - 1
⊢ Multiset.card 0 = 0 ∧
    Multiset.Pairwise _root_.Disjoint 0 ∧
      ∀ ⦃u : Multiset (ZMod (a * b))⦄, u ∈ 0 → Multiset.card u = 2 * a + 1 ∧ u.sum ∈ AddSubgroup.zmultiples ↑a
Tactic:
simp
Proof state after:
no goals
Theorem: ZMod.exists_submultiset_eq_zero
Proof state before:
n✝ p : ℕ
inst✝ : Fact p.Prime
s✝ : Multiset (ZMod p)
a : ℕ
ha : 2 ≤ a
iha : ∀ {s : Multiset (ZMod a)}, 2 * a - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = a ∧ t.sum = 0
b : ℕ
hb : 2 ≤ b
ihb : ∀ {s : Multiset (ZMod b)}, 2 * b - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = b ∧ t.sum = 0
s : Multiset (ZMod (a * b))
hs : 2 * (a * b) - 1 ≤ Multiset.card s
n : ℕ
ih :
  n ≤ 2 * b - 1 →
    ∃ m,
      Multiset.card m = n ∧
        Multiset.Pairwise _root_.Disjoint m ∧
          ∀ ⦃u : Multiset (ZMod (a * b))⦄, u ∈ m → Multiset.card u = 2 * a + 1 ∧ u.sum ∈ AddSubgroup.zmultiples ↑a
hn : n + 1 ≤ 2 * b - 1
m : Multiset (Multiset (ZMod (a * b)))
hm :
  Multiset.card m = n ∧
    Multiset.Pairwise _root_.Disjoint m ∧
      ∀ ⦃u : Multiset (ZMod (a * b))⦄, u ∈ m → Multiset.card u = 2 * a + 1 ∧ u.sum ∈ AddSubgroup.zmultiples ↑a
⊢ 2 * a - 1 ≤ Multiset.card (Multiset.map (⇑(castHom ⋯ (ZMod a))) (s - m.sum))
Tactic:
rw [card_map]
Proof state after:
n✝ p : ℕ
inst✝ : Fact p.Prime
s✝ : Multiset (ZMod p)
a : ℕ
ha : 2 ≤ a
iha : ∀ {s : Multiset (ZMod a)}, 2 * a - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = a ∧ t.sum = 0
b : ℕ
hb : 2 ≤ b
ihb : ∀ {s : Multiset (ZMod b)}, 2 * b - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = b ∧ t.sum = 0
s : Multiset (ZMod (a * b))
hs : 2 * (a * b) - 1 ≤ Multiset.card s
n : ℕ
ih :
  n ≤ 2 * b - 1 →
    ∃ m,
      Multiset.card m = n ∧
        Multiset.Pairwise _root_.Disjoint m ∧
          ∀ ⦃u : Multiset (ZMod (a * b))⦄, u ∈ m → Multiset.card u = 2 * a + 1 ∧ u.sum ∈ AddSubgroup.zmultiples ↑a
hn : n + 1 ≤ 2 * b - 1
m : Multiset (Multiset (ZMod (a * b)))
hm :
  Multiset.card m = n ∧
    Multiset.Pairwise _root_.Disjoint m ∧
      ∀ ⦃u : Multiset (ZMod (a * b))⦄, u ∈ m → Multiset.card u = 2 * a + 1 ∧ u.sum ∈ AddSubgroup.zmultiples ↑a
⊢ 2 * a - 1 ≤ Multiset.card (s - m.sum)
Theorem: ZMod.exists_submultiset_eq_zero
Proof state before:
n✝ p : ℕ
inst✝ : Fact p.Prime
s✝ : Multiset (ZMod p)
a : ℕ
ha : 2 ≤ a
iha : ∀ {s : Multiset (ZMod a)}, 2 * a - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = a ∧ t.sum = 0
b : ℕ
hb : 2 ≤ b
ihb : ∀ {s : Multiset (ZMod b)}, 2 * b - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = b ∧ t.sum = 0
s : Multiset (ZMod (a * b))
hs : 2 * (a * b) - 1 ≤ Multiset.card s
n : ℕ
ih :
  n ≤ 2 * b - 1 →
    ∃ m,
      Multiset.card m = n ∧
        Multiset.Pairwise _root_.Disjoint m ∧
          ∀ ⦃u : Multiset (ZMod (a * b))⦄, u ∈ m → Multiset.card u = 2 * a + 1 ∧ u.sum ∈ AddSubgroup.zmultiples ↑a
hn : n + 1 ≤ 2 * b - 1
m : Multiset (Multiset (ZMod (a * b)))
hm :
  Multiset.card m = n ∧
    Multiset.Pairwise _root_.Disjoint m ∧
      ∀ ⦃u : Multiset (ZMod (a * b))⦄, u ∈ m → Multiset.card u = 2 * a + 1 ∧ u.sum ∈ AddSubgroup.zmultiples ↑a
⊢ 2 * a - 1 ≤ Multiset.card (s - m.sum)
Tactic:
refine (le_tsub_of_add_le_left $ le_trans ?_ hs).trans le_card_sub
Proof state after:
n✝ p : ℕ
inst✝ : Fact p.Prime
s✝ : Multiset (ZMod p)
a : ℕ
ha : 2 ≤ a
iha : ∀ {s : Multiset (ZMod a)}, 2 * a - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = a ∧ t.sum = 0
b : ℕ
hb : 2 ≤ b
ihb : ∀ {s : Multiset (ZMod b)}, 2 * b - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = b ∧ t.sum = 0
s : Multiset (ZMod (a * b))
hs : 2 * (a * b) - 1 ≤ Multiset.card s
n : ℕ
ih :
  n ≤ 2 * b - 1 →
    ∃ m,
      Multiset.card m = n ∧
        Multiset.Pairwise _root_.Disjoint m ∧
          ∀ ⦃u : Multiset (ZMod (a * b))⦄, u ∈ m → Multiset.card u = 2 * a + 1 ∧ u.sum ∈ AddSubgroup.zmultiples ↑a
hn : n + 1 ≤ 2 * b - 1
m : Multiset (Multiset (ZMod (a * b)))
hm :
  Multiset.card m = n ∧
    Multiset.Pairwise _root_.Disjoint m ∧
      ∀ ⦃u : Multiset (ZMod (a * b))⦄, u ∈ m → Multiset.card u = 2 * a + 1 ∧ u.sum ∈ AddSubgroup.zmultiples ↑a
⊢ Multiset.card m.sum + (2 * a - 1) ≤ 2 * (a * b) - 1
Theorem: ZMod.exists_submultiset_eq_zero
Proof state before:
n✝ p : ℕ
inst✝ : Fact p.Prime
s✝ : Multiset (ZMod p)
a : ℕ
ha : 2 ≤ a
iha : ∀ {s : Multiset (ZMod a)}, 2 * a - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = a ∧ t.sum = 0
b : ℕ
hb : 2 ≤ b
ihb : ∀ {s : Multiset (ZMod b)}, 2 * b - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = b ∧ t.sum = 0
s : Multiset (ZMod (a * b))
hs : 2 * (a * b) - 1 ≤ Multiset.card s
n : ℕ
ih :
  n ≤ 2 * b - 1 →
    ∃ m,
      Multiset.card m = n ∧
        Multiset.Pairwise _root_.Disjoint m ∧
          ∀ ⦃u : Multiset (ZMod (a * b))⦄, u ∈ m → Multiset.card u = 2 * a + 1 ∧ u.sum ∈ AddSubgroup.zmultiples ↑a
hn : n + 1 ≤ 2 * b - 1
m : Multiset (Multiset (ZMod (a * b)))
hm :
  Multiset.card m = n ∧
    Multiset.Pairwise _root_.Disjoint m ∧
      ∀ ⦃u : Multiset (ZMod (a * b))⦄, u ∈ m → Multiset.card u = 2 * a + 1 ∧ u.sum ∈ AddSubgroup.zmultiples ↑a
⊢ Multiset.card m.sum + (2 * a - 1) ≤ 2 * (a * b) - 1
Tactic:
have : m.map Multiset.card = replicate (2 * a - 1) n := sorry
Proof state after:
n✝ p : ℕ
inst✝ : Fact p.Prime
s✝ : Multiset (ZMod p)
a : ℕ
ha : 2 ≤ a
iha : ∀ {s : Multiset (ZMod a)}, 2 * a - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = a ∧ t.sum = 0
b : ℕ
hb : 2 ≤ b
ihb : ∀ {s : Multiset (ZMod b)}, 2 * b - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = b ∧ t.sum = 0
s : Multiset (ZMod (a * b))
hs : 2 * (a * b) - 1 ≤ Multiset.card s
n : ℕ
ih :
  n ≤ 2 * b - 1 →
    ∃ m,
      Multiset.card m = n ∧
        Multiset.Pairwise _root_.Disjoint m ∧
          ∀ ⦃u : Multiset (ZMod (a * b))⦄, u ∈ m → Multiset.card u = 2 * a + 1 ∧ u.sum ∈ AddSubgroup.zmultiples ↑a
hn : n + 1 ≤ 2 * b - 1
m : Multiset (Multiset (ZMod (a * b)))
hm :
  Multiset.card m = n ∧
    Multiset.Pairwise _root_.Disjoint m ∧
      ∀ ⦃u : Multiset (ZMod (a * b))⦄, u ∈ m → Multiset.card u = 2 * a + 1 ∧ u.sum ∈ AddSubgroup.zmultiples ↑a
this : Multiset.map (⇑Multiset.card) m = replicate (2 * a - 1) n
⊢ Multiset.card m.sum + (2 * a - 1) ≤ 2 * (a * b) - 1
Theorem: ZMod.exists_submultiset_eq_zero
Proof state before:
n✝ p : ℕ
inst✝ : Fact p.Prime
s✝ : Multiset (ZMod p)
a : ℕ
ha : 2 ≤ a
iha : ∀ {s : Multiset (ZMod a)}, 2 * a - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = a ∧ t.sum = 0
b : ℕ
hb : 2 ≤ b
ihb : ∀ {s : Multiset (ZMod b)}, 2 * b - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = b ∧ t.sum = 0
s : Multiset (ZMod (a * b))
hs : 2 * (a * b) - 1 ≤ Multiset.card s
n : ℕ
ih :
  n ≤ 2 * b - 1 →
    ∃ m,
      Multiset.card m = n ∧
        Multiset.Pairwise _root_.Disjoint m ∧
          ∀ ⦃u : Multiset (ZMod (a * b))⦄, u ∈ m → Multiset.card u = 2 * a + 1 ∧ u.sum ∈ AddSubgroup.zmultiples ↑a
hn : n + 1 ≤ 2 * b - 1
m : Multiset (Multiset (ZMod (a * b)))
hm :
  Multiset.card m = n ∧
    Multiset.Pairwise _root_.Disjoint m ∧
      ∀ ⦃u : Multiset (ZMod (a * b))⦄, u ∈ m → Multiset.card u = 2 * a + 1 ∧ u.sum ∈ AddSubgroup.zmultiples ↑a
this : Multiset.map (⇑Multiset.card) m = replicate (2 * a - 1) n
⊢ 1 ≤ 2 * a

n✝ p : ℕ
inst✝ : Fact p.Prime
s✝ : Multiset (ZMod p)
a : ℕ
ha : 2 ≤ a
iha : ∀ {s : Multiset (ZMod a)}, 2 * a - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = a ∧ t.sum = 0
b : ℕ
hb : 2 ≤ b
ihb : ∀ {s : Multiset (ZMod b)}, 2 * b - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = b ∧ t.sum = 0
s : Multiset (ZMod (a * b))
hs : 2 * (a * b) - 1 ≤ Multiset.card s
n : ℕ
ih :
  n ≤ 2 * b - 1 →
    ∃ m,
      Multiset.card m = n ∧
        Multiset.Pairwise _root_.Disjoint m ∧
          ∀ ⦃u : Multiset (ZMod (a * b))⦄, u ∈ m → Multiset.card u = 2 * a + 1 ∧ u.sum ∈ AddSubgroup.zmultiples ↑a
hn : n + 1 ≤ 2 * b - 1
m : Multiset (Multiset (ZMod (a * b)))
hm :
  Multiset.card m = n ∧
    Multiset.Pairwise _root_.Disjoint m ∧
      ∀ ⦃u : Multiset (ZMod (a * b))⦄, u ∈ m → Multiset.card u = 2 * a + 1 ∧ u.sum ∈ AddSubgroup.zmultiples ↑a
this : Multiset.map (⇑Multiset.card) m = replicate (2 * a - 1) n
⊢ 2 * a - 1 ≤ 2 * (a * b) - 1
Tactic:
sorry
Proof state after:
n✝ p : ℕ
inst✝ : Fact p.Prime
s✝ : Multiset (ZMod p)
a : ℕ
ha : 2 ≤ a
iha : ∀ {s : Multiset (ZMod a)}, 2 * a - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = a ∧ t.sum = 0
b : ℕ
hb : 2 ≤ b
ihb : ∀ {s : Multiset (ZMod b)}, 2 * b - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = b ∧ t.sum = 0
s : Multiset (ZMod (a * b))
hs : 2 * (a * b) - 1 ≤ Multiset.card s
n : ℕ
ih :
  n ≤ 2 * b - 1 →
    ∃ m,
      Multiset.card m = n ∧
        Multiset.Pairwise _root_.Disjoint m ∧
          ∀ ⦃u : Multiset (ZMod (a * b))⦄, u ∈ m → Multiset.card u = 2 * a + 1 ∧ u.sum ∈ AddSubgroup.zmultiples ↑a
hn : n + 1 ≤ 2 * b - 1
m : Multiset (Multiset (ZMod (a * b)))
hm :
  Multiset.card m = n ∧
    Multiset.Pairwise _root_.Disjoint m ∧
      ∀ ⦃u : Multiset (ZMod (a * b))⦄, u ∈ m → Multiset.card u = 2 * a + 1 ∧ u.sum ∈ AddSubgroup.zmultiples ↑a
this : Multiset.map (⇑Multiset.card) m = replicate (2 * a - 1) n
⊢ 2 * a - 1 ≤ 2 * (a * b) - 1
Theorem: ZMod.exists_submultiset_eq_zero
Proof state before:
n✝ p : ℕ
inst✝ : Fact p.Prime
s✝ : Multiset (ZMod p)
a : ℕ
ha : 2 ≤ a
iha : ∀ {s : Multiset (ZMod a)}, 2 * a - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = a ∧ t.sum = 0
b : ℕ
hb : 2 ≤ b
ihb : ∀ {s : Multiset (ZMod b)}, 2 * b - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = b ∧ t.sum = 0
s : Multiset (ZMod (a * b))
hs : 2 * (a * b) - 1 ≤ Multiset.card s
n : ℕ
ih :
  n ≤ 2 * b - 1 →
    ∃ m,
      Multiset.card m = n ∧
        Multiset.Pairwise _root_.Disjoint m ∧
          ∀ ⦃u : Multiset (ZMod (a * b))⦄, u ∈ m → Multiset.card u = 2 * a + 1 ∧ u.sum ∈ AddSubgroup.zmultiples ↑a
hn : n + 1 ≤ 2 * b - 1
m : Multiset (Multiset (ZMod (a * b)))
hm :
  Multiset.card m = n ∧
    Multiset.Pairwise _root_.Disjoint m ∧
      ∀ ⦃u : Multiset (ZMod (a * b))⦄, u ∈ m → Multiset.card u = 2 * a + 1 ∧ u.sum ∈ AddSubgroup.zmultiples ↑a
this : Multiset.map (⇑Multiset.card) m = replicate (2 * a - 1) n
⊢ 2 * a - 1 ≤ 2 * (a * b) - 1
Tactic:
sorry
Proof state after:
no goals