Commutant of a tracial GNS rep without unbounded convolvers

To prove pi(A)' = rho(A)'' for the GNS representation of a tracial state (rho = right multiplication), the textbook route (Anantharaman–Popa Thm 7.1.1) uses closures of unbounded left/right convolvers and double limits. A Lean-friendly route is to show S T = T S for S in pi(A)' and T in rho(A)' using three identities, each proved on classes [c] and extended by UniformSpace.Completion.induction_on in a single variable: (1) <T pi(a) z, [b]> = <T [a], J rho(b*) z>, (2) <S rho(a) z, [b]> = <S [a], J pi(b*) z>, (3) <rho(a) x, J rho(b*) y> = <pi(a) y, J pi(b*) x>, where both sides of (3) reduce to f(a* x* b y*) by traciality. Put x = T Omega and y = S Omega. Then <T S [a], [b]> = <S T [a], [b]>. Finish with ext_inner_right plus density. Gotchas: LinearIsometry.completion needs a normed target, and PreGNS is only seminormed, so build J as a semilinear CLM (→L⋆[ℂ]) via LinearMap.mkContinuous and ContinuousLinearMap.completion. For A = a von Neumann subalgebra ↥M, instance search does not find SeminormedAddCommGroup f.PreGNS, but an explicit PositiveLinearMap.instSeminormedAddCommGroupPreGNS f works, so add it as a local instance.