Lean Tutorial

Stream: new members

[James Arthur]

I am slightly confused on the Lean tutorial. I am at the following

import data.real.basic

example (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a + b :=
begin
  sorry
end

and can't seem to get anywhere.

Thanks, James

[Kevin Buzzard]

The tactic linarith will solve it, but if you want to find out the name of the function which will do it directly you can try library_search.

[Patrick Massot]

Kevin, this is fine when you're cheating in a speed-run against undergrads, but we're trying to teach something here.

[Patrick Massot]

James, you should try using le_add_of_nonneg_right

[Kevin Buzzard]

It was any%!