Any summary of all Lean tactics?

Stream: new members

[Ching-Tsun Chou]

I learned of the omega tactic only yesterday, more than three months after starting to use Lean and having read #mil and browsed through the other three introductory books given here. (None of those books mention the omega tactic.). I wonder what else I have been missing. Is there a summary of all Lean tactics?

[Aaron Liu]

https://seasawher.github.io/mathlib4-help/

[Ching-Tsun Chou]

Alas, why isn't this on the official Lean community page?

[Julian Berman]

It will be shortly, a version is being worked on.

[Robin Arnez]

Note that you can also just #help tactic within lean

[Tomas Skrivan]

Is there any description of the new mysterious tactic grind? I keep on reading about it in the Lean 4 updates but have no clue what it is supposed to do.

[Aaron Liu]

I also have no idea what it's supposed to do. Apparently it will also supercede omega?

[Ruben Van de Velde]

Nothing more than is said in #lean4 > `grind` is refined `cc` without AC module?, as far as I know

[Kyle Miller]

It's not officially released yet, but when it is there will be more information.

[Robin Arnez]

There is a "guide" for it in the test files https://github.com/leanprover/lean4/blob/master/tests/lean/run/grind_guide.lean

[Robin Arnez]

actually some of the other tests there might also help understanding what it is capable of

[Vlad Tsyrklevich]

Ching-Tsun Chou said:

I learned of the omega tactic only yesterday, more than three months after starting to use Lean and having read #mil and browsed through the other three introductory books given here. (None of those books mention the omega tactic.). I wonder what else I have been missing. Is there a summary of all Lean tactics?

Note that omega was only released in the last year, that is the reason many resources have not been updated to use/mention it.

[spamegg]

There is this for Mathlib4: https://github.com/haruhisa-enomoto/mathlib4-all-tactics