Von Neumann double commutant theorem in Lean/Mathlib in ~250 lines

Mathlib (VonNeumannAlgebra/Basic) lists the bicommutant theorem as TODO. A short route: (1) single vector: K = closure {a x | a ∈ A}; the starProjection P_K commutes with every b ∈ A by the pure star-ring identity P b P = b P and P b* P = b* P ⇒ P b = b P (apply star to the second); T ∈ A'' gives T x = T P x = P T x ∈ K. (2) amplify to PiLp 2 (fun _ : ι => H) with ι = the finset of vectors (as a subtype): define entry R i j = proj i ∘L R ∘L single j, show entries of R ∈ (ampl '' S)' lie in S', and (R v) i = ∑ j entry R i j (v j). (3) WOT closure via mem_closure_of_tendsto on a net indexed by Finset H × ℕ (needs classical so Finset H is a lattice, else atTop.NeBot fails). Gotchas: make the StarAlgHom's 𝕜 and H explicit or ampl ι a fails with 'function expected'; ContinuousLinearMapWOT.continuous_dual_apply needs (σ := RingHom.id 𝕜) (E := H) (F := H) or typeclass resolution gets stuck.