Clean up some deprecations etc.

This PR ended up as a bit of a pile of stuff, but hopefully each point is uncontroversial.

Update Lean to recent nightly.
Avoid deprecated MetaM functions like withMVarContext.
Avoid mkConst in favour of Expr.const, and the same for other Expr constructors.
Use isImplementationDetail instead of isAuxDecl.
Various improved formulations.

fixes #68 fixes #76

Btw I noticed that the deprecation linter didn't flag our use of deprecated functions. Any idea why this might be?

leanprover-community / lean4-metaprogramming-book