import data.nat.basic gives an error

Stream: new members

[slwkB]

Hey, it will be my first question :) I'm going through exercises from https://leanprover.github.io/theorem_proving_in_lean/theorem_proving_in_lean.pdf . Exercise 4 from section 4.6 requires aforementioned import. But what I get is "invalid import: data.nat.basic could not resolve import: data.nat.basic". My version is:
Lean (version 3.24.0, commit 13007ebb4de6, Release)
It was installed with instruction from https://leanprover-community.github.io/install/macos.html (via curl). The question is what am I doing wrong, or what configurational step did I miss?

[Kevin Buzzard]

Is there not a URL in the error message which lists the standard mistakes beginners have made when imports don't work?

[slwkB]

There is indeed, but it was as another error not expanded in vs code infoview when I selected the line with import :see_no_evil:

[Bryan Gin-ge Chen]

You'll have to create a project that depends on mathlib in order to import data.nat.basic (and this should probably be mentioned explicitly in TPiL, cc: @Jeremy Avigad ). See the steps on the "Lean projects" page.

[Jeremy Avigad]

Good point. The "about Lean" section is really outdated. https://leanprover.github.io/theorem_proving_in_lean/introduction.html#about-lean
I think it would be helpful there to:

• mention mathlib
• explain that TPIL focuses on core aspects of Lean rather than mathlib
• point out that, nonetheless, parts of it rely on importing files from mathlib
• point to the Lean community web pages for information on installing Lean and setting up a mathlib project
• point to the Lean community web pages for documentation of mathlib.

Would that address this particular issue? Is there anything else that should go in that section?

[Bryan Gin-ge Chen]

That looks good to me, thanks!