-- Mathlib/Combinatorics/SimpleGraph/Regularity/Equitabilise.lean
theorem card_filter_equitabilise_small (hm : m ≠ 0) :
    #{u ∈ (P.equitabilise h).parts | #u = m} = a

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = #s
hm : m ≠ 0
⊢ (equitabilise h).parts =
    filter (fun u => #u = m) (equitabilise h).parts ∪ filter (fun u => #u = m + 1) (equitabilise h).parts

Tactic:
rw [← filter_or, filter_true_of_mem]

Result:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = #s
hm : m ≠ 0
⊢ ∀ x ∈ (equitabilise h).parts, #x = m ∨ #x = m + 1

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = #s
hm : m ≠ 0
hunion :
  (equitabilise h).parts =
    filter (fun u => #u = m) (equitabilise h).parts ∪ filter (fun u => #u = m + 1) (equitabilise h).parts
⊢ #(filter (fun u => #u = m) (equitabilise h).parts) * m + b * (m + 1) =
    ∑ i ∈ filter (fun u => #u = m) (equitabilise h).parts ∪ filter (fun u => #u = m + 1) (equitabilise h).parts, #i

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

Result:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = #s
hm : m ≠ 0
hunion :
  (equitabilise h).parts =
    filter (fun u => #u = m) (equitabilise h).parts ∪ filter (fun u => #u = m + 1) (equitabilise h).parts
⊢ Disjoint (filter (fun u => #u = m) (equitabilise h).parts) (filter (fun u => #u = m + 1) (equitabilise h).parts)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h✝ : a * m + b * (m + 1) = #s
hm : m ≠ 0
hunion :
  (equitabilise h✝).parts =
    filter (fun u => #u = m) (equitabilise h✝).parts ∪ filter (fun u => #u = m + 1) (equitabilise h✝).parts
x : Finset α → Prop
ha : x ≤ fun u => #u = m
hb : x ≤ fun u => #u = m + 1
i : Finset α
h : x i
⊢ m.succ = m

Tactic:
exact (hb i h).symm.trans (ha i h)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = #s
hm : m ≠ 0
hunion :
  (equitabilise h).parts =
    filter (fun u => #u = m) (equitabilise h).parts ∪ filter (fun u => #u = m + 1) (equitabilise h).parts
⊢ #(filter (fun u => #u = m) (equitabilise h).parts) * m + b * (m + 1) = ∑ i ∈ (equitabilise h).parts, #i

Tactic:
nth_rw 2 [hunion]

Result:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = #s
hm : m ≠ 0
hunion :
  (equitabilise h).parts =
    filter (fun u => #u = m) (equitabilise h).parts ∪ filter (fun u => #u = m + 1) (equitabilise h).parts
⊢ #(filter (fun u => #u = m) (equitabilise h).parts) * m + b * (m + 1) =
    ∑ i ∈ filter (fun u => #u = m) (equitabilise h).parts ∪ filter (fun u => #u = m + 1) (equitabilise h).parts, #i

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = #s
hm : m ≠ 0
⊢ #(filter (fun u => #u = m) (equitabilise h).parts) = a

Tactic:
refine (mul_eq_mul_right_iff.1 <| (add_left_inj (b * (m + 1))).1 ?_).resolve_right hm

Result:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = #s
hm : m ≠ 0
⊢ #(filter (fun u => #u = m) (equitabilise h).parts) * m + b * (m + 1) = a * m + b * (m + 1)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = #s
hm : m ≠ 0
⊢ ∀ x ∈ (equitabilise h).parts, #x = m ∨ #x = m + 1

Tactic:
exact fun x => card_eq_of_mem_parts_equitabilise

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = #s
hm : m ≠ 0
hunion :
  (equitabilise h).parts =
    filter (fun u => #u = m) (equitabilise h).parts ∪ filter (fun u => #u = m + 1) (equitabilise h).parts
⊢ Disjoint (fun u => #u = m) fun u => #u = m + 1

Tactic:
intro x ha hb i h

Result:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h✝ : a * m + b * (m + 1) = #s
hm : m ≠ 0
hunion :
  (equitabilise h✝).parts =
    filter (fun u => #u = m) (equitabilise h✝).parts ∪ filter (fun u => #u = m + 1) (equitabilise h✝).parts
x : Finset α → Prop
ha : x ≤ fun u => #u = m
hb : x ≤ fun u => #u = m + 1
i : Finset α
h : x i
⊢ ⊥ i

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = #s
hm : m ≠ 0
hunion :
  (equitabilise h).parts =
    filter (fun u => #u = m) (equitabilise h).parts ∪ filter (fun u => #u = m + 1) (equitabilise h).parts
⊢ Disjoint (filter (fun u => #u = m) (equitabilise h).parts) (filter (fun u => #u = m + 1) (equitabilise h).parts)

Tactic:
refine disjoint_filter_filter' _ _ ?_

Result:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = #s
hm : m ≠ 0
hunion :
  (equitabilise h).parts =
    filter (fun u => #u = m) (equitabilise h).parts ∪ filter (fun u => #u = m + 1) (equitabilise h).parts
⊢ Disjoint (fun u => #u = m) fun u => #u = m + 1

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = #s
hm : m ≠ 0
⊢ #(filter (fun u => #u = m) (equitabilise h).parts) * m + b * (m + 1) = ∑ i ∈ (equitabilise h).parts, #i

Tactic:
have hunion :
  (P.equitabilise h).parts =
    {u ∈ (P.equitabilise h).parts | #u = m} ∪ {u ∈ (P.equitabilise h).parts | #u = m + 1} := by
  rw [← filter_or, filter_true_of_mem]
  exact fun x => card_eq_of_mem_parts_equitabilise

Result:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = #s
hm : m ≠ 0
hunion :
  (equitabilise h).parts =
    filter (fun u => #u = m) (equitabilise h).parts ∪ filter (fun u => #u = m + 1) (equitabilise h).parts
⊢ #(filter (fun u => #u = m) (equitabilise h).parts) * m + b * (m + 1) = ∑ i ∈ (equitabilise h).parts, #i

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = #s
hm : m ≠ 0
⊢ #(filter (fun u => #u = m) (equitabilise h).parts) * m + b * (m + 1) = a * m + b * (m + 1)

Tactic:
rw [h, ← (P.equitabilise h).sum_card_parts]

Result:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = #s
hm : m ≠ 0
⊢ #(filter (fun u => #u = m) (equitabilise h).parts) * m + b * (m + 1) = ∑ i ∈ (equitabilise h).parts, #i

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h✝ : a * m + b * (m + 1) = #s
hm : m ≠ 0
hunion :
  (equitabilise h✝).parts =
    filter (fun u => #u = m) (equitabilise h✝).parts ∪ filter (fun u => #u = m + 1) (equitabilise h✝).parts
x : Finset α → Prop
ha : x ≤ fun u => #u = m
hb : x ≤ fun u => #u = m + 1
i : Finset α
h : x i
⊢ ⊥ i

Tactic:
apply succ_ne_self m _

Result:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h✝ : a * m + b * (m + 1) = #s
hm : m ≠ 0
hunion :
  (equitabilise h✝).parts =
    filter (fun u => #u = m) (equitabilise h✝).parts ∪ filter (fun u => #u = m + 1) (equitabilise h✝).parts
x : Finset α → Prop
ha : x ≤ fun u => #u = m
hb : x ≤ fun u => #u = m + 1
i : Finset α
h : x i
⊢ m.succ = m