## Stream: new members

### Topic: instantiating meta variales

#### Ken Roe (Jul 24 2018 at 19:06):

Is there a way to instantiate meta variables. Consider the theorem below:

theorem x: ∃ x, x=5 :=
begin existsi _, ..
end


What should the ... be replaced with? In this theorem, we could just change the existsi _ but in more complex theorems, meta variables seem to appear in many other places and it would be nice to instantiate them.

#### Kenny Lau (Jul 24 2018 at 19:07):

what information would you provide in order for the metavariables to be instantiated?

#### Kenny Lau (Jul 24 2018 at 19:07):

replacing .. with refl would prove the theorem, but I don't know if that is what you want

#### Ken Roe (Jul 24 2018 at 19:22):

refl is not what I want. In Coq, you can provide a value using instantiate (meta_var := value). Is there something similar in Lean?

#### Patrick Massot (Jul 24 2018 at 19:23):

Doesn't this meta variable appear as a new goal?

#### Kevin Buzzard (Jul 24 2018 at 19:38):

existsi 7 will instantiate the metavariable. If you use a hole _ then you get a new goal ⊢ ℕ as Patrick says. You can make this the first goal with show ℕ or swap and then instantiate it with exact 7.

#### Ken Roe (Jul 24 2018 at 19:48):

I've seen those new goals as holes--that is how to fill in the holes. Can swap be used beyond the second goal or is there something similar to switch for example the first and third goal?

#### Patrick Massot (Jul 24 2018 at 19:49):

https://github.com/leanprover/mathlib/blob/master/tactic/interactive.lean#L159

#### Patrick Massot (Jul 24 2018 at 19:49):

as explained by Kevin

#### Patrick Massot (Jul 24 2018 at 19:50):

You can also use show if you have only one goal of that type

Last updated: May 12 2021 at 04:19 UTC