rw 表达式 IN 表达式
rw expression IN expression
说，我需要：
rw ← nat.mul_one (d+d),
但是整个目标有多个(d+d)。我可以做类似的事情吗：
rw ← nat.mul_one (d+d) in (5+(d+d)),
使得(d+d)只在括号中的完整表达式为5+(d+d)匹配的地方被重写？
您可以了解 conv 模式 here, which enable you to do targetted rewriting, or you can use the nth_rewrite tactic documented here 的乐趣，您可以精确选择要更改的 d+d 模式。
您可以尝试 mathlib 的 nth_rewrite 或 rw 的可选 occs 参数。例如：
如果 ⊢ (d + d) + 5 * (d + d) + 2 * (d + d) = 8 * (d + d)，那么 nth_rewrite ←nat.mul_one (d + d) 1 应该工作，rw ←nat.mul_one (d + d) { occs := occurrences.pos [2]} 也应该工作（注意 nth_rewrite 是零索引而 rw 是 1 索引).
你也可以把 conv 搞得一团糟，但我不建议这样做； conv 适用于上述示例的是 conv { congr, congr, congr, skip, rw ←nat.mul_one (d + d) }.
说，我需要：
rw ← nat.mul_one (d+d),
但是整个目标有多个(d+d)。我可以做类似的事情吗：
rw ← nat.mul_one (d+d) in (5+(d+d)),
使得(d+d)只在括号中的完整表达式为5+(d+d)匹配的地方被重写？
您可以了解 conv 模式 here, which enable you to do targetted rewriting, or you can use the nth_rewrite tactic documented here 的乐趣，您可以精确选择要更改的 d+d 模式。
您可以尝试 mathlib 的 nth_rewrite 或 rw 的可选 occs 参数。例如：
如果 ⊢ (d + d) + 5 * (d + d) + 2 * (d + d) = 8 * (d + d)，那么 nth_rewrite ←nat.mul_one (d + d) 1 应该工作，rw ←nat.mul_one (d + d) { occs := occurrences.pos [2]} 也应该工作（注意 nth_rewrite 是零索引而 rw 是 1 索引).
你也可以把 conv 搞得一团糟，但我不建议这样做； conv 适用于上述示例的是 conv { congr, congr, congr, skip, rw ←nat.mul_one (d + d) }.