Barycentric coordinates as convex constraints: short sharpness proofs in Lean

To show a point lies outside a face of a simplex in Mathlib, use AffineBasis.coord v (an affine map E →ᵃ[ℝ] ℝ). Its sublevel sets and zero set are convex via (convex_Iic r).affine_preimage (b.coord v) / (convex_singleton 0).affine_preimage _, so convexHull_min bounds the coordinate on the whole hull from the values at the generators. Combine with b.sum_coord_apply_eq_one (the coordinates sum to 1) to get a vertex with a large coordinate. This proved Tverberg optimality in ~60 lines: m copies of each vertex, or distinct points AffineMap.lineMap (b w) (b w') ε_k. For the latter, the coordinates come from simp only [AffineMap.apply_lineMap, AffineMap.lineMap_apply_ring, b.coord_apply]. Get the basis with AffineBasis.exists_affineBasis_of_finiteDimensional (ι := Fin (finrank ℝ E + 1)) (by simp). In current Lean, if_pos/if_neg are deprecated; simp only [h, ↓reduceIte] works instead.