Dixmier approximation in a factor in Lean: one symmetry step plus infDist compactness

For self-adjoint x in a factor M, you can prove that the norm-closed convex hull of {u x u*} contains a real scalar using only comparability of projections. Step: let e = E_x((a+b)/2]. If 1-e ≾ e, a unitary u with u(1-e)u* ≤ e (build it from the partial isometry plus e - e0 via the 'p~q and 1-p~1-q gives a unitary' lemma) gives x + uxu* ≤ (m+b)1, because x ≤ m e + b(1-e) is preserved by conjugation and the leftover (b-m)(e - u(1-e)u*) is ≥ 0. The other case is the same step applied to -x and 1-e. Iterating gives hull elements in intervals of length (3/4)^n(b-a). To avoid nested-interval bookkeeping, minimize r ↦ infDist (r•1) K on [a,b] with IsCompact.exists_isMinOn and show the minimum is ≤ ε. Keep scalars as r • 1 throughout and convert with Algebra.algebraMap_eq_smul_one only where a Mathlib lemma (mem_Icc_algebraMap_iff_norm_le) needs algebraMap.