α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
m n a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = card s
hm : m ≠ 0
⊢ card (filter (fun u => card u = m) (equitabilise h).parts) * m + b * (m + 1) = a * m + b * (m + 1)
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
m n a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = card s
hm : m ≠ 0
⊢ card (filter (fun u => card u = m) (equitabilise h).parts) = a
refine' (mul_eq_mul_right_iff.1 <| (add_left_inj (b * (m + 1))).1 _).resolve_right hm
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
m n a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = card s
hm : m ≠ 0
⊢ card (filter (fun u => card u = m) (equitabilise h).parts) * m + b * (m + 1) =
    Finset.sum (equitabilise h).parts fun i => card i
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
m n a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = card s
hm : m ≠ 0
⊢ card (filter (fun u => card u = m) (equitabilise h).parts) * m + b * (m + 1) = a * m + b * (m + 1)
rw [h, ← (P.equitabilise h).sum_card_parts]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
m n a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = card s
hm : m ≠ 0
hunion :
  (equitabilise h).parts =
    filter (fun u => card u = m) (equitabilise h).parts ∪ filter (fun u => card u = m + 1) (equitabilise h).parts
⊢ card (filter (fun u => card u = m) (equitabilise h).parts) * m + b * (m + 1) =
    Finset.sum (equitabilise h).parts fun i => card i
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
m n a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = card s
hm : m ≠ 0
⊢ card (filter (fun u => card u = m) (equitabilise h).parts) * m + b * (m + 1) =
    Finset.sum (equitabilise h).parts fun i => card i
have hunion :
  (P.equitabilise h).parts =
    ((P.equitabilise h).parts.filter fun u => u.card = m) ∪
      (P.equitabilise h).parts.filter fun u => u.card = m + 1 := by
  rw [← filter_or, filter_true_of_mem]
  exact fun x => card_eq_of_mem_parts_equitabilise
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
m n a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = card s
hm : m ≠ 0
hunion :
  (equitabilise h).parts =
    filter (fun u => card u = m) (equitabilise h).parts ∪ filter (fun u => card u = m + 1) (equitabilise h).parts
⊢ card (filter (fun u => card u = m) (equitabilise h).parts) * m + b * (m + 1) =
    Finset.sum
      (filter (fun u => card u = m) (equitabilise h).parts ∪ filter (fun u => card u = m + 1) (equitabilise h).parts)
      fun i => card i
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
m n a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = card s
hm : m ≠ 0
hunion :
  (equitabilise h).parts =
    filter (fun u => card u = m) (equitabilise h).parts ∪ filter (fun u => card u = m + 1) (equitabilise h).parts
⊢ card (filter (fun u => card u = m) (equitabilise h).parts) * m + b * (m + 1) =
    Finset.sum (equitabilise h).parts fun i => card i
nth_rw 2 [hunion]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
m n a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = card s
hm : m ≠ 0
hunion :
  (equitabilise h).parts =
    filter (fun u => card u = m) (equitabilise h).parts ∪ filter (fun u => card u = m + 1) (equitabilise h).parts
⊢ Disjoint (filter (fun u => card u = m) (equitabilise h).parts)
    (filter (fun u => card u = m + 1) (equitabilise h).parts)
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
m n a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = card s
hm : m ≠ 0
hunion :
  (equitabilise h).parts =
    filter (fun u => card u = m) (equitabilise h).parts ∪ filter (fun u => card u = m + 1) (equitabilise h).parts
⊢ card (filter (fun u => card u = m) (equitabilise h).parts) * m + b * (m + 1) =
    Finset.sum
      (filter (fun u => card u = m) (equitabilise h).parts ∪ filter (fun u => card u = m + 1) (equitabilise h).parts)
      fun i => card i
rw [sum_union, sum_const_nat fun x hx => (mem_filter.1 hx).2,
  sum_const_nat fun x hx => (mem_filter.1 hx).2, P.card_filter_equitabilise_big]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
