Theorem: ZMod.exists_submultiset_eq_zero (LeanCamCombi/ErdosGinzburgZiv.lean)

State before:
n p : ℕ
inst✝ : Fact p.Prime
s✝ : Multiset (ZMod p)
s : Multiset (ZMod n)
hs : 2 * n - 1 ≤ Multiset.card s
⊢ ∃ t ≤ s, Multiset.card t = n ∧ t.sum = 0
Tactic:
induction n using Nat.prime_composite_induction
State after:
case zero
n p : ℕ
inst✝ : Fact p.Prime
s✝ : Multiset (ZMod p)
s : Multiset (ZMod 0)
hs : 2 * 0 - 1 ≤ Multiset.card s
⊢ ∃ t ≤ s, Multiset.card t = 0 ∧ t.sum = 0

case one
n p : ℕ
inst✝ : Fact p.Prime
s✝ : Multiset (ZMod p)
s : Multiset (ZMod 1)
hs : 2 * 1 - 1 ≤ Multiset.card s
⊢ ∃ t ≤ s, Multiset.card t = 1 ∧ t.sum = 0

case prime
n p : ℕ
inst✝ : Fact p.Prime
s✝ : Multiset (ZMod p)
p✝ : ℕ
a✝ : p✝.Prime
s : Multiset (ZMod p✝)
hs : 2 * p✝ - 1 ≤ Multiset.card s
⊢ ∃ t ≤ s, Multiset.card t = p✝ ∧ t.sum = 0

