Is there a tactic manual?

Stream: new members

[Jiang Jiedong]

Hi everyone,

I think maybe a major obstacle of new members getting more familiar with lean after reading mathematics_in_lean is that they still don't know how many tactic exists in lean and what each tactic does. For example, I learned quite recently that there is a powerful tactic called omega. Is there a cheatsheet that lists all (or most) tactics somewhere? Is there a searching method for the tactics? I think these materials will definitely help new members greatly.

[Rida Hamadani]

This one is by @Martin Dvořák :
https://github.com/madvorak/lean4-tactics

[Rida Hamadani]

It is not exhaustive but still useful, I wonder if we can do PRs to it in order to add new tactics.

[María Inés de Frutos Fernández]

There is also a quite complete list of tactics here, but omega is not there yet.

[Markus Schmaus]

I found the #help command from Mathlib to be a good way to search for tactics tactics:

import Mathlib

#help tactic omega

[Martin Dvořák]

Rida Hamadani said:

I wonder if we can do PRs to it in order to add new tactics.

Please do!