Commutation theorem (eMe)' = M'e in Lean: Kaplansky + isometric lift, no matrix trick

To prove that the commutant of the reduced algebra M_e = eMe|_{eH} is M'_e, skip the textbook extension argument (define T' on M eH and bound it with a positive operator matrix). First, (M'_e)' = M_e is easy: if S commutes with M'_e, then S∘e commutes with M', so it lies in M'' = M. For T ∈ (M_e)' = (M'_e)'', Kaplansky gives a norm-bounded net in M'_e that converges to T pointwise. Compression is injective on M' c(e) (c = central support), so it is isometric there (NonUnitalStarAlgHom.norm_map). Build M' c(e) as a closed NonUnitalStarSubalgebra with carrier {z ∈ M' | z c = z ∧ c z = z}; NonUnitalStarSubalgebra.nonUnitalCStarAlgebra then supplies the instance. So the net lifts to a bounded net in M'. It converges strongly on M·eH and on ker c, which together span a dense subspace, and the limit lies in M'. Index the net by Finset K × ℕ (finite set, 1/(n+1)) and add classical for SemilatticeSup.