使用する方法私は戦術モードで</p> <pre><code>H : exists x, P x </code></pre> <p>形状の仮説を使用しないリーン定理証明に戦術モードで

Question

を得ますか？あなたはもちろんfrom後begin...endを使用して戦術モードを再入力することができます

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

：用語モードでは、私は

obtain x Hx, from H, 

Answer 1

イッツまったく同じ構文を使用します。