# Zulip Chat Archive

## Stream: new members

### Topic: Basic inequalities

#### Emiel Lanckriet (Jul 16 2020 at 14:51):

I want to show that `y - x < e`

given `abs(x - y) < e`

and ` x \leq y`

. I found a lemma

```
theorem abs_of_nonpos :
a ≤ 0 → abs a = -a
```

but I can't figure out how to get `x - y \leq 0`

from ` x \leq y`

.

Does anyone have any hints?

#### Dan Stanescu (Jul 16 2020 at 14:59):

Try `linarith`

.

```
import tactic
import data.real.basic
example (x y : ℝ) (h : x - y ≤ 0) : x ≤ y := by linarith
```

#### Ruben Van de Velde (Jul 16 2020 at 15:31):

Other way around, I think, which can be solved with

```
example (x y : ℝ) (h : x ≤ y) : x - y ≤ 0 := sub_nonpos_of_le h
```

#### Emiel Lanckriet (Jul 16 2020 at 15:31):

Can you use linarith in the begin end-mode? Because each time I try it, the program seems to get stuck. When I make its own functions then it works.

#### Ruben Van de Velde (Jul 16 2020 at 15:32):

Alternatively,

```
example (x y : ℝ) (h : x ≤ y) : x - y ≤ 0 := by library_search
```

gives

```
Try this: exact sub_nonpos.mpr h
```

#### Bryan Gin-ge Chen (Jul 16 2020 at 15:33):

@Emiel Lanckriet Could you post an #mwe ? I don't know what you mean here:

Because each time I try it, the program seems to get stuck. When I make its own functions then it works.

#### Dan Stanescu (Jul 16 2020 at 15:35):

Emiel Lanckriet said:

Can you use linarith in the begin end-mode? Because each time I try it, the program seems to get stuck. When I make its own functions then it works.

Like this?

```
example (x y : ℝ) (h : x ≤ y) : x - y ≤ 0 :=
begin
linarith, done
end
```

#### Emiel Lanckriet (Jul 16 2020 at 15:37):

Sorry, I must have wrongly identified the problem because I can't seem to reproduce it and the example works.

#### Dan Stanescu (Jul 16 2020 at 15:42):

Emiel Lanckriet said:

Sorry, I must have wrongly identified the problem because I can't seem to reproduce it and the example works.

No problem, remember to post minimal working examples:

https://leanprover-community.github.io/mwe.html

so we can help more effectively.

#### Emiel Lanckriet (Jul 18 2020 at 08:56):

Is there a function that has signature `abs(x) < e -> x > 0 -> x < e`

? Also, is there a way to comb through mathlib using type signatures much like the searches you can do in Hoogle for Haskell commands?

#### Eloi (Jul 18 2020 at 09:09):

I have found `#check (@abs_le ℤ _)`

I don't know if there is anything closer.

#### Markus Himmel (Jul 18 2020 at 09:16):

It looks like this function does not exist yet. Here is one way to write it:

```
lemma lt_of_abs_lt {α : Type*} [decidable_linear_ordered_add_comm_group α] {x e : α} : abs x < e → x < e :=
λ h, (abs_lt.mp h).right
```

#### Scott Morrison (Jul 18 2020 at 09:19):

If you state the result you want as an `example`

`library_search`

is often successful. (You can use `library_search`

mid tactic block as well, but often it helps to state a cleaner version of the result you know you're after.)

#### Scott Morrison (Jul 18 2020 at 09:19):

There's also the `#find`

command, but it's unusually pretty unsatisfactory.

#### Scott Morrison (Jul 18 2020 at 09:20):

The other strategy is to know the name ahead of time -- Markus's suggestion is pretty good. Using ctrl+space completion with the correct prefix is often useful.

#### Kevin Buzzard (Jul 18 2020 at 09:25):

This function has unused inputs so will be rejected by the maths linter :-) `abs(x)<e -> x < e`

without any further assumptions.

#### Emiel Lanckriet (Jul 18 2020 at 09:35):

Kevin Buzzard said:

This function has unused inputs so will be rejected by the maths linter :-)

`abs(x)<e -> x < e`

without any further assumptions.

Ah, I see, thank you. I indeed made a mistake.

#### Emiel Lanckriet (Jul 18 2020 at 09:53):

Markus Himmel said:

It looks like this function does not exist yet. Here is one way to write it:

`lemma lt_of_abs_lt {α : Type*} [decidable_linear_ordered_add_comm_group α] {x e : α} : abs x < e → x < e := λ h, (abs_lt.mp h).right`

What does .mp mean in the solution? When I try it specifically for \R I get an error for this, I already found the solution in a slightly different way, but I was still wondering what .mp does.

#### Markus Himmel (Jul 18 2020 at 09:55):

`mp`

converts an if-and-only-if to an implication from the left to the right side

#### Markus Himmel (Jul 18 2020 at 09:56):

What error do you get? The following works for me:

```
import data.real.basic
lemma lt_of_abs_lt {x e : ℝ} : abs x < e → x < e :=
λ h, (abs_lt.mp h).right
```

#### Emiel Lanckriet (Jul 18 2020 at 09:57):

It is probably because I tried to use the command in begin-end-mode.

#### Markus Himmel (Jul 18 2020 at 09:58):

If you post your code, I can help you fix it

#### Emiel Lanckriet (Jul 18 2020 at 09:59):

The problem I had before is gone, so now it works, thanks a lot for your help. I don't what I did wrong the first time, but it is apparently not a problem anymore.

#### Scott Morrison (Jul 18 2020 at 10:00):

`mp`

is short for "modus ponens" if that helps you remember. (It doesn't help me. :-)

#### Kevin Buzzard (Jul 18 2020 at 10:28):

I like @Heather Macbeth 's take on it -- "iMPlies" :-)

#### Mario Carneiro (Jul 18 2020 at 17:27):

I find `.1`

and `.2`

easier to remember

Last updated: Dec 20 2023 at 11:08 UTC