English
Given an equipartition of a finite set, there exists a bijection of the set with Fin #s that preserves part membership modulo the number of parts: two elements have equal part iff their images have equal residue modulo the number of parts.
Русский
Дано равномерное разбиение конечного множества; существует биекция с Fin #s, сохраняющая принадлежность к части модуля числа частей: два элемента принадлежат к одной части тогда и только тогда, когда их образы имеют одинаковый остаток по модулю числа частей.
LaTeX
$$$\\exists f : s \\simeq Fin \\#s, \\forall a,b : s,\\ P.part a = P.part b \\iff f a \\% \\#P.parts = f b \\% \\#P.parts$$$
Lean4
/-- Given a finset equipartitioned into `k` parts, its elements can be enumerated such that
elements in the same part have congruent indices modulo `k`. -/
theorem exists_partPreservingEquiv (hP : P.IsEquipartition) :
∃ f : s ≃ Fin #s, ∀ a b : s, P.part a = P.part b ↔ f a % #P.parts = f b % #P.parts :=
by
obtain ⟨f, hf⟩ := P.exists_enumeration
obtain ⟨g, hg⟩ := hP.exists_partsEquiv
let z := fun a ↦ #P.parts * (f a).2 + g (f a).1
have gl := fun a ↦ (g (f a).1).2
have less : ∀ a, z a < #s := fun a ↦
by
rcases hP.card_parts_eq_average (f a).1.2 with (c | c)
·
calc
_ < #P.parts * ((f a).2 + 1) := add_lt_add_left (gl a) _
_ ≤ #P.parts * (#s / #P.parts) := (mul_le_mul_left' (c ▸ (f a).2.2) _)
_ ≤ #P.parts * (#s / #P.parts) + #s % #P.parts := Nat.le_add_right ..
_ = _ := Nat.div_add_mod ..
· rw [← Nat.div_add_mod (#s) #P.parts]
exact add_lt_add_of_le_of_lt (mul_le_mul_left' (by cutsat) _) ((hg (f a).1).mp c)
let z' : s → Fin #s := fun a ↦ ⟨z a, less a⟩
have bij : z'.Bijective :=
by
refine (bijective_iff_injective_and_card z').mpr ⟨fun a b e ↦ ?_, by simp⟩
simp_rw [z', z, Fin.mk.injEq, mul_comm #P.parts] at e
haveI : NeZero #P.parts := ⟨((Nat.zero_le _).trans_lt (gl a)).ne'⟩
change (#P.parts).divModEquiv.symm (_, _) = (#P.parts).divModEquiv.symm (_, _) at e
simp only [Equiv.apply_eq_iff_eq, Prod.mk.injEq] at e
apply_fun f
exact Sigma.ext e.2 <| (Fin.heq_ext_iff (by rw [e.2])).mpr e.1
use Equiv.ofBijective _ bij
intro a b
simp_rw [z', z, Equiv.ofBijective_apply, hf a b, Nat.mul_add_mod, Nat.mod_eq_of_lt (gl a), Nat.mod_eq_of_lt (gl b),
Fin.val_eq_val, g.apply_eq_iff_eq]
