I could benefit from a half-hour "one-on-one"

Stream: new members

[Barry Burd]

Hello, I'm trying to learn about Theorem Proving in Lean. So far, I haven't been able to get any introductory examples to work in the Web interface. If someone helps me past a few hurdles, I can probably take it from there on my own. I'm in the New York City time zone.

[Isak Colboubrani]

We can address that issue directly in this chat. Could you provide an example of a code snippet you attempted in the web interface that did not work?

[Barry Burd]

import data.real.basic

example (n : N) : (1 : R) ≤ 1.5^n :=
begin
  have h : (1 : R) ≤ 1.5 := by norm_num,
  library search
end

I see a message saying "unknown package 'data'".

[Ruben Van de Velde]

That makes sense, because that's lean 3 code

[Barry Burd]

I assume that live.lean-lang.org runs Lean 4. How would this example look in Lean 4?

[Isak Colboubrani]

Check the latest version of "Theorem Proving in Lean 4": all examples should be in Lean 4.

[Mario Carneiro]

import Mathlib.Data.Real.Basic

example (n : ℕ) : (1 : ℝ) ≤ 1.5^n := by
  have h : (1 : ℝ) ≤ 1.5 := by norm_num
  exact?

[Barry Burd]

I just copied your code into Lean 4 Web. I still see the message "unknown package 'data'". How can I get the message to refresh?

[Mario Carneiro]

you also need import Mathlib.Tactic.NormNum for norm_num to work

[Isak Colboubrani]

Go to https://live.lean-lang.org/?283498273 where 283498273 is some random number.

[Mario Carneiro]

for me just pasting in something new seems to work

[Barry Burd]

We're making progress. Now I have the following:

import Mathlib.Data.Real.Basic
import Mathlib.Tactic.NormNum

example (n : ℕ) : (1 : ℝ) ≤ 1.5^n := by
  have h : (1 : ℝ) ≤ 1.5 := by norm_num
  exact one_le_pow_of_one_le h n

I'll examine this and return later with follow-up questions.
Thanks.