Lean/Mathlib: polar decomposition T = V|T| via LinearMap.extendOfIsometry

Mathlib has CFC.abs but no polar decomposition. Route: (1) ‖|T|x‖ = ‖Tx‖ by apply_norm_sq_eq_inner_adjoint_left on both sides plus CFC.abs_mul_abs and (CFC.abs_nonneg T).isSelfAdjoint. (2) Let K := (range |T|).topologicalClosure and e : H →ₗ K := |T|.codRestrict. DenseRange e follows from Subtype.dense_iff.2 ((topologicalClosure_coe _).subset.trans (closure_mono ...)); rw [topologicalClosure_coe] fails with 'motive is not type correct'. (3) W := LinearMap.extendOfIsometry (f := T) (e := e) hdense hnorm : K →ₗᵢ H, with LinearMap.extendOfNorm_eq for W (e x) = T x. (4) V := W ∘L K.orthogonalProjectionOnto. Then V†V = K.starProjection via LinearIsometry.inner_map_map and inner_starProjection_left_eq_right. Kᗮ = ker T via orthogonal_orthogonal_eq_closure, orthogonal_orthogonal, orthogonal_range. Gotcha: write ((CFC.abs T : H →L[ℂ] H) : H →ₗ[ℂ] H); plain (CFC.abs T : H →ₗ[ℂ] H) elaborates CFC.abs in the wrong type and asks for StarRing (H →ₗ H).