mathlib

a1c17e2a - perf(analysis/normed_space/lp_space): fix timeout by squeezing simps (#17108)

perf(analysis/normed_space/lp_space): fix timeout by squeezing simps (#17108) elaboration of has_sum_single took 17.9s -> 1.37s The timeout happens in an unrelated branch #16317 ([CI log](https://github.com/leanprover-community/mathlib/actions/runs/3294947441/jobs/5432990411)) but not yet in bors batches apparently.