feat: copy `#time` command from Mathlib

[alexkeizer]

Description:

Copy the #time command, with some adaptations, from Mathlib, since it's very useful in getting rough performance numbers for automation.

License-wise, this should be fine, since both are Apache licensed, but we're waiting on an official answer from Leo on that.

EDIT: Leo confirmed it's fine, but also suggested asking Kim if it's worth upstreaming to core, so I've pinged them. Let's wait for the result of that

License:

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.

[bollu]

LGTM, yoink it in. Maybe ask Kim if we can toss it into core :)

[shigoel]

When we bump the toolchain to at least nightly-2024-08-15 where #time was upstreamed, we can snuff out this PR.

[alexkeizer]

We can't really update the toolchain until LeanSAT gets merged completely (or the library gets updated, but that's unlikely to happen). Luckily, the process seems to be going quite quickly: PR 4 out of 6 just got merged