Instantiating an existential with a specific proof

Question

I'm currently trying to write a tactic that instantiates an existential quantifier using a term that can be generated easily (in this specific example, from tauto). My first attempt:

Ltac mytac :=
  match goal with
  | |- (exists (_ : ?X), _) => cut X; 
                             [ let t := fresh "t" in intro t ; exists t; firstorder 
                               | tauto ]
  end.

This tactic will work on a simple problem like

Lemma obv1(X : Set) : exists f : X -> X, f = f.
  mytac.
Qed.

However it won't work on a goal like

Lemma obv2(X : Set) : exists f : X -> X, forall x, f x = x.
  mytac. (* goal becomes t x = x for arbitrary t,x *)

Here I would like to use this tactic, trusting that the f which tauto finds will be just fun x => x, thus subbing in the specific proof (which should be the identity function) and not just the generic t from my current script. How might I go about writing such a tactic?

Answer 1

You can use eexists to introduce an existential variable, and let tauto instantiates it.

This give the following simple code.

Lemma obv2(X : Set) : exists f : X -> X, forall x, f x = x.
  eexists; tauto.
Qed.