instantiating meta variales

Stream: new members

[Ken Roe]

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]

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

[Kenny Lau]

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

[Ken Roe]

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]

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

[Kevin Buzzard]

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]

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]

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

[Patrick Massot]

as explained by Kevin

[Patrick Massot]

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