Use Lean 4 as default in documentation and unqualified toolchain references

[Kha]

No description provided.

[kim-em]

One thought about the documentation:

The fact that you can create custom releases of Lean 4 simply by pushing a tag to your own fork, and then specifying e.g. semorrison/lean4:release-20230620-max either in lean-toolchain or with elan toolchain, seems to be a secret only "documented" in zulip. Might we want to add a sentence or two here? This is really useful to know if when you need to test changes against mathlib (and want CI assistance, so mere elan override with a local Lean 4 is insufficient).

[Kha]

@semorrison I think it's roughly documented at the right place:

$ elan toolchain help
elan-toolchain
Modify or query the installed toolchains

USAGE:
    elan toolchain <SUBCOMMAND>

FLAGS:
    -h, --help    Prints help information

SUBCOMMANDS:
    list         List installed toolchains
    install      Install or update a given toolchain
    uninstall    Uninstall a toolchain
    link         Create a custom toolchain by symlinking to a directory
    help         Prints this message or the help of the given subcommand(s)

DISCUSSION:
    Many `elan` commands deal with *toolchains*, a single
    installation of the Lean theorem prover. `elan` supports multiple
    types of toolchains. The most basic track the official release
    channel: 'nightly'; but `elan` can also install toolchains from
    the official archives and from local builds.

    Standard release channel toolchain names have the following form:

        [<origin>:]<channel>[-<date>]

        <channel>       = nightly|<version>
        <date>          = YYYY-MM-DD

    'channel' is either a named release channel or an explicit version
    number, such as '4.0.0-m5'. Channel names can be optionally appended
    with an archive date, as in 'nightly-2018-04-10', in which case
    the toolchain is downloaded from the archive for that date.
    'origin' can be used to refer to custom forks of Lean on Github;
    the default is 'leanprover/lean'. For nightly versions, '-nightly'
    is appended to the value of 'origin'.

    elan can also manage symlinked local toolchain builds, which are
    often used to for developing Lean itself. For more information see
    `elan toolchain help link`.

That doesn't tell you how to create such a release, but that doesn't really belong to elan's documentation

[kim-em]

I've added information about generating releases from tags at leanprover/lean4#2302.

Let's merge this, and I'll update the community webpage docs!