lean - リーン定理証明器の戦術モードで取得を使用する

Question

形状の仮説をどのように使用するか

H : exists x, P x

戦術モード？用語モードでは、使用します

obtain x Hx, from H,

Answer 1

まったく同じ構文です。

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

begin...endもちろん、 afterを使用して戦術モードに再度入ることもできますfrom。