## Stream: new members

### Topic: Linking / Using mathlib and tactics

#### Adeeb K (Apr 21 2020 at 00:33):

Hello everybody! I am pretty new to using Lean - I just installed via the extension on VScode a few weeks ago. I was collaborating with an instructor remotely, and I downloaded a file they had been editing. It used the linarith tactic (specifically unknown identifier 'linarith' ). However, I have been getting errors from its use, and it does not seem like I can import anything to make them go away. Is there anything I can do? Thank you!

#### Scott Morrison (Apr 21 2020 at 00:34):

import tactic

#### Bryan Gin-ge Chen (Apr 21 2020 at 00:35):

Installing via the extension won't get you everything you need to use mathlib. You should follow the instructions here for your OS and then proceed to the projects doc.

#### Scott Morrison (Apr 21 2020 at 00:35):

(If that doesn't work, can you tell us which installation instructions you followed?)

#### Adeeb K (Apr 21 2020 at 00:37):

@Scott Morrison unfortunately, import tactic is giving me this error: file 'tactic' not found in the LEAN_PATH
@Bryan Gin-ge Chen I followed installation for the supporting tools for macOS, but I didn't touch anything related to elan

#### Scott Morrison (Apr 21 2020 at 00:39):

Did you follow the "You're not done yet" link at the bottom of the macOS page?

#### Scott Morrison (Apr 21 2020 at 00:39):

From the sounds of it you didn't!

#### Scott Morrison (Apr 21 2020 at 00:40):

linarith, along with almost everything else, is in mathlib, not Lean itself, and you need to install it too.

#### Adeeb K (Apr 21 2020 at 00:41):

Ah, makes sense. I'll do that now and report back!

#### Adeeb K (Apr 21 2020 at 00:48):

It works! I have a few questions about the content of the thing I'm working on, but I'll make a new topic for that. Thank you both so much for all the help!

Last updated: May 12 2021 at 04:19 UTC