import can't be found

Stream: new members

[Donna Jo]

Hello, why does the info window always show that the file for the package that is imported in a .lean file could not be found? Thanks a lot.

[Notification Bot]

A message was moved here from #general > Can't click on some mathlib3 docs by Eric Wieser.

[Kevin Buzzard]

Can you send a screenshot of VS Code (if you're talking about VS Code), with the file explorer open?