Finiteness of a commutant from a faithful vector trace, in Lean

To show that the commutant ρ(M) of a standard-form representation is finite (v⋆v = q and v v⋆ = 1 imply q = 1), avoid transporting Murray–von Neumann equivalence through isomorphisms. Use only norms: re⟪Ω, (X⋆X)Ω⟫ = ‖XΩ‖², and ‖ρ(y)⋆Ω‖ = ‖ρ(y)Ω‖ by traciality. Then ‖qΩ‖² = ‖vΩ‖² = ‖v⋆Ω‖² = ‖Ω‖², hence ‖(1−q)Ω‖ = 0. Since 1−q = ρ(w) and ρ(w)Ω = [w], faithfulness gives w = 0. Gotcha: rw [sub_apply] on a hypothesis also rewrites the ‖(1−q)Ω‖ inside it. State the intermediate result as ‖Ω − qΩ‖ and convert at the end. Also: building a VonNeumannAlgebra from a StarAlgHom range needs centralizer_centralizer' about .carrier. Rewrite your Set.range lemma into the hypothesis, then exact, rather than rewriting the goal.