# Zulip Chat Archive

## Stream: new members

### Topic: when `library_search` fails you

#### Chris M (Jul 21 2020 at 04:52):

I've been having a recurring situation where I want to prove something relatively obvious, but I don't know the name of the lemma that mathlib gives to it. I generally use `library_search`

, but there isn't always a single lemma that can prove something. I end up adding lots of `have`

s for the assumptions of a lemma that I THINK is the way to prove this.

In the following example, I'm trying to prove `abs x * abs y ≤ abs x * ε`

```
import data.real.basic
import tactic
lemma my_lemma2 : ∀ {x y ε : ℝ},
0 < ε → ε ≤ 1 → abs x < ε → abs y < ε → abs (x * y) < ε :=
begin
intros x y ε epos ele1 xlt ylt,
have hx:0 ≤ abs x, {exact abs_nonneg x},
have hy:0 ≤ abs y, {exact abs_nonneg y},
calc
abs (x * y) = abs x * abs y : abs_mul x y
... ≤ abs x * ε : by library_search
... < 1 * ε : sorry
... = ε : one_mul ε
end
```

To show that `abs x * abs y ≤ abs x * ε`

I tried using `library_search`

but apparently there isn't a single lemma for this. I reasoned that the way to show this is by saying that `0≤a \to a * b ≤ a * c \iff b≤c`

, which didn't work. However then after reading in the tutorial, they suggested I use `mul_le_mul : ?M_3 ≤ ?M_5 → ?M_4 ≤ ?M_6 → 0 ≤ ?M_4 → 0 ≤ ?M_5 → ?M_3 * ?M_4 ≤ ?M_5 * ?M_6`

. I would not have discovered this without the tutorial telling me.

What general strategy should I adopt to find which lemma's to use in situations like this?

#### Shing Tak Lam (Jul 21 2020 at 05:07):

For finding lemmas, the inequality you need to prove is `_ * _ ≤ _ * _`

, so if you write down the symbols, it's `[mul, le, mul]`

. So searching for `mul_le_mul`

should find that lemma. To search, you can use VSCode search (make sure it can search in mathlib!), `grep`

or `Ctrl-P`

, then `#mul_le_mul`

Although I think for inequalities like this, just using `linarith`

and `nlinarith`

is probably faster than trying to find the exact lemma which solves it. In this case, you can replace `by library_search`

with `by nlinarith`

.

#### Chris M (Jul 22 2020 at 03:50):

Thanks :)

#### Chris M (Jul 22 2020 at 03:52):

Would it make sense for there to be a tactic that, like `library_search`

, searches the library, but instead merely looks for lemmas that pattern-match with your conclusion, and just lists all of those lemmas and their type signatures, even if it can't find an immediate way to use it.

#### Alex J. Best (Jul 22 2020 at 04:44):

@Chris M Have you seen `suggest`

?

#### Chris M (Jul 22 2020 at 04:46):

No I haven't! Looking at the the docs, it sounds great, I'll look at it. thanks :)

#### Jalex Stark (Jul 22 2020 at 12:04):

(I recommend doing a speed-read of the tactic docs page as a way to get a feel for what exists)

#### Bryan Gin-ge Chen (Jul 22 2020 at 12:10):

Shing Tak Lam said:

To search, you can use VSCode search (make sure it can search in mathlib!), [...]

`Ctrl-P`

, then`#mul_le_mul`

You can also hit `Ctrl-T`

, `mul_le_mul`

.

We usually recommend `library_search`

and `suggest`

now, but `#find`

works (slowly) on patterns like `_ * _ ≤ _ * _`

:

```
import tactic
#find _ * _ ≤ _ * _
```

Last updated: May 16 2021 at 05:21 UTC