# Zulip Chat Archive

## Stream: general

### Topic: question about tutorial 09/0072

#### Antoine Chambert-Loir (Jul 21 2020 at 18:55):

Hello,

There's something I don't understand in tutorial/09, lemma 0072 is_sup_iff.

I need to prove `∀ n : ℕ, ∃ a ∈ A, x - 1/(n+1) < a`

, and after `intros n`

and a proof of `this: 1/(n+1 : ℝ) > 0`

which are given by the exercise file, I wanted to go on with `let y := x - 1/(n+1:ℝ), have : y < x by linarith[this], apply lt_sup h y, assumption`

.

This does not work, because `linarith`

doesn't find the proof of the inequality `y<x`

.

On the other hand, the given solution is shorter : `exact lt_sup h _ (by linarith)`

.

Why does it work and mine does not?

Thank you in advance,

#### Jalex Stark (Jul 21 2020 at 19:11):

`linarith`

can't see through `let`

#### Jalex Stark (Jul 21 2020 at 19:11):

in order for linarith to work here, there needs to be a proof of `y = x - 1/(n+1:\R)`

in context

#### Chris Hughes (Jul 21 2020 at 19:12):

I think there's a `set`

tactic that helps in this situation. I've never used it, but it will make the proof of `y = x - 1/(n+1:\R)`

for you.

#### Jalex Stark (Jul 21 2020 at 19:13):

i just always use `set`

instead of `let`

#### Antoine Chambert-Loir (Jul 22 2020 at 21:50):

Jalex Stark said:

i just always use

`set`

instead of`let`

It did not work with set either… anyway, it was time to go to the next exercise! Thank you.

Last updated: May 14 2021 at 00:42 UTC