为什么在LEAN的二项式定理证明中联想的“重写”失败？

Question

[帝国理工学院开发的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。您能帮我了解这里的问题吗？此外，任何多余的代码或提示都将很棒！我从来没有参加过抽象的代数课程，尽管我喜欢这款游戏并学到了很多东西，但有些东西在这里我还是不认识。

Answer 1

a * a + a * b + (a * b + b * b)实际上是(a * a + a * b) + (a * b + b * b)。如果首先使用rw add_assoc (a * a)，则rw ← add_assoc (a*b) (a*b) (b*b)将起作用。

当然，ring策略也将解决这样的目标。