chore(*): bump to lean 3.47.0 (#16252)
A major change is that notations now require names when they are shadowing another identical notation, even if it is a local notation. Also, because localized notations can be imported in a variety of contexts, there are some new best practices for them:
* localized notations should always have a `(name := ...)`. Notation names are unrelated to declaration names, but the declaration name is a reasonable base for the notation name.
* localized notations should never use `_` in the notation, because this gets desugared to a unique metavariable index, meaning that the notation will not be recognized as a duplicate of itself if `open_locale` is used when the notation is already available. Instead, you should use the `hole!` notation, which unfolds to `_`.
Another major change is that projection notation (`x.foo`) now always instantiates implicit arguments with metavariables, which is consistent with Lean 4. To simulate the older behavior, one can use either strict implicit arguments for the structure field (e.g. `∀ {{n}}, p n` instead of `∀ {n}, p n`) or, depending on specifics, writing `λ _, x.foo` to ensure the implicit argument is preserved as an argument.
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
