having trouble with mathlib in windows

Stream: Lean for the curious mathematician 2020

[Eduardo Vianna]

I'm a Windows user and I installed lean using the instructions at https://leanprover-community.github.io/install/windows.html but still can't deal with anything that isn't basic lean.
For example, when I try to import something in Vscode using "import data.set data.int.basic data.set.function
import data.set.lattic" at the beginning of the code it tells me "file 'data\set' not found in the search path" and a bunch more of error messages. I'd like to use Lean on VsCode because it would help me to know what the functions do.

[Bryan Gin-ge Chen]

Have you created a Lean project as mentioned on the next page? https://leanprover-community.github.io/install/project.html

[Eduardo Vianna]

When I tried coding through a repository I cloned from a professor, it wan't working. But after creating a project like in this link it didn't have any problems with the import command, thanks!

[Bryan Gin-ge Chen]

If the repository is itself a Lean project that depends on mathlib, running leanproject get-mathlib-cache in that directory might get things working.