Merge pull request #3 from lean-ja/add_nth_rewrite

nth_rewriteの記述追加

Examples/Rw.lean

@@ -1,3 +1,8 @@
+import Mathlib.Algebra.Group.Basic
+import Mathlib.Tactic.NthRewrite
+
+
+-- ANCHOR: rw
 example (a b c d e f : Nat) (h : a * b = c * d) (h' : e = f) : a * (b * e) = c * (d * f) := by
   rw [h']
 
@@ -7,3 +12,17 @@ example (a b c d e f : Nat) (h : a * b = c * d) (h' : e = f) : a * (b * e) = c *
 
   -- 結合法則を使う
   rw [Nat.mul_assoc]
+-- ANCHOR_END: rw
+
+-- ANCHOR: nth_rewrite
+-- `G` は群
+variable [Group G]
+
+example (a b : G) : a * b⁻¹ = 1 ↔ a = b := by
+  -- `one_mul: 1 * b = b` を使って `b` を `1 * b` に書き換える
+  -- `b` は2回出現するが，2番目だけ置き換える
+  nth_rewrite 2 [← one_mul b]
+
+  -- `mul_inv_eq_iff_eq_mul: a * b⁻¹ = c ↔ a = c * b` を使う
+  exact mul_inv_eq_iff_eq_mul
+-- ANCHOR_END: nth_rewrite

src/rw.md

@@ -14,5 +14,15 @@
 ゴールではなく，ローカルコンテキストにある `h: P` を書き換えたいときには `at` をつけて `rw [hPQ] at h` とします．すべての箇所で置き換えたいときは `rw [hPQ] at *` とします．
 
 ```lean
-{{#include ../Examples/Rw.lean}}
+{{#include ../Examples/Rw.lean:rw}}
+```
+
+## nth_rewrite
+
+needs: `import Mathlib.Tactic.NthRewrite`
+
+`rw` はマッチした項をすべて置き換えてしまいます．特定の項だけを書き換えたいとき，`nth_rewrite` が使用できます．対象の式中に現れる順番を1始まりで指定することで，項を指定します．指定された順番が式中の対象の項の数よりも多い場合はエラーになります．
+
+```lean
+{{#include ../Examples/Rw.lean:nth_rewrite}}
 ```