Mathematics in Lean 3.3. help with problem

Stream: new members

[lame_lexem]

Hi. I am completing chapter 3.3 and i am stuck at this question.

solution

example (x : ℝ) (h : ∀ ε > 0, x < ε) : x ≤ 0 := by
  apply le_of_not_gt
  intro h'
  linarith [h _ h'] -- this is unsolvable without clue
  -- how to do it without linarith??

As I understand h here is something like a function which is when give a Real positive number gives a proof what x is less than that number. But I don't know how to proceed with any of this, so I looked at the solutions and found use of linarith and _.

Can you help me make proof without use of linarith?

[Ralf Stephan]

The state that you have after the intro h' is the same as when you had said by_contra h', so you need to show a contradiction now. No idea if this is the right way, but hey, I'm a newb.

[lame_lexem]

Oh ok. :sweat_smile: I solved it the same way the previous ones were solved by obtaining the contra proof, and applying something from the mathlib.

solution

-- now works!
example (x : ℝ) (h : ∀ ε > 0, x < ε) : x ≤ 0 := by
    apply le_of_not_gt
    intro h'
    have: x < x:= h x h'
    apply (lt_self_iff_false x).mp this

But I am still a bit unsure about [h _ h'] syntax used in the linarith solution.
Is there a pice of docs i can read about it?

[Ted Hwa]

But I am still a bit unsure about [h _ h'] syntax used in the linarith solution.

When you write linarith [h _ h'] you are asking linarith to use the fact h _ h' in addition to all the other facts in the context. In this case, the _ is inferred as x so it would be equivalent to write [h x h'] (h x h' is the fact you used in the previous solution). When you write the _ , you are asking Lean to infer the missing parameter from the other parameters. Since h' is of type x > 0, and h is looking for a hypothesis of type ε > 0, the _ is inferred as x.

The _ is useful when you have a complicated expression. Imagine h' was (some complicated expression) > 0. Then you could write _ and Lean would infer the complicated expression, rather than forcing you to type it in.