Lean/Mathlib v4.35: EuclideanSpace coordinates, chromatic number bounds in ℕ∞, and a regular simplex

Notes from proving d+1 ≤ χ(ℝᵈ) ≤ (⌈√d⌉+1)ᵈ for the unit distance graph. (1) Lower bounds: SimpleGraph.le_chromaticNumber_of_pairwise_adj (hn : n ≤ Nat.card ι) f hf takes a pairwise-adjacent family directly, no clique Finset needed. (2) Regular unit simplex in any inner product space: v_i = (1/√2)•b_i from stdOrthonormalBasis, last vertex t•∑ b_i with t = (√2+√(2+2d))/(2d). Do all distances via inner products (inner_sub_left/right, orthonormal_iff_ite, sum_inner). For the quadratic, derive 2*d*t - r = s by field_simp, then linear_combination (1/4)*((2*d*t - r + s)*h3 + hs - hr). Index the d+1 points with Fin.lastCases w v and do the case analysis with induction i using Fin.lastCases. (3) Coordinates: EuclideanSpace.dist_eq x y : dist x y = √(∑ i, dist (x i) (y i) ^ 2); a single coordinate is bounded by Real.le_sqrt_of_sq_le + Finset.single_le_sum. (4) ℕ∞ trap: after simpa, a hypothesis can read 1 + 1 ≤ χ under instLEENat while the goal is 2 ≤ χ under the lattice LE, and simpa cannot close it. Use rw [finrank_euclideanSpace_fin] at this; convert this using 1; rfl. (5) Colouring by Fin d → ZMod m with Coloring.colorable, then rw [Fintype.card_fun, ZMod.card, Fintype.card_fin].