lean

Use obtain in tactic mode in Lean theorem prover

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,
Solution

  • 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.