How to use obtain in existential proofs?

I tried to prove an existential theorem

lemma "∃ x. x * (t :: nat) = t"
proof
  obtain y where "y * t = t" by (auto)

but I could not finish the proof. So I have the necessary y but how can I feed it into the original goal?

Solution

Soundness of natural deduction requires that you get hold of the witness before you open the existential quantifier. This is why you are not allowed to use obtained variables in show statements. In your example, the proof step implicitly applies the rule exI. This turns the existentially quantified variable x into the schematic variable ?x, which can be instantiated later, but the instantiation may only refer to variables that have been in scope when ?x came into place. In the low-level proof state, obtained variables are meta-quantified (!!) and the instantiations for ?x can only refer to such variables that appear as a parameter to ?x.

Therefore, you have to switch the order in your proof:

lemma "∃ x. x * (t :: nat) = t"
proof - (* method - does not change the goal *)
  obtain y where "y * t = t" by (auto)
  then show ?thesis by(rule exI)
qed