how to download tactic module

Stream: new members

[Shaun Modipane]

It seems like I'm unable to use the tactic instructions, E.g. use, refl, simp, on my visual studio. I am open to any suggestions!

[Chris B]

How did you install Lean, are you using mathlib, and what error messages are you getting?

[Shaun Modipane]

I've folded this YouTube video https://www.youtube.com/watch?v=y3GsHIe4wZ4&t=555s to the letter. the error message is "file 'tactic' not found in the search path Use 'lean --path' to see where lean is looking"

[Shaun Modipane]

nevermind, I've solved the problem. I just need to follow instructions. https://leanprover-community.github.io/install/project.html