Lean中使用rw重写命令时如何指定仅重写特定子表达式内的匹配项？

Lean rw 战术指定重写范围说明 #

你提到的语法是完全支持的：
rw 战术原生支持 in 子句来限定重写的作用范围，你写的 rw ← nat.mul_one (d+d) in (5+(d+d)), 确实只会在目标里的 5+(d+d) 子表达式内部寻找d+d的匹配项进行重写，不会修改目标中其他位置的d+d。

另外还有两种常用的精准重写技巧可以按需选用：

• 如果你不需要限定子表达式范围，只想重写第N个匹配到的目标项，可以用occs参数：

  -- 仅重写目标里第2处出现的(d+d)
  rw ← nat.mul_one (d+d) { occs := occurrences.pos [2] }
  

• 如果你需要在某条局部假设里限定范围重写，把in换成at加假设名即可：

  -- 仅在假设h里的5+(d+d)子表达式中重写
  rw ← nat.mul_one (d+d) in (5+(d+d)) at h
  

注意使用in子句时，后面跟的子表达式需要和目标/假设中的对应子表达式严格匹配，否则会出现找不到重写位置的报错。

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