feat: upstream and update #where command

[kmill]

This command comes from Lean 3, which I had previously ported and contributed to Batteries (née Std). In this new version, #where produces actual command Syntax for all features of a top-level scope (rather than splicing together strings), and it also now reports included variables.

[kmill]

@semorrison Here's an upstreamed #where!

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-5065 has successfully built against this PR. (2024-08-16 02:08:53) View Log
• 🟡 Mathlib branch lean-pr-testing-5065 build against this PR was cancelled. (2024-08-16 16:02:18) View Log
• ✅ Mathlib branch lean-pr-testing-5065 has successfully built against this PR. (2024-08-16 17:07:37) View Log

[leanprover-community-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 8822b0fca7f0b232742e7ee1aea92067e4340952 --onto 09e1a05ee922bf8581ba9820f096ac1a2b1a2945. (2024-10-25 01:49:37)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 8822b0fca7f0b232742e7ee1aea92067e4340952 --onto 4ee44ceb1d77f16b9b81bc655bc8b318cd6e8c4d. (2024-10-30 02:16:41)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 8822b0fca7f0b232742e7ee1aea92067e4340952 --onto 38c39482f40536b864a9b43c718e10e8413b26e5. (2024-10-30 18:01:31)