eexists as in Rocq

Stream: Is there code for X?

[Ka Wing Li]

Is there any tactic like eexists in Rocq?

[Jakub Nowak]

You mean choose?

[Ka Wing Li]

I tried existsi _ but throws "don't know how to synthesize placeholder for argument w"

[Ka Wing Li]

I would like a metavar to be generated and instantiated later.

[Henrik Böving]

apply Exists.intro

[Ka Wing Li]

Something like

theorem f {P : ℕ → Prop}  : P 0 → ∃ x, P x := by
  intro h
  apply Exists.intro _
  exact h

that I have to write apply Exists.intro _ everywhere

[Ruben Van de Velde]

use ?_, maybe

[Ka Wing Li]

Oh, I don't know about the trick of ?_. That is helpful!

[Kyle Miller]

The constructor tactic puts the goals in the order you're looking for.