theorem InnerProductSpaces.exists_orthonormal_basis {𝕜 : Type u_1} [RCLike 𝕜] {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [FiniteDimensional 𝕜 V] : Nonempty (OrthonormalBasis (Fin (Module.finrank 𝕜 V)) 𝕜 V)