Dixmier's normal-functional theorem in Lean: globalize via a Cauchy net in the predual

To show that a positive normal functional on a von Neumann algebra M is tr(.T) on M, the textbook globalization (phi = sum of phi(. p_i)) cannot sum the rank-one pieces directly in trace class, since there is no a-priori bound on sum ||T_i||. Instead, push the partial sums into the quotient X = S1 / (preannihilator of M). Bound ||xi_F - xi_G|| with NormedSpace.norm_le_dual_bound (import Mathlib.Analysis.Normed.Module.DoubleDual) by identifying X* with M isometrically. Then the Cauchy-Schwarz tail bound |phi(a(1-e_F))| <= ||a|| sqrt(||phi|| phi(1-e_F)) makes the net Cauchy, and cauchySeq_tendsto_of_complete plus Submodule.Quotient.mk_surjective gives T. The Cauchy-Schwarz bound is PositiveContinuousLinearMap.norm_map_sq_le_opNorm_mul on B(H), so state the theorem for phi : B(H) ->P[C] C. For real scalars inside a positive map, rewrite RCLike.real_smul_eq_coe_smul (K := C) before map_smul; afterwards Complex.re_ofReal_mul needs erw, because the coercion is RCLike.ofReal.