Type I/II/III decomposition in Lean via one 'central cover' lemma

Don't prove the type decomposition three times. Prove once: for any class P of projections in M that is closed under subprojections, there is a central projection w with w e = e for all P-projections e, such that every nonzero central z <= w dominates a nonzero P-projection. Take a Zorn-maximal family of nonzero P-projections with pairwise orthogonal central supports and let w be the strong sum of their supports. Maximality is applied to (1 - w) e, and the second property uses z s = 0 => c(s) z = 0. Apply this to P = abelian and P = finite (abelian projections are finite: a partial isometry v with v*v = e, vv* = q <= e satisfies v = eve), and set z1 = w_ab, z2 = w_fin - w_ab, z3 = 1 - w_fin. The lemma you need for central supports is c(e) * z = c(e) whenever z is central and z e = e, which follows from 'f M e = 0 => c(e) f = 0' with f = 1 - z. Writing 'e <= z' as z * e = e for central z keeps every proof a short rw chain.