feat: run hint tactics in parallel

[semorrison]

Note that this is more resource intensive, as all hint tactics will start running at once.

I've worked out how to thread through cancellation hooks so as soon as one succeeds, any still running are cancelled. (If they are doing kernel computations or IO they might not listen, however!)

---

• depends on: [Merged by Bors] - chore: reduce imports of Data.List.Defs #8635

I've had to make this depend on #8635 to avoid breaking an assert_not_exists statement.

[semorrison]

Here for example we used to run linarith first, and as it succeeded that was all that was reported.

Now exact? succeeds more quickly, and that prevents linarith being reported.

[thorimur]

I've put the parallelism through some paces on my end, making sure that it e.g. doesn't propagate state between tasks, does in fact start all tasks before cancelling, leaves the outer monad in an appropriate state after takeUpToFirst and asArray, etc.... It behaved as expected in all cases! :)

These review comments are mostly very small and quick style changes for readability (and therefore maintainability). I tried to get rid of .2.1 style access in favor of clearer destructuring.

There's one meaningful comment in the test file, which is on how aesop produces a warning in one case which isn't reflected in the suggestions.

I did eventually figure out how to reduce all of the MLList.Meta code via MonadControl, but it preferably requires a core change because the instance is a bit wonky. We can leave that for another PR! :)

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• [Merged by Bors] - chore: reduce imports of Data.List.Defs #8635
  By Dependent Issues (🤖). Happy coding!