English
Let P be an equipartition and u be a part of P. If |u| ≠ m · 4^{|P.parts|} + a, then |u| equals (4^{|P.parts|} − (a+1))·m + (a+1)(m+1).
Русский
Пусть P — равномерное разбиение, и u — часть разбиения. Если |u| не равно m · 4^{|P.parts|} + a, то |u| = (4^{|P.parts|} − (a+1))·m + (a+1)(m+1).
LaTeX
$$$|u| \neq m \cdot 4^{|P.parts|} + a \Rightarrow |u| = (4^{|P.parts|} - (a+1)) \cdot m + (a+1)(m+1)$$$
Lean4
theorem card_aux₂ (hP : P.IsEquipartition) (hu : u ∈ P.parts) (hucard : #u ≠ m * 4 ^ #P.parts + a) :
(4 ^ #P.parts - (a + 1)) * m + (a + 1) * (m + 1) = #u :=
by
have : m * 4 ^ #P.parts ≤ card α / #P.parts :=
by
rw [stepBound, ← Nat.div_div_eq_div_mul]
exact Nat.div_mul_le_self _ _
rw [Nat.add_sub_of_le this] at hucard
rw [(hP.card_parts_eq_average hu).resolve_left hucard, mul_add, mul_one, ← add_assoc, ← add_mul,
Nat.sub_add_cancel a_add_one_le_four_pow_parts_card, ← add_assoc, mul_comm, Nat.add_sub_of_le this, card_univ]
