Issue with imports

Stream: new members

[Siva Gollapalli]

image.png
Here I have a theorem and it's proof. Now in the right side the VS Code extension of LEAN isn't showing any errors, but when I try to run the command lean <filename> it says import error.
Can someone help me with this

[Ira Fesefeldt]

Prefer using lake to build your project via lake build <projectname>, not lean directly.

I believe, the error comes from executing lean from the wrong folder (you are in a subfolder, while vscode executes it from the root folder). But even if you didn't, there may appear import problems from not properly building your project.

[Sebastian Ullrich]

If you do want to run Lean on a single file of a project, use lake lean