Error import tactic

Stream: new members

[Gemma Crowe]

Hello! I'm very new to Lean and going through the YouTube videos from the workshop last year. Could I get some help? Please send to a different chat topic if I'm asking in the wrong place.

I've been going through the proof from https://www.youtube.com/watch?v=b59fpAJ8Mfs and my code comes up with an error when I add
import tactic.linarith

It's saying this is an invalid import command, any ideas why? Everything else works in the proof up to then.

Thanks!

[Anne Baanen]

Could you post a copy of your code (see also #backticks for tips on how to format it) and the complete error message?

[Anne Baanen]

And welcome to the Zulip chat, you're definitely asking in the right place here.

[Eric Rodriguez]

sometimes Lean gets confused, can you try the restart Lean command one time first?

[Gemma Crowe]

@Eric Rodriguez that worked! I just restarted it and it's all fine now, thanks! Does this happen a lot with Lean, that it gets confused?

[Eric Rodriguez]

yeah, I find that sometimes working with new files it does that, not sure why...