Set a default toolchain in our devcontainer.

Sets it to the toolchain of the project we're cloning, if any, or
otherwise to stable.

Setting it at all is useful in order to enable single files to work (be
editable) without warning to standard error that no default toolchain is
configured.

.devcontainer/lazyvim/Dockerfile

@@ -35,7 +35,7 @@ COPY lean.lua .config/nvim/lua/plugins/lean.lua
 
 ARG LEAN_PROJECT=https://github.com/leanprover-community/mathlib4
 
-RUN git clone --filter=blob:none $LEAN_PROJECT && cd $(basename "$LEAN_PROJECT") && lake exe cache get
+RUN git clone --filter=blob:none $LEAN_PROJECT && cd $(basename "$LEAN_PROJECT") && lake exe cache get && elan default "$(cat lean-toolchain || echo stable)"
 
 # SHELL isn't supported by OCI images
 CMD ["zsh", "-l"]