refactor(frontends/lean): rename parser methods is_section* to is_local*
fix(emacs/lean-syntax): glitch on syntax highlight
feat(frontends/lean): add 'universe variable' command

We can declare variables anywhere. So, we must also be able do declare
"universe" variables anywhere. Here is a minimal example that requires
this feature

```
-- We want A and B to be in the same universe
universe variable l
variable A : Type.{l}
variable B : Type.{l}
definition tst := A = B
```

The following doesn't work because A and B are in different universes
```
variable A : Type
variable B : Type
definition tst := A = B
```

The following works, but tst is not universe polymorphic, since l is
one *fixed* global universe
```
universe l
variable A : Type.{l}
variable B : Type.{l}
definition tst := A = B
```
refactor(frontends/lean): adjust function names to reflect how parameters/variables behave
feat(library/algebra/category): use variables instead of parameters
refactor(library/algebra/category): remove unnecessary sections
refactor(frontends/lean): do not expose unnecessary functions
feat(frontends/lean/notation_cmd): remove the cleanup notation hack
feat(frontends/lean): allow parameters only in contexts
refactor(library/scoped_ext): sections are just "nameless" namespaces
feat(frontends/lean): do not allow coercion definition in sections
feat(frontends/lean): add '[]' notation for marking arguments where class-instance resolution should be applied
fix(library/data/prod): make the notation for tuples and product types consistent
fix(emacs/lean-syntax): syntax highlight for declarations with explicit universes
test(tests/lean/run): expand tree example
fix(frontends/lean/decl_cmds): error messages
feat(frontends/lean): add option '-X': discard all proofs after theorems are checked

This option is useful for generating compact .olean files for web demos
feat(library/kernel_serializer): compress binder modifier annotations when saving .olean file
refactor(frontends/lean/parser): add missing 'const'
feat(frontends/lean): elaborate inductive datatypes and introduction rules as a single elaboration problem