Introduce variable

Stream: new members

[leafGecko]

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]

simply have x: R, generates a goal R, which (I presume) is wanting me to prove that R has a member?

[Mario Carneiro]

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]

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

[Jake Levinson]

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]

@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]

*can't