feat: allow using language id lean in markdown code blocks (#622)

This PR ensures that doc comments can use `lean` in addition to `lean4`
for the language ID in markdown code blocks and also have them be
highlighted in hovers.

Author: mhuisi

vscode-lean4/package.json

@@ -666,6 +666,10 @@
                     ".lean"
                 ]
             },
+            {
+                "id": "lean",
+                "configuration": "./language-configuration.json"
+            },
             {
                 "id": "lean4markdown",
                 "aliases": [],
@@ -695,6 +699,11 @@
                 "embeddedLanguages": {
                     "meta.embedded.block.lean4": "lean4"
                 }
+            },
+            {
+                "language": "lean",
+                "scopeName": "source.lean4",
+                "path": "./syntaxes/lean4.json"
             }
         ],
         "keybindings": [