lean core nightly bump

Stream: mathlib4

[Arthur Paulino]

Starting out this thread so we can post nightly bump PRs since they should be merged ASAP.

mathlib4#257 (by @Edward Ayers )

[Edward Ayers]

Maybe it's a sensible policy that as long as the CI passes and no really big changes are happening in the PR for a nightly bump it's ok to merge? @Gabriel Ebner does that sound ok?

[Arthur Paulino]

Still good to post though, just to make everyone aware that we're up to date

[Mario Carneiro]

yeah I don't think we need to chronicle these

[Arthur Paulino]

Some bumps do need reviews tho. I'll be posting the ones I make here

[Gabriel Ebner]

Maybe it's a sensible policy that as long as the CI passes and no really big changes are happening in the PR for a nightly bump it's ok to merge?

Yes, that's perfectly ok. Please bors r+ them as you see fit. mathlib4#254 has/had some nontrivial changes though, so it was good to wait for reviews.