This PR enables auto-implicits in the Lake math template. This resolves
an issue where new users sometimes set up a new project for math
formalization and then quickly realize that none of the code samples in
our official books and docs that use auto-implicits work in their
projects. With the introduction of [inlay hints for
auto-implicits](https://github.com/leanprover/lean4/pull/6768), we
consider the auto-implicit UX to be sufficiently usable that they can be
enabled by default in the math template.
Notably, this change does not affect Mathlib itself, which will proceed
to disable auto-implicits.
This change was previously discussed with and agreed to by the Mathlib
maintainer team.
e123b327a5