tactic cheatsheet

Stream: general

[Floris van Doorn]

I have updated my tactic cheatsheet (pdf, tex) that I used for my course last year. It is now 2.5 pages and pretty extensive.
Some categorizations are a bit arbitrary, and I'll probably still move things around a bit.
Comments or PRs are welcome.

[Floris van Doorn]

After a round of comments, I will upload it to the community website and add it to https://leanprover-community.github.io/learn.html

[Shreyas Srinivas]

One comment: simp_rw can write under binders while rw cannot. It might be useful to mention this

[Floris van Doorn]

There is a lot of things to tell about tactics. I try to keep each description here to 1 line, so I cannot go into all the details, or explain the difference between two tactics. That information should go elsewhere.

[Floris van Doorn]

I created a PR adding (a slightly updated) tactic cheatsheet to the Leanprover-community website: https://github.com/leanprover-community/leanprover-community.github.io/pull/584 (for users using Mathlib)

[Jon Eugster]

@Floris van Doorn I've created a verso manual yesterday which is inteded to talk about tactics and also has an automatically generated list of all tactics:

https://leanprover-community.github.io/mathlib-manual/html-multi/

it's not linked anywhere yet. We should at least cross-link these resources, or maybe your content could be (eventually) added as a first section there, giving some interactive features from verso

[Floris van Doorn]

Oh nice!

That is a very useful recourse, which we should widely link to once it's ready for user consumption. I'm happy if my pdf is just a printable summary of this; browsing it with verso is often nicer of course (and you can give a significantly more detailed description on a webpage).

Noticed a small typo: Coersions -> Coercions

[Jason Rute]

There are other tactic lists here (https://proofassistants.stackexchange.com/questions/3986/is-there-a-complete-index-of-lean-4-tactics) and when your lists are ready, maybe they should be answers there as well.

[Asei Inoue]

I created these:

• https://seasawher.github.io/mathlib4-help/tactics/
• (Japanese only) https://lean-ja.github.io/lean-by-example/

[Jz Pan]

I think there is a mistake in the cheatsheet: #loogle does not require Internet connection; it will search all imported results matching the search query.

[Jireh Loreaux]

That's not true?

[Jz Pan]

Oh sorry. I've read that loogle can be run locally (https://github.com/nomeata/loogle?tab=readme-ov-file#running-locally). I think that #loogle must uses this feature...

[Jireh Loreaux]

Yes, you can run loogle locally, but you have to build the index yourself, which takes time most users aren't willing to spend (and you would need to redo it every time you check out a new branch).