使用获得的战术模式，精益定理证明

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 

通过from后使用begin...end当然，你可以重新进入战术模式。