Use obtain in tactic mode in Lean theorem prover -

how use hypothesis of shape

h : exists x, p x 

in tactic mode? in term mode use

obtain x hx, h, 

it's same syntax:

example (a : type) (p : × a) : := begin   obtain x y, p, x end 

you can of course re-enter tactic mode using begin...end after from.