case composite
n p : ℕ
inst✝ : Fact p.Prime
s✝ : Multiset (ZMod p)
a✝⁴ : ℕ
a✝³ : 2 ≤ a✝⁴
a✝² : ∀ {s : Multiset (ZMod a✝⁴)}, 2 * a✝⁴ - 1 ≤ Multiset.card s → ∃ t ≤ s, Multiset.card t = a✝⁴ ∧ t.sum = 0
b✝ : ℕ
a✝¹ : 2 ≤ b✝
a✝ : ∀ {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

State before:
n p : ℕ
inst✝ : Fact p.Prime
s✝ : Multiset (ZMod p)
s : Multiset (ZMod 0)
hs : 2 * 0 - 1 ≤ Multiset.card s
⊢ ∃ t ≤ s, Multiset.card t = 0 ∧ t.sum = 0
Tactic:
case zero => exact ⟨0, s.zero_le, card_zero, sum_zero⟩
State after:
no goals

State before:
n p : ℕ
inst✝ : Fact p.Prime
s✝ : Multiset (ZMod p)
s : Multiset (ZMod 1)
hs : 2 * 1 - 1 ≤ Multiset.card s
⊢ ∃ t ≤ s, Multiset.card t = 1 ∧ t.sum = 0
Tactic:
case one => obtain ⟨t, ht, hn⟩ := exists_le_card_eq hs; exact ⟨t, ht, hn, Subsingleton.elim _ _⟩
State after:
no goals

State before:
n p✝ : ℕ
inst✝ : Fact p✝.Prime
s✝ : Multiset (ZMod p✝)
p : ℕ
hp : p.Prime
s : Multiset (ZMod p)
hs : 2 * p - 1 ≤ Multiset.card s
⊢ ∃ t ≤ s, Multiset.card t = p ∧ t.sum = 0
Tactic:
case prime p hp =>
  haveI := Fact.mk hp
  obtain ⟨t, hts, ht⟩ := exists_le_card_eq hs
  obtain ⟨u, hut, hu⟩ := aux ht
  exact ⟨u, hut.trans hts, hu⟩
State after:
no goals

State before:
n p : ℕ
inst✝ : Fact p.Prime
s✝ : Multiset (ZMod p)
s : Multiset (ZMod 0)
hs : 2 * 0 - 1 ≤ Multiset.card s
⊢ ∃ t ≤ s, Multiset.card t = 0 ∧ t.sum = 0
Tactic:
exact ⟨0, s.zero_le, card_zero, sum_zero⟩
State after:
no goals

State before:
n p : ℕ
inst✝ : Fact p.Prime
s✝ : Multiset (ZMod p)
s : Multiset (ZMod 1)
hs : 2 * 1 - 1 ≤ Multiset.card s
⊢ ∃ t ≤ s, Multiset.card t = 1 ∧ t.sum = 0
Tactic:
obtain ⟨t, ht, hn⟩ := exists_le_card_eq hs
State after:
case intro.intro
n p : ℕ
inst✝ : Fact p.Prime
s✝ : Multiset (ZMod p)
s : Multiset (ZMod 1)
hs : 2 * 1 - 1 ≤ Multiset.card s
t : Multiset (ZMod 1)
ht : t ≤ s
hn : Multiset.card t = 2 * 1 - 1
⊢ ∃ t ≤ s, Multiset.card t = 1 ∧ t.sum = 0

State before:
case intro.intro
n p : ℕ
inst✝ : Fact p.Prime
s✝ : Multiset (ZMod p)
s : Multiset (ZMod 1)
hs : 2 * 1 - 1 ≤ Multiset.card s
t : Multiset (ZMod 1)
ht : t ≤ s
hn : Multiset.card t = 2 * 1 - 1
⊢ ∃ t ≤ s, Multiset.card t = 1 ∧ t.sum = 0
Tactic:
exact ⟨t, ht, hn, Subsingleton.elim _ _⟩
State after:
no goals

State before:
n p✝ : ℕ
inst✝ : Fact p✝.Prime
s✝ : Multiset (ZMod p✝)
p : ℕ
hp : p.Prime
s : Multiset (ZMod p)
hs : 2 * p - 1 ≤ Multiset.card s
⊢ ∃ t ≤ s, Multiset.card t = p ∧ t.sum = 0
Tactic:
haveI := Fact.mk hp
State after:
n p✝ : ℕ
inst✝ : Fact p✝.Prime
s✝ : Multiset (ZMod p✝)
p : ℕ
hp : p.Prime
s : Multiset (ZMod p)
hs : 2 * p - 1 ≤ Multiset.card s
this : Fact p.Prime
⊢ ∃ t ≤ s, Multiset.card t = p ∧ t.sum = 0

State before:
n p✝ : ℕ
inst✝ : Fact p✝.Prime
s✝ : Multiset (ZMod p✝)
p : ℕ
hp : p.Prime
s : Multiset (ZMod p)
hs : 2 * p - 1 ≤ Multiset.card s
this : Fact p.Prime
⊢ ∃ t ≤ s, Multiset.card t = p ∧ t.sum = 0
Tactic:
obtain ⟨t, hts, ht⟩ := exists_le_card_eq hs
State after:
case intro.intro
n p✝ : ℕ
inst✝ : Fact p✝.Prime
s✝ : Multiset (ZMod p✝)
p : ℕ
hp : p.Prime
s : Multiset (ZMod p)
hs : 2 * p - 1 ≤ Multiset.card s
this : Fact p.Prime
t : Multiset (ZMod p)
hts : t ≤ s
ht : Multiset.card t = 2 * p - 1
⊢ ∃ t ≤ s, Multiset.card t = p ∧ t.sum = 0

State before:
case intro.intro
n p✝ : ℕ
inst✝ : Fact p✝.Prime
s✝ : Multiset (ZMod p✝)
p : ℕ
hp : p.Prime
s : Multiset (ZMod p)
hs : 2 * p - 1 ≤ Multiset.card s
this : Fact p.Prime
t : Multiset (ZMod p)
hts : t ≤ s
ht : Multiset.card t = 2 * p - 1
⊢ ∃ t ≤ s, Multiset.card t = p ∧ t.sum = 0
Tactic:
obtain ⟨u, hut, hu⟩ := aux ht
State after:
case intro.intro.intro.intro
n p✝ : ℕ
inst✝ : Fact p✝.Prime
s✝ : Multiset (ZMod p✝)
p : ℕ
hp : p.Prime
s : Multiset (ZMod p)
hs : 2 * p - 1 ≤ Multiset.card s
this : Fact p.Prime
t : Multiset (ZMod p)
hts : t ≤ s
ht : Multiset.card t = 2 * p - 1
u : Multiset (ZMod p)
hut : u ≤ t
hu : Multiset.card u = p ∧ u.sum = 0
⊢ ∃ t ≤ s, Multiset.card t = p ∧ t.sum = 0

State before:
case intro.intro.intro.intro
n p✝ : ℕ
inst✝ : Fact p✝.Prime
s✝ : Multiset (ZMod p✝)
p : ℕ
hp : p.Prime
s : Multiset (ZMod p)
hs : 2 * p - 1 ≤ Multiset.card s
this : Fact p.Prime
t : Multiset (ZMod p)
hts : t ≤ s
ht : Multiset.card t = 2 * p - 1
u : Multiset (ZMod p)
hut : u ≤ t
hu : Multiset.card u = p ∧ u.sum = 0
⊢ ∃ t ≤ s, Multiset.card t = p ∧ t.sum = 0
Tactic:
exact ⟨u, hut.trans hts, hu⟩
State after:
no goals

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

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

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

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)
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

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

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
State after:
no goals

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

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
State after:
no goals

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⟩
State after:
no goals

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
State after:
no goals

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]
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)

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

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

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]
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

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) • 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
Tactic:
sorry
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
⊢ 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

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

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
State after:
no goals