Remove the space from Lean 4

[eric-wieser]

This makes lean4 work as a markdown block language instead of lean-4.

Description

This change is consistent with how Pygments-based highlighters demarcate Lean 4. I estimate that exactly no one has ever written ```lean-4, as no one will have thought to try!

Checklist:

• I am adding a new extension to a language.

  • The new extension is used in hundreds of repositories on GitHub.com
    • Search results for each extension:
      • https://github.com/search?type=code&q=NOT+is%3Afork+path%3A*.FOOBAR+KEYWORDS
  • I have included a real-world usage sample for all extensions added in this PR:
    • Sample source(s):
      • [URL to each sample source, if applicable]
    • Sample license(s):
  • I have included a change to the heuristics to distinguish my language from others using the same extension.

• I am adding a new language.

  • The extension of the new language is used in hundreds of repositories on GitHub.com.
    • Search results for each extension:
      • https://github.com/search?type=code&q=NOT+is%3Afork+path%3A*.FOOBAR+KEYWORDS
  • I have included a real-world usage sample for all extensions added in this PR:
    • Sample source(s):
      • [URL to each sample source, if applicable]
    • Sample license(s):
  • I have included a syntax highlighting grammar: [URL to grammar repo]
  • I have added a color
    • Hex value: #RRGGBB
    • Rationale:
  • I have updated the heuristics to distinguish my language from others using the same extension.

• I am fixing a misclassified language

  • I have included a new sample for the misclassified language:
    • Sample source(s):
      • [URL to each sample source, if applicable]
    • Sample license(s):
  • I have included a change to the heuristics to distinguish my language from others using the same extension.

• I am changing the source of a syntax highlighting grammar

  • Old: [URL to grammar repo]
  • New: [URL to grammar repo]

• I am updating a grammar submodule

• I am adding new or changing current functionality

  • I have added or updated the tests for the new or changed functionality.

• I am changing the color associated with a language

  • I have obtained agreement from the wider language community on this color change.
    • [URL to public discussion]
    • [Optional: URL to official branding guidelines for the language]

[eric-wieser]

Some evidence that the language community is in favor is on Zulip at #general > Markdown codeblocks: `lean4` or `lean-4`? @ 💬

[lildude]

This makes lean4 work as a markdown block language instead of lean-4.

If this is your sole reason, this is the wrong thing to do. Adding an alias is what you should be doing instead.