unknown identifier use

Stream: new members

[Martin Dvořák]

I am in the "script mode" and my current goal is ⊢ ∃ (x : ℕ), x.pred = 0.
When I write use int.one, as the next command, VS Code Lean Infoview tells me: unknown identifier 'use'.
Any idea why this could be happening?

[Martin Dvořák]

Do I need to import some library in order to have the command use available to me?

[Patrick Massot]

use is defined in mathlib

[Patrick Massot]

import tactic will be more than enough

[Martin Dvořák]

Oh, thanks! I didn't know it I had to import tactic. I incorrectly assumed that use was a keyword, not a tactic. My bad!

[Kevin Buzzard]

The "script mode" is tactic mode, everything you're writing there like use or apply is really running tactic.interactive.use or tactic.interactive.apply etc.

[Martin Dvořák]

Thank you!