m n a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = card s
hm : m ≠ 0
hunion :
  (equitabilise h).parts =
    filter (fun u => card u = m) (equitabilise h).parts ∪ filter (fun u => card u = m + 1) (equitabilise h).parts
⊢ Disjoint (fun u => card u = m) fun u => card u = m + 1
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
m n a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = card s
hm : m ≠ 0
hunion :
  (equitabilise h).parts =
    filter (fun u => card u = m) (equitabilise h).parts ∪ filter (fun u => card u = m + 1) (equitabilise h).parts
⊢ Disjoint (filter (fun u => card u = m) (equitabilise h).parts)
    (filter (fun u => card u = m + 1) (equitabilise h).parts)
refine' disjoint_filter_filter' _ _ _
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
m n a b : ℕ
P : Finpartition s
h✝ : a * m + b * (m + 1) = card s
hm : m ≠ 0
hunion :
  (equitabilise h✝).parts =
    filter (fun u => card u = m) (equitabilise h✝).parts ∪ filter (fun u => card u = m + 1) (equitabilise h✝).parts
x : Finset α → Prop
ha : x ≤ fun u => card u = m
hb : x ≤ fun u => card u = m + 1
i : Finset α
h : x i
⊢ ⊥ i
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
m n a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = card s
hm : m ≠ 0
hunion :
  (equitabilise h).parts =
    filter (fun u => card u = m) (equitabilise h).parts ∪ filter (fun u => card u = m + 1) (equitabilise h).parts
⊢ Disjoint (fun u => card u = m) fun u => card u = m + 1
intro x ha hb i h
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
m n a b : ℕ
P : Finpartition s
h✝ : a * m + b * (m + 1) = card s
hm : m ≠ 0
hunion :
  (equitabilise h✝).parts =
    filter (fun u => card u = m) (equitabilise h✝).parts ∪ filter (fun u => card u = m + 1) (equitabilise h✝).parts
x : Finset α → Prop
ha : x ≤ fun u => card u = m
hb : x ≤ fun u => card u = m + 1
i : Finset α
h : x i
⊢ succ m = m
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
m n a b : ℕ
P : Finpartition s
h✝ : a * m + b * (m + 1) = card s
hm : m ≠ 0
hunion :
  (equitabilise h✝).parts =
    filter (fun u => card u = m) (equitabilise h✝).parts ∪ filter (fun u => card u = m + 1) (equitabilise h✝).parts
x : Finset α → Prop
ha : x ≤ fun u => card u = m
hb : x ≤ fun u => card u = m + 1
i : Finset α
h : x i
⊢ ⊥ i
apply succ_ne_self m _
no goals
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
m n a b : ℕ
P : Finpartition s
h✝ : a * m + b * (m + 1) = card s
hm : m ≠ 0
hunion :
  (equitabilise h✝).parts =
    filter (fun u => card u = m) (equitabilise h✝).parts ∪ filter (fun u => card u = m + 1) (equitabilise h✝).parts
x : Finset α → Prop
ha : x ≤ fun u => card u = m
hb : x ≤ fun u => card u = m + 1
i : Finset α
h : x i
⊢ succ m = m
exact (hb i h).symm.trans (ha i h)
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
m n a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = card s
hm : m ≠ 0
⊢ ∀ (x : Finset α), x ∈ (equitabilise h).parts → card x = m ∨ card x = m + 1
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
m n a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = card s
hm : m ≠ 0
⊢ (equitabilise h).parts =
    filter (fun u => card u = m) (equitabilise h).parts ∪ filter (fun u => card u = m + 1) (equitabilise h).parts
rw [← filter_or, filter_true_of_mem]
no goals
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
m n a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = card s
hm : m ≠ 0
⊢ ∀ (x : Finset α), x ∈ (equitabilise h).parts → card x = m ∨ card x = m + 1
exact fun x => card_eq_of_mem_parts_equitabilise