chore: syntax documentation for universe, open, export, variable

[AdrienChampion]

• Put an X in this bracket to confirm you have read the
  External Contribution Guidelines.

Mentored by @digama0, adds syntax-documentation with examples to universe, open, export, and variable.

The documentation shows up when hovering over keywords, hopefully improving the experience for beginners.

[leanprover-community-mathlib4-bot]

• ✅ Mathlib branch lean-pr-testing-2645 has successfully built against this PR. (2023-10-10 12:56:00) View Log
• ✅ Mathlib branch lean-pr-testing-2645 has successfully built against this PR. (2023-10-14 12:07:57) View Log
• ✅ Mathlib branch lean-pr-testing-2645 has successfully built against this PR. (2023-10-19 12:41:48) View Log
• ✅ Mathlib branch lean-pr-testing-2645 has successfully built against this PR. (2023-10-22 17:53:17) View Log
• ✅ Mathlib branch lean-pr-testing-2645 has successfully built against this PR. (2023-10-23 12:01:15) View Log
• ✅ Mathlib branch lean-pr-testing-2645 has successfully built against this PR. (2023-10-24 11:43:44) View Log
• 💥 Mathlib branch lean-pr-testing-2645 build failed against this PR. (2023-10-31 18:03:14) View Log
• ❗ Mathlib CI can not be attempted yet, as the 'nightly-testing-2023-11-04' branch does not exist there yet. We will retry when you push more commits. It may be necessary to rebase onto 'nightly' tomorrow. (2023-11-04 12:19:14)
• 💥 Mathlib branch lean-pr-testing-2645 build failed against this PR. (2023-11-05 01:56:31) View Log
• ✅ Mathlib branch lean-pr-testing-2645 has successfully built against this PR. (2023-11-06 16:57:19) View Log

[david-christiansen]

This is a great improvement, thanks!

I think it can be even better with some small modifications. They come in a few categories:

1. Describing not just what the feature does, but also the problems that it solves for users
2. Using less-abstract examples that are more likely to be understood by our audiences
3. Reducing the technical programming-languages jargon
4. Picking syntactic metavariables that have less potential for confusion

Thanks again, and please let me know if there's anything unclear in my comments!

[david-christiansen]

It looks like you've made great progress on it!

[david-christiansen]

Almost there! I'm happy to finish this up if you're getting discouraged, but I think there's just a couple minor details and then I'll think we're good to go. Thank you so much for your patience!