`grw` を紹介する

grw は、Mathlib.Tactic.rwSeq に定義されている戦術で、rw に似ていますが、= や ↔ 以外の関係（relation）でも書き換えができる点が異なります。

たとえば次のように使えます：

example (h₁ : a < b) (h₂ : b ≤ c) : a + d ≤ c + d := by
  grw [h₁, h₂]

この例では、< や ≤ といった関係をまたいで、grw が書き換えを行っています。

他にも：

example (h : a ≡ b [ZMOD n]) : a ^ 2 ≡ b ^ 2 [ZMOD n] := by
  grw [h]

ここでは合同式（≡）に対して書き換えています。

example : (h₁ : a ∣ b) (h₂ : c ∣ a * d) : a ∣ b * d := by
  grw [h₁]
  exact h₂

約数関係（∣）に対する書き換えも grw で可能です。

注意点

grw を使うには、関係に対応する補題（lemmas）が @[gcongr] という属性でタグ付けされている必要があります。また、関係が推移的（transitive）である必要がある場合には、IsTrans インスタンスを用意することでそれに対応できます。

要するに、grw は「等式だけでなく、いろんな関係に対して rw 的な書き換えを可能にする戦術」です。

-- ChatGPT で生成

Start with the grw tactic described as Mathlib.Tactic.rwSeq, and review the supplied examples for relations such as <, ≤, congruence, and divisibility. Check where tactic introductions are organized in the repository, then add a Japanese explanation covering the examples, @[gcongr] lemmas, and the IsTrans requirement.