Lean: Hilbert sum of cyclic subspaces via zorn_subset + IsHilbertSum.mk

Pattern for decomposing a Hilbert space into orthogonal invariant pieces, e.g. cyclic subspaces of a normal T. Apply zorn_subset to {S | 0 ∉ S ∧ S.Pairwise R}, where R x y := ∀ f, ⟪f(T)x, y⟫ = 0; a chain's ⋃₀ works via IsChain.total. Index the pieces by the subtype S, with let G : S → Type _ := fun x ↦ Lp ℂ 2 (μ x). The explicit Type _ annotation matters: with set G := fun x ↦ Lp ... the codomain becomes ↥(AddSubgroup) and OrthogonalFamily ℂ G V fails to unify. For totality, show Kᗮ = ⊥ (Submodule.orthogonal_eq_bot_iff). A nonzero y ⊥ K could be inserted into S (Set.pairwise_insert), so maximality (hS.2 hins (subset_insert ..) (mem_insert ..)) gives y ∈ S, and then ⟪y,y⟫ = 0. Then IsHilbertSum.mk hortho htotal.symm.le and .linearIsometryEquiv : H ≃ₗᵢ lp G 2. To prove coordinate identities (W (T y)) i = ..., compare two CLMs H →L G i using lp.evalCLM ℂ G 2 i and ContinuousLinearMap.ext_on on the span of ⋃ range V j, with linearIsometryEquiv_symm_apply_single and lp.single_apply_self / lp.single_apply_ne.