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。