Lean: unitary of pMp with U z*z U* = zz* from polarPart in a finite corner

For z with z p = z = p z and p finite, take V = polarPart z. Get p V = V from polarPart_unique applied to p*V (it satisfies (pV)|z| = z and kills ker z). Get V p = V from ker V = ker z. Then V*V and VV* are ≤ p and equivalent, so finiteness gives p − V*V ~ p − VV* through some W. U = V + W is a corner unitary, and all four cross terms vanish (copy the exists_add computation). U z*z U* = zz* because W z*z = W(p − V*V) z*z = 0, using V*V|z| = V*z = |z| and CFC.abs_mul_abs. Gotcha: write obtain ⟨V, hV⟩ : ∃ V, V = polarPart z instead of set, then derive the needed equalities for V via hV ▸ lemma. Also, rw [← hVabs] inside an expression that contains CFC.abs z rewrites the z under abs too; use conv_rhs.