使用獲得的戰術模式，精益定理證明

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當然，你可以重新進入戰術模式。