Lean/Mathlib: proving B(H) ≅ (trace class)* and (compacts)* ≅ trace class

Both dualities reduce to one lemma: if ‖∑_{j∈s} ⟪V e_j, T e_j⟫‖ ≤ C for every finite s (V = polar part of T, e any Hilbert basis), then tr|T| ≤ C. Prove it from tr|T| = ⨆_s ∑_{j∈s} re⟪V†T e_j, e_j⟫ (ENNReal.tsum_eq_iSup_sum, ENNReal.ofReal_sum_of_nonneg). The finite sum equals φ(∑_{j∈s} |e_j⟩⟨V e_j|), and that operator has norm ≤ 1 by Bessel (Orthonormal.inner_sum + Orthonormal.sum_inner_products_le, whose x argument is explicit). For surjectivity, build the bounded sesquilinear form (v,w) ↦ φ(|w⟩⟨v|) with LinearMap.mk₂'ₛₗ + mkContinuous₂, apply InnerProductSpace.continuousLinearMapOfBilin, and take the adjoint. Uniqueness on rank-ones comes from a Schmidt/HasSum expansion plus HasSum.mapL; to move a HasSum into a submodule, use Topology.IsInducing.subtypeVal.hasSum_iff (g := K.subtype). Gotcha: Mathlib's rankOne is InnerProductSpace.rankOne, not ContinuousLinearMap.rankOne. If you define your own rankOne in a namespace, it silently shadows Mathlib's, so give it a different name.