mathlib3

b21c9aa1 - chore(analysis/inner_product_space): golf two proofs (#15679)

chore(analysis/inner_product_space): golf two proofs (#15679) Golf two proofs and move the lemmas into `inner_product_space/basic` since they now only depend on elementary facts about inner product spaces.