α : 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
⊢ Disjoint (filter (fun x => card x = m) (equitabilise h).parts)
    (filter (fun x => card x = 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
⊢ card (equitabilise h).parts = a + b
rw [← filter_true_of_mem fun x => card_eq_of_mem_parts_equitabilise, filter_or, card_union_eq,
  P.card_filter_equitabilise_small _ hm, P.card_filter_equitabilise_big]
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
⊢ Disjoint (filter (fun x => card x = m) (equitabilise h).parts)
    (filter (fun x => card x = m + 1) (equitabilise h).parts)
exact disjoint_filter.2 fun x _ h₀ h₁ => Nat.succ_ne_self m <| h₁.symm.trans h₀