Lean证明器中rw策略何时自动完成证明？场景差异解析

我正在通过自然数游戏（Natural number game）学习Lean定理证明，目前对rw策略的行为逻辑存在疑问。

不同关卡的实际运行表现 #

• 在不等式世界第1关（共17关）中，我编写了如下代码：

use 1,
rw add_comm,

代码执行后Lean直接完成了证明，全程没有调用refl策略。

• 在不等式世界第2关（共17关）中，我编写了逻辑相似的代码：

use 0,
rw add_zero,

这段代码无法完成证明。我最初猜测调整为如下代码即可正常生效：

use 0,
symmetry,
rw add_zero,

但调整后的代码依然无法结束证明，这类场景下必须额外调用refl策略才能完成证明。

核心疑问 #

两类场景下rw策略的行为差异应当如何理解？

内容的提问来源于stack exchange，提问作者energy