# Zulip Chat Archive

## Stream: new members

### Topic: Introduce variable

#### leafGecko (Sep 09 2021 at 20:54):

Hi all,

Is it possible that I introduce a new existential variable *inside the proof* when it does not appear inside the goal? Like a `(x: R)`

. Or is it strictly unnecessary ...

and can I introduce a theorem / lemma to environment so that `linarith`

can make use of it?

#### leafGecko (Sep 09 2021 at 20:54):

simply `have x: R`

, generates a goal `R`

, which (I presume) is wanting me to prove that `R `

has a member?

#### Mario Carneiro (Sep 09 2021 at 20:58):

You can use `have bla : x < 0 := ...`

to introduce an assertion `x < 0`

to the context, or `have bla : x < 0, { proof }`

which makes you prove the assertion by tactics in `proof`

#### Mario Carneiro (Sep 09 2021 at 20:58):

You can also add arguments to linarith, like `linarith [x_lt_zero]`

#### Jake Levinson (Sep 10 2021 at 04:36):

Be aware that if you want to introduce a *proposition* e.g. `h : x < 0`

, then `have h : x < 0 := { my_proof },`

is fine.

But if you want to introduce a value / piece of data, and need to remember what it is, e.g. `x := y+1`

, then you should use `set x := y+1 with hx`

, which will add `x : R := y+1`

and `hx : x = y + 1`

to the context, and you can then use `rw hx`

later on if needed (and `linarith`

should detect it in this case). By contrast if you write `have x := y+1`

then the context will only have `x : R`

and will not remember the value you defined x with.

#### Johan Commelin (Sep 10 2021 at 05:05):

@leafGecko If you have a proof of `nonempty X`

in your context, then you can extract from it a random `x : X`

. But otherwise you can just pull a `x : X`

out of nowhere, because `X`

might be empty.

#### Eric Wieser (Sep 10 2021 at 07:35):

*can't

Last updated: Dec 20 2023 at 11:08 UTC