# Zulip Chat Archive

## Stream: new members

### Topic: Finding Theorems

#### Alex Zhang (May 25 2021 at 12:38):

When I am writing a Lean project and if I want to use some lemma/theorem "L" to prove a new one, how do I know whether "L" has already existed in mathlib?

#### Kevin Buzzard (May 25 2021 at 12:39):

How can you use it if it doesn't exist? I'm a bit confused by this question.

#### Alex Zhang (May 25 2021 at 12:41):

"in mathlib" I mean, I edited the question. Sorry for any confusion.

#### Kevin Buzzard (May 25 2021 at 12:42):

Oh so "L" is a mathematical theorem, not a formalised one? You can search for it in the docs or ask in #Is there code for X?

#### Kevin Buzzard (May 25 2021 at 12:43):

If I'm hacking on `mathlib`

then I often just use the search functionality of VS Code.

#### Alex Zhang (May 25 2021 at 12:45):

Yeah, I do mean a math theorem or a commonly used lemma (such as if x is real, then x^2>=0).

#### Kevin Buzzard (May 25 2021 at 12:45):

For something as simple as that, I would guess the name of the lemma.

#### Kevin Buzzard (May 25 2021 at 12:46):

```
import data.real.basic
#check pow_two_nonneg -- works
```

#### Eric Rodriguez (May 25 2021 at 12:48):

other options include `library_search`

, `suggest`

, using `simp`

and seeing what lemmas it uses with`squeeze_simp`

#### Alex Zhang (May 25 2021 at 12:48):

Many thanks! I am just taking that simple lemma as an example.

#### Kevin Buzzard (May 25 2021 at 12:48):

The naming conventions are here.

#### Kevin Buzzard (May 25 2021 at 12:54):

Alex Zhang said:

Many thanks! I am just taking that simple lemma as an example.

Different examples require different techniques -- your question is very broad.

#### Alex Zhang (May 25 2021 at 13:11):

Eric, could you please explain how to use `squeeze_simp`

maybe with a #mwe?

#### Kevin Buzzard (May 25 2021 at 13:12):

This is the variant of your question where the theorem you want is actually your goal in a formalisation effort. You suspect the result is in the library, and then you discover that `simp`

solves the goal, you can replace it with `squeeze_simp`

and see what actually happened.

#### Anne Baanen (May 25 2021 at 13:13):

For example:

```
example : 4 * 0 = 0 := by squeeze_simp
-- Try this: simp only [mul_zero]
example : 4 * 0 = 0 := mul_zero _
```

Last updated: Dec 20 2023 at 11:08 UTC