## 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 withsqueeze_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.

#### 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