Lean: [T*] ~ [T] from the polar decomposition, using two range-projection lemmas

To show V*V = [T*] and VV* = [T] for the polar part V of T (range projections = starProjection of the closure of the range), two small lemmas avoid any subspace bookkeeping. (1) Minimality: if E * T = T then E * [T] = [T]. Prove it with closure_minimal on the closed set {y | E y = y}, after rewriting Submodule.topologicalClosure_coe and LinearMap.coe_range. (2) If A = B C and B = A D then [A] = [B]: apply (1) both ways, take star of one equation, and chain. For V*V, the initial space is the range projection of |T|, and |T| = T* V, T* = |T| V* (star of V* T = |T| and V|T| = T). For VV*, get [T] V = V from uniqueness of the polar decomposition (U|T| = T and U vanishes on ker T), and get VV* T = T from V V* V = V. Then E := VV* satisfies [T] E = E and E [T] = [T], so E = [T].