mathlib tutorial 5: invalid import: tuto_lib

Stream: general

[Siyuan Yan]

this line has an error:

▶ 4:1-4:2: error:
invalid import: tuto_lib
could not resolve import: tuto_lib

is it because of an updated mathlib? How should I fix it?
@Johan Commelin you might be interested?

[Siyuan Yan]

ohh, it's a local file in the solution directory but not in the exercise directory.