Resolving goals containing existential quantifiers

Stream: general

[Andrew Helwer]

In the natural number game, the use keyword resolves goals which contain existential quantifiers by assigning a concrete value to the quantified variable. Using Lean by itself it looks like use isn't available; what do you do instead?

[Alastair Horn]

I might be wrong but I think what you're looking for is called existsi

[Scott Morrison]

Using Lean by itself is usually a bad idea. The tactic use is provided in mathlib, along with everything else.

[Kevin Buzzard]

use is a mathlib tactic. import tactic and you'll get it

[Andrew Helwer]

Thanks everyone!