feat: test minimizing slowdown from #4595

[kim-em]

This is a minimization of a fairly typical slowdown from #4595 in Mathlib. The bad slowdowns seem to mostly be in declarations that generate many different simp proofs internally (often via aesop).

This test works fine on master, but is very slow on #4595. There's some nonlinearity going on here: the time savings coming from replacing each simp only by sorry adds up to more than the total time.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 31de2494fb603081d261a5ded574b7c2f884c755 --onto ce73bbe277140201cdb3ad3015c13d01948704b2. (2024-07-16 03:19:03)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 1a9cbc96f1cbbbd2bb0092e574c5de64dc9d948c --onto ce73bbe277140201cdb3ad3015c13d01948704b2. (2024-07-16 13:47:18)

[kim-em]

I've moved this directly into #4595. (I'm not entirely sure why I didn't do that in the first place.)