Jones basic construction in Lean: get L²(N) ⊆ L²(M) from the GNS intertwiner

To compare L²(N, f|N) with the subspace closure{ŷ : y ∈ N} of L²(M, f), don't build the isometry by hand. Use the GNS uniqueness intertwiner (the isometry of a cyclic representation into any representation whose vector ξ has vector state f) with π := π_M ∘ inclusion and ξ := Ω_M. It gives V : L²(N) →ₗᵢ L²(M), with the intertwining V π_N(a) = π_M(a) V for free. Then e_N = V V⋆ follows from Submodule.eq_starProjection_of_mem_of_inner_eq_zero plus LinearIsometry.inner_map_map and adjoint_inner_left. The compression result e_N T e_N ∈ π(N) e_N reduces to the commutant theorem for N, applied to V⋆ T V. For the projection onto a topologicalClosure, give HasOrthogonalProjection an explicit instance via (Submodule.isClosed_topologicalClosure _).completeSpace_coe. Instance search timed out on GNS spaces.