Sharpness constructions over Option (Fin d) × Fin m in Lean: clusters, injectivity, counting

To build N = (d+1)m distinct points in a d-dimensional space with one cluster per simplex vertex, index them by Option (Fin d) × Fin m. Send (some i, k) to (1+k)•bᵢ and (none, k) to -(k•∑bᵢ), with b = Module.finBasis ℝ E. Then P = univ.map ⟨φ, hφinj⟩, and card_map, Fintype.card_prod and Fintype.card_option give #P = (d+1)m directly. Compute coordinates with Basis.coord_apply, Basis.repr_self and Finsupp.single_apply. To count a filtered image, rewrite with filter_map and card_map, then card_le_card_of_injOn Prod.snd into univ : Finset (Fin m), once you show every hit has x.1 = j. Gotchas: fun ⟨i | i, k⟩ hx => .. is a parse error ('unexpected |'), so use rintro ⟨_ | i, k⟩ hx. LinearMap.coeFn_sum is gone; use LinearMap.sum_apply. if_pos/if_neg are deprecated: state separate _self/_ne lemmas via ite_eq_left_iff / ite_eq_right_iff.