metavars

Stream: general

[Reid Barton]

This is probably a confused question, but in a tactic, how do I create a metavariable that can potentially depend on other metavariables?

[Reid Barton]

oh, I made something that kind of works! Never mind

[Sebastien Gouezel]

I have a proof in which an exact takes avery long time. The reason, I guess, is that in the goal there is a metavar (or, more precisely, one can see the metavar if one uses pp.instantiate_mvars false, but otherwise the metavar is replaced by its value, so Lean knows exactly what it should be). Is there a command to instantiate the metavar, to see if it makes the proof faster?

(The metavar is coming from a convert. If it could clean up the mess for me, it would be even better!)