Commit 2022-12-04 20:02 ce613251
View on Github →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.