Nat.find

Stream: new members

[Matt Chen]

Hi, I am just starting on Lean4.
I was able to find 'Nat.find' in Mathlib/Init/Data/Nat/Lemmas.lean on github, but when I build my own project with mathlib in vscode the this file is totally different and does not contain Nat.find. I am wondering why are local files different from online mathlib.

Also, what is the smallest unit of import? Can I import only one theorem from another lean file?

[Julian Berman]

Can you share what your project's lakefile.lean contains?

[Eric Wieser]

Matt Chen said:

Also, what is the smallest unit of import? Can I import only one theorem from another lean file?

No, the smallest unit of import is a file and all its (transitive) dependencies

[Julian Berman]

Matt Chen said:

I was able to find 'Nat.find' in Mathlib/Init/Data/Nat/Lemmas.lean on github

I'm not sure if you were looking at an old revision, but it would seem at this point that Nat.find lives in Mathlib.Data.Nat.Find: https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/Nat/Find.lean

[Matt Chen]

oh I see. loogle is directing me to an older version on github.
i am able to to find Nat.Find in the local directory you provided!

Julian Berman said:

Matt Chen said:

I was able to find 'Nat.find' in Mathlib/Init/Data/Nat/Lemmas.lean on github

I'm not sure if you were looking at an old revision, but it would seem at this point that Nat.find lives in Mathlib.Data.Nat.Find: https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/Nat/Find.lean

Thanks a lot

[Julian Berman]

Great! You can also in the future try the "lazy way", which is to use import Mathlib, which imports everything, and then #check Nat.find, and if you jump to the definition it will show you where it lives.

[Julian Berman]

In theory you can then also put #min_imports at the bottom of the file and it will tell you the minimal imports you need -- but in practice that doesn't seem to work here in the web playground, so maybe I don't know how to use that myself, and someone else can teach us both what's needed for that.

[Matt Chen]

this is great!
as a beginner for lean, where can i learn more of these useful tips?

[Kevin Buzzard]

Ask questions in #new members :-)

[Notification Bot]

This topic was moved here from #lean4 > Nat.find by Eric Wieser.