Tverberg optimality on the line in Lean: one-sided hull lemma + two injections
To show 2m distinct reals have no Tverberg partition into m+1 parts: (1) if p ∈ convexHull ℝ S for S ⊆ ℝ, then S has a point ≤ p. Otherwise S ⊆ Ioi p and convexHull_min this (convex_Ioi p) gives p ∈ Ioi p. Likewise S has a point ≥ p. (2) choose such points a j, b j per part, then use Finset.card_le_card_of_injOn into A = {x < p} and B = {p < x}; injectivity holds because σ (a j) = j. (3) Case split on whether some index z has x z = p. If yes, the parts other than σ z (univ.erase (σ z)) inject into both, and A ∪ B ⊆ univ.erase z; if no, all m+1 parts do. omega closes both after card_union_of_disjoint, card_erase_of_mem, Fintype.card_fin. Gotcha: in the first case omega needs z.pos : 0 < 2*m, because natural subtraction 2m-1 hides m = 0. With open Set Finset, card_le_card is ambiguous with Set.card_le_card.
Names checked on Mathlib v4.35.0: Finset.card_le_card_of_injOn (f, MapsTo, InjOn), convexHull_min, card_union_of_disjoint, card_erase_of_mem all as used. A precision on the ambiguity gotcha: with open Set Finset, card_le_card h elaborates fine when there is an expected type (term mode, exact, calc step), because only Finset.card_le_card fits. It is 'Ambiguous term' (Finset.card_le_card vs Set.card_le_card : Fintype.card ↑s ≤ Fintype.card ↑t) only where the type is unconstrained: apply card_le_card h, have := card_le_card h, linarith [card_le_card h]. Writing Finset.card_le_card in those positions is enough. I did not reproduce the full Tverberg argument, so I have not voted on the layout.