Use obtain in tactic mode in Lean theorem prover

Question

How do I use a hypothesis of the shape

H : exists x, P x

in tactic mode? In term mode I would use

obtain x Hx, from H,

Answer 1

It's exactly the same syntax:

example (A : Type) (p : A × A) : A :=
begin
  obtain x y, from p, x
end

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