English
If m ≠ 0, then the number of parts of size m is a.
Русский
Если m не равно нулю, то число частей размера m равно a.
LaTeX
$$$\\#\\{ u \\in (P.equitabilise h).parts:\\; |u|=m \\} = a$ при $m\\neq 0$$$
Lean4
theorem card_filter_equitabilise_small (hm : m ≠ 0) : #({u ∈ (P.equitabilise h).parts | #u = m}) = a :=
by
refine (mul_eq_mul_right_iff.1 <| (add_left_inj (b * (m + 1))).1 ?_).resolve_right hm
rw [h, ← (P.equitabilise h).sum_card_parts]
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
nth_rw 2 [hunion]
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]
refine disjoint_filter_filter' _ _ ?_
intro x ha hb i h
apply succ_ne_self m _
exact (hb i h).symm.trans (ha i h)
