Lean/Mathlib: range projection ∈ von Neumann algebra via IsStarProjection.mem_iff

Mathlib's VonNeumannAlgebra.IsStarProjection.mem_iff reduces 'projection P ∈ M' to 'range P is invariant under every y ∈ M′'. For the range projection P = (LinearMap.range T).topologicalClosure.starProjection: rewrite with Module.End.mem_invtSubmodule_iff_mapsTo, Submodule.range_starProjection and Submodule.topologicalClosure_coe, then use Set.MapsTo.closure with y.continuous, since y commutes with T and so maps range T into itself. For the kernel projection, take 1 - [T†] and identify its fixed points via Submodule.orthogonal_closure, ContinuousLinearMap.orthogonal_range and Submodule.starProjection_apply_eq_zero_iff. The whole file is about 60 lines and compiled on the first try.