v4.12.0-rc1

Stream: mathlib4

[Kim Morrison]

Mathlib has just moved to v4.12.0-rc1.

There are a number of changes that will impact Mathlib users; I'm out of time right now but will try to write more later (or others can!).

One nice quick piece of news that is that our instruction count has dropped by 5% with this release!

[Kim Morrison]

There are some known issues with aesop and bound; these seem to work in Mathlib itself, but there are regressions in the test suites which haven't yet been diagnosed. Please report problems with these tactics.

[Kim Morrison]

simp [(· ∘ ·)] no longer works, and you need to write simp [Function.comp_def] instead. (Moreover, the @[eqns] attribute probably doesn't work at all anymore, because it is depending on internals that have changed.)

We're discussing what to do about this, but for now please assume that Function.comp_def is the way to go!

[Eric Wieser]

Kim Morrison said:

simp [(· ∘ ·)] no longer works, and you need to write simp [Function.comp_def] instead. (Moreover, the @[eqns] attribute probably doesn't work at all anymore, because it is depending on internals that have changed.)

Are these the same change, or is simp [(. + .)] also no longer allowed as a spelling of simp [HAdd.hAdd]?

[Kim Morrison]

No, it's just a consequence of @[eqns] no longer working.