question about tutorial 09/0072

Stream: general

[Antoine Chambert-Loir]

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]

linarith can't see through let

[Jalex Stark]

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

[Chris Hughes]

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]

i just always use set instead of let

[Antoine Chambert-Loir]

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.