nth_rewriteの記載追加

[s-taiga]

rwは書き換え可能な箇所をすべて書き換えるタクティックですが、これに対して式中で書き換え可能な箇所のうちn番目のみ書き換えるnth_rewriteというタクティックがあります。
https://leanprover-community.github.io/mathlib_docs/tactic/nth_rewrite/default.html
例えば以下のように用いることができます。
https://github.com/s-taiga/lean-math-workshop-my-solution/blob/d58278dc98ac95129c3ce7d7627dec70110dc2f4/Tutorial/Advanced/Algebra/Lecture1.lean#L262
個人的には先日の勉強会時にはかなりお世話になったタクティックだったので、言及があると良いのではないかと思います。

[Seasawher]

そうですね．conv モードで代替することもできますが，「すべて置き換える」挙動を制御するタクティクは必要ですね. ありがとうございます．

rw のページに派生タクティクとして紹介するのが良さそうに思います．

挙げてくださったコード例も簡潔で良いと思います．ただ依存関係がわからないので，minimal working example にして，適宜コメントもつけてもらえますか？

[Seasawher]

具体的には，こんな感じでどうでしょうか

import Mathlib.Algebra.Group.Basic
import Mathlib.Tactic.NthRewrite

-- `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

[Seasawher]

せっかくなので PR を出していただきたいです．

• ルールについては CONTRIBUTING.md を参照してください
• ビルド & ローカルプレビューは mdbook を用いて行っています
• rw にオプションがついているタクティクなので，rw.md に追記するのが良いと思います
• この issue の development の欄から作成した PR をリンクすることができます（オプション）