解决包含存在量词的目标

Question

在自然数游戏中，use关键字通过为量化变量分配具体值来解析包含存在量词的目标。单独使用Lean，看起来无法使用；你会怎么做？

Answer 1

您可以使用existsi，但通常建议避免单独使用精益；mathlib也应该始终使用。按照这里的文档设置你的项目，然后在.lean文件的顶部写import tactic，以访问use策略。