naming a metavariable

Stream: general

[Scott Morrison]

Say I have a goal P ?m_1, and a second goal nat. I want to work on the first goal for a while, deferring the actual choice of the nat for pedagogical reasons. In the interim, how do I make the goal look like P n instead of P ?m_1?

[Scott Morrison]

Surely there is some trick! I feel like I've done this in the past but can't for the life of me remember how.

[Scott Morrison]

In particular I want to refer to ?m_1 all through a calc proof. I can leave it as _, and unify them all afterwards, but that's dirty.

[Johan Commelin]

let n : _ := _, use n

[Scott Morrison]

I wonder if this should be defer n.

[Eric Wieser]

It would be neat if ?n were syntax for '_ but call the metavariable "n"'

[Eric Wieser]

So that you didn't need a separate tactic line to defer it