mathlib3

ce613251 - chore(analysis/inner_product_space/rayleigh): squeeze a simp (#17811)

chore(analysis/inner_product_space/rayleigh): squeeze a simp (#17811) This lemma times out in #14228. Regardless of whether the other PR gets merged, the elaboration time drops from ~11s to ~2s with the squeeze, so I thought of PRing separately anyway.