# Zulip Chat Archive

## Stream: new members

### Topic: Lemma Help

#### David⚛️ (Apr 05 2023 at 17:53):

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 (Apr 05 2023 at 18:04):

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⚛️ (Apr 05 2023 at 18:06):

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 (Apr 05 2023 at 18:29):

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

#### David⚛️ (Apr 06 2023 at 17:11):

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 (Apr 06 2023 at 17:14):

Do `import Mathlib.Tactic.LibrarySearch`

and you will have the same tactic as in Lean 3

#### David⚛️ (Apr 19 2023 at 06:35):

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

Suggestions, please.

Last updated: Dec 20 2023 at 11:08 UTC