Lean编程中重排引理：快速交换项匹配等式两侧的方法

针对你需要证明的目标：

Goal:
a ^ d * b ^ d * a * b = a ^ d * a * b ^ d * b

原始左侧带隐含括号为 ((a ^ d * b ^ d) * a )* b，不用反复调用mul_assoc和mul_comm的话，有几种更高效的方法：

• 组合rewrite规则一步调整
  直接在一次rw中链式调用所需的结合律和交换律规则，避免分步操作：

  rw [← mul_assoc (a^d * b^d), mul_comm (b^d) a, mul_assoc (a^d)]
  

  这里← mul_assoc先把外层括号调整为a^d * (b^d * a)，接着用mul_comm交换b^d和a，最后再次用mul_assoc把a^d * (a * b^d)合并为(a^d * a) * b^d，最终左侧结构就和右侧完全匹配。

• 使用ac_rfl策略
  如果你的目标只是基于乘法结合律和交换律的等式，ac_rfl可以直接完成证明——它会自动处理所有结合、交换的排列，不需要手动调整括号或交换项：

  ac_rfl
  

  这个策略专门针对这类"同表达式不同排列"的等式，是最快捷的选择之一。

• 利用ring策略（交换环场景）
  如果你的上下文中已经声明了变量所在的结构是交换环（比如variables {R : Type*} [comm_ring R]），直接用ring策略一步到位：

  ring
  

  ring会自动处理幂运算、乘法的结合/交换等所有环论规则，适合更复杂的代数等式证明。

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