bump mathlib manual

Stream: mathlib documentation

[Jon Eugster]

Michael Rothgang said:

rss-bot said:

feat(Tactic): dependent rewriting ct'd (mathlib4#26835)

Add dependent rewrite tactics rw! and rewrite!.
These operate by inserting casts in front of terms that would otherwise become type-incorrect after the rewrite.
In the default mode, only proof terms are casted, so that (by proof irrelevance) no observable complexity is added.
In the most liberal mode, the tactics never encounter the 'motive is not type correct' error,
but may add casts that make the goal or other term very complex.

Co-authored-by: Aaron Liu <aaronliu2008@outlook.com>

Co-authored-by: Wojciech Nawrocki <wjnawrocki@protonmail.com>
Co-authored-by: Aaron Liu <aaronliu2008@outlook.com>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>

Authored-by: Vtec234 (commit)

Jon Eugster Can we bump the mathlib manual again to include these tactics? (Is there a way to help out with this?) Thanks!

@Michael Rothgang currently the mathlib manual follows stable releases of Verso+Mathlib. These tactics will be included in the v4.22.0 bump.

I guess you could update it manually before that (it's the same as every Lean project) or if you do have the resources to fix it more frequently, one could change it to move with main/master. If you fancy, you could also set-up a clever CI which tries to follow main automatically. That should not be hard, I've just haven't done it yet because in the past Verso/Lean updates broke projects quiet often when they didn't follow stable releases.