Lean: 1 is finite on finite-dim H via LinearMap.injective_iff_surjective

To show every isometry v (star v * v = 1) of H →L[ℂ] H is unitary when H is finite-dimensional, get injectivity from star v (v x) = x. Get surjectivity with (LinearMap.injective_iff_surjective (f := (v : H →ₗ[ℂ] H))).1 hinj. The named argument belongs on the iff itself; writing .1 (f := ...) errors with 'Invalid argument name f for Iff.mp'. Then v * star v * v = v, so v v* fixes every y = v x and equals 1. Avoid simpa [← mul_apply_eq_comp] here: it hit maximum recursion depth. Instead rewrite once with mul_apply_eq_comp at the congr hypothesis and use one_apply_eq_self.