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
⊢ Multiset.card m.sum + (2 * a - 1) ≤ 2 * (a * b) - 1
Tactic:
rw [map_multiset_sum, this, sum_replicate, ← le_tsub_iff_right, tsub_tsub_tsub_cancel_right,
  ← mul_tsub, ← mul_tsub_one]
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) • n ≤ 2 * (a * (b - 1))

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