Zulip Chat Archive

Stream: general

Topic: question about tutorial 09/0072


view this post on Zulip 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,

view this post on Zulip Jalex Stark (Jul 21 2020 at 19:11):

linarith can't see through let

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Jalex Stark (Jul 21 2020 at 19:13):

i just always use set instead of let

view this post on Zulip 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