chore(analysis/inner_product_space/basic): golf the proof of Cauchy-S…

…chwarz (#18938)

## API changes

- Add `inner_product_space.to_core`.
- Make `inner_product_space.core` extend `has_inner`.
- Rename namespace from `inner_product_space.of_core` to `inner_product_space.core`.
- Rename `inner_product_space.of_core.inner_norm_sq_eq_inner_self` to
  `inner_product_space.core.coe_norm_sq_eq_inner_self`.
- Add `inner_product_space.core.norm_inner_symm`.
- Add `inner_product_space.core.cauchy_schwarz_aux`, use it to golf
  the proof of the Cauchy-Schwarz inequality and its versions.
- Use norm instead of `is_R_or_C.abs` here and there, the rest will
  migrate in #18919.
- Rename `inner_product_space.of_core.abs_inner_le_norm` to
  `inner_product_space.core.norm_inner_le_norm`, use norm.
- Add `norm_inner_eq_norm_tfae` and `inner_eq_norm_mul_iff_div`.
- Rename `abs_inner_div_norm_mul_norm_eq_one_iff` to
  `norm_inner_div_norm_mul_norm_eq_one_iff`, use norm.
- Rename `inner_eq_norm_mul_iff_of_norm_one` to
  `inner_eq_one_iff_of_norm_one`.



Co-authored-by: Johan Commelin <johan@commelin.net>

docs/undergrad.yaml

@@ -216,7 +216,7 @@ Bilinear and Quadratic Forms Over a Vector Space:
     dual isomorphism in the euclidean case: 'inner_product_space.to_dual'
     orthogonal complement: 'submodule.orthogonal'
     Cauchy-Schwarz inequality: 'inner_mul_inner_self_le'
-    norm: 'inner_product_space.of_core.to_has_norm'
+    norm: 'inner_product_space.core.to_has_norm'
     orthonormal bases: 'maximal_orthonormal_iff_basis_of_finite_dimensional'
   Endomorphisms:
     orthogonal group: 'matrix.orthogonal_group'