[Merged by Bors] - chore(*): bump to lean 3.47.0

[digama0]

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.

[kmill]

I notice you're going through a cycle of fixing issues with projection notation. I just want to be sure you know that the changes I submitted worked, so if you're switching to strict implicit arguments for stylistic reasons then feel free to carry on.

I also added a blurb to the PR description about the breaking change to projection notation.

[digama0]

Yes, unfortunately what happened is that your notification that you had pushed the changes happened exactly when I had finished my own local compile of mathlib, including the projection fixes. So the cycle of fixes now is only the result of merge conflicts between our two (individually working) changes.

[kmill]

I see -- if I had known you were also doing projection fixes I'd have left it to you! When you said on Zulip that it was good to know I was working on it, I was under the impression that this meant that you weren't. Now we're spending more than twice the time on this collectively than necessary.

[gebner]

bors r+

[YaelDillies]

It's a bit sad seeing the heuristic that you can fill the op_mem field of a subobject_class instance with λ s, s.op_mem' breaking.

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests

[kmill]

@YaelDillies Maybe we should take this as motivation to use {{...}} arguments more often (though it would be nice to have some way to easily turn these into standard implicit arguments).

Consider also that projections now elaborate the same way as any other function (for example, it's id : ?M_1 → ?M_1 not id : Π {α : Sort u_1}, α → α).