Schwarz inequality (real)

import Mathlib

theorem cauchy_schwarz_real {n : ℕ} (x y : Fin n → ℝ) : (∑ i, x i * y i) ^ 2 ≤ (∑ i, x i ^ 2) * (∑ i, y i ^ 2) :=
  Finset.sum_mul_sq_le_sq_mul_sq Finset.univ x y