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: Sep 26 2023 at 11:01 UTC