Unable to find Mathlib files

Stream: mathlib4

[Shivam Singh]

Sometimes while importing Mathlib, in the lean info view in VScode it shows that its unable to find Mathlib or Mathlib.Lean in search path entries "/Users/shivamsingh/.elan/toolchains/stable/lib/lean". Why does this happen?

[Kevin Buzzard]

Maybe because you didn't open the root directory of a correctly formatted lean project using VS Code's "open folder" functionality?