Lemma Help

Stream: new members

[David⚛️]

This thread is mainly to assist new members on how to search out appropriate Lemmas. I am new to Lean 4, and I need help on how to navigate or call appropriate lemmas in Lean Proof.
Any trick or suggestion will go a long way to help.
Useful resources will be appreciated.
Thanks

[Mario Carneiro]

The easiest way to find lemmas in mathlib are:

• the library_search tactic tries to prove your goal in one step using anything in the library. So you can write the signature of a theorem you think exists and see if this tactic proves the goal
• The mathlib docs can be searched to find lemmas by name or by docstring
• grep or file search in mathlib itself can also sometimes be helpful, and is often the fastest option although it's obviously not as smart as the other options
• The #Is there code for X? stream is human-powered mathlib search, you can ask about a theorem or area of mathematics and find out about what we currently have and near-term plans for where we are headed, PRs that are in limbo or work on peoples' local machines that you won't find through the other methods.

[David⚛️]

Mario Carneiro said:

The easiest way to find lemmas in mathlib are:

• the library_search tactic tries to prove your goal in one step using anything in the library. So you can write the signature of a theorem you think exists and see if this tactic proves the goal
• The mathlib docs can be searched to find lemmas by name or by docstring
• grep or file search in mathlib itself can also sometimes be helpful, and is often the fastest option although it's obviously not as smart as the other options
• The #Is there code for X? stream is human-powered mathlib search, you can ask about a theorem or area of mathematics and find out about what we currently have and near-term plans for where we are headed, PRs that are in limbo or work on peoples' local machines that you won't find through the other methods.

Thank you

[Alex J. Best]

The mathlib 4 docs (https://leanprover-community.github.io/mathlib4_docs/) is the one you want if you are using lean 4 though

[David⚛️]

Mario Carneiro said:

The easiest way to find lemmas in mathlib are:

• the library_search tactic tries to prove your goal in one step using anything in the library. So you can write the signature of a theorem you think exists and see if this tactic proves the goal
• The mathlib docs can be searched to find lemmas by name or by docstring
• grep or file search in mathlib itself can also sometimes be helpful, and is often the fastest option although it's obviously not as smart as the other options
• The #Is there code for X? stream is human-powered mathlib search, you can ask about a theorem or area of mathematics and find out about what we currently have and near-term plans for where we are headed, PRs that are in limbo or work on peoples' local machines that you won't find through the other methods.

Hello Mario,
Does library_search work for LEAN 4? is not working for me

[Jeremy Tan]

Do import Mathlib.Tactic.LibrarySearch and you will have the same tactic as in Lean 3

[David⚛️]

How do I read this document (book) Theorem Proving in Lean 4 on vscode?
Suggestions, please.