If I do something like
Goal exists n, n < 2. then
esplit., I get one goal with type
?n < 2. I can instantiate
?n up front by instead doing
split with (x:=1).. Is there a tactic that will leave me with two subgoals: one being
?n : nat and the other being accessible when I have instantiated
?n with some expression
n' via Ltac, with type
n' < 2? A proof could then look like:
Goal exists n, n < 2. esplit'. (* I'm asking what should go here. *) - exact 1. (* Or I could have a more complex tactic script producing `1`. *) - auto. (* Continue to prove `1 < 2`. *) Qed.
unshelve eexists (or unshelve esplit but generally people use eexists for this)
Thanks (and so quick)!
James Wood has marked this topic as resolved.
Last updated: Feb 08 2023 at 22:03 UTC