Imperial College开发的Natural Number Game是一个好主意，对LEAN中的证明编写基础有很大帮助。在经历了大部分内容之后，仍然存在一个“额外”问题，我还无法弄清楚。下面是此问题的精简版本，可以将其放在一个空文件中，并可以在LEAN中独立运行。

open nat

lemma two_eq_succ_one : 2 = succ(1) := rfl
lemma one_eq_succ_zero : 1 = succ(0) := rfl

theorem add_squared (a b : ℕ) :
    (a + b) ^ (2 : ℕ) = a ^ (2 : ℕ) + b ^ (2 : ℕ) + (2 : ℕ) * a * b :=
begin
    rw two_eq_succ_one,rw pow_succ (a+b) 1,rw pow_one (a+b),rw mul_add (a+b) a b,rw add_mul a b a,rw add_mul a b b,rw ← mul_comm a b,-- uncomment the rw below to see it fails
    --rw ← add_assoc (a*b) (a*b) (b*b),end

rw策略在这里无法识别应替换的模式，尽管它的打印方式与目标中的显示方式完全相同。在线提供的解决方案并没有说明为什么会发生这种情况，而是使用ring策略来解决。但是，游戏的作者说，有一种解决方案仅使用rw。您能帮我了解这里的问题吗？此外，任何多余的代码或提示都将很棒！我从来没有参加过抽象的代数课程，尽管我喜欢游戏并学到了很多东西，但有些东西在这里我还是没能认出。