From 04689a2823f72f9c158668542427eebea92f1e58 Mon Sep 17 00:00:00 2001
From: Codex <codex@openai.com>
Date: Fri, 22 May 2026 10:15:34 +0900
Subject: [PATCH 1/3] Add symm tactic article

---
 LeanByExample/Tactic/README.lean |  1 +
 LeanByExample/Tactic/Symm.lean   | 78 ++++++++++++++++++++++++++++++++
 booksrc/SUMMARY.md               |  1 +
 3 files changed, 80 insertions(+)
 create mode 100644 LeanByExample/Tactic/Symm.lean

diff --git a/LeanByExample/Tactic/README.lean b/LeanByExample/Tactic/README.lean
index b6232f44..75b217a2 100644
--- a/LeanByExample/Tactic/README.lean
+++ b/LeanByExample/Tactic/README.lean
@@ -13,6 +13,7 @@ Lean で利用可能なタクティクは多岐にわたるので、ここによ
 |-----------|------|
 | [`rw`](./Rw.md) | `A = B` という等式を使って書き換えを行いたいとき |
 | [`rfl`](./Rfl.md) | `A = B` という等式を定義に展開することで示したいとき |
+| [`symm`](./Symm.md) | `A = B` などの対称な関係の向きを反転したいとき |
 | [`congr`](./Congr.md) | `f a = f b` を `a = b` に帰着して示したいとき |
 | [`calc`](./Calc.md) | 等式を連鎖させて `a = b` を示したいとき |
 
diff --git a/LeanByExample/Tactic/Symm.lean b/LeanByExample/Tactic/Symm.lean
new file mode 100644
index 00000000..769d78f9
--- /dev/null
+++ b/LeanByExample/Tactic/Symm.lean
@@ -0,0 +1,78 @@
+/- # symm
+
+`symm` は、等式や同値などの対称な関係の向きを反転するタクティクです。
+
+たとえばゴールが `b = a` であるとき、`symm` を実行するとゴールは `a = b` に変わります。-/
+
+variable {a b c : Nat}
+
+example (h : a = b) : b = a := by
+  symm
+
+  -- ゴールが反転する
+  guard_target =ₛ a = b
+
+  assumption
+
+/- ## 仮定を反転する
+
+`symm at h` と書くと、ローカルコンテキストにある仮定 `h` の向きを反転できます。-/
+
+example (h : a = b) (ha : a + c = 0) : b + c = 0 := by
+  symm at h
+
+  -- 仮定の向きが反転する
+  guard_hyp h : b = a
+
+  rw [h]
+  assumption
+
+/- ## 同値関係にも使える
+
+`symm` は等式だけではなく、命題の同値 `↔` にも使えます。-/
+
+example {P Q : Prop} (h : Q ↔ P) : P ↔ Q := by
+  symm
+
+  -- ゴールが反転する
+  guard_target =ₛ Q ↔ P
+
+  assumption
+
+example {P Q : Prop} (h : P ↔ Q) (hq : Q) : P := by
+  symm at h
+
+  -- 仮定の向きが反転する
+  guard_hyp h : Q ↔ P
+
+  rw [h] at hq
+  assumption
+
+/- ## カスタマイズ
+
+一般の二項関係で `symm` を使いたい場合は、その関係が対称であることを示す定理に `[symm]` 属性を付与します。-/
+
+/-- 2つの自然数の差が高々1であることを表す関係 -/
+def Close (x y : Nat) : Prop :=
+  x ≤ y + 1 ∧ y ≤ x + 1
+
+/-- `Close` は対称な関係 -/
+theorem Close.symm {x y : Nat} (h : Close x y) : Close y x := by
+  exact ⟨h.right, h.left⟩
+
+example {x y : Nat} (h : Close x y) : Close y x := by
+  -- 登録していないと `symm` は使用できない
+  fail_if_success symm
+
+  exact Close.symm h
+
+-- `Close` が対称であることを登録する
+attribute [symm] Close.symm
+
+example {x y : Nat} (h : Close x y) : Close y x := by
+  symm
+
+  -- `Close y x` が `Close x y` に反転する
+  guard_target =ₛ Close x y
+
+  assumption
diff --git a/booksrc/SUMMARY.md b/booksrc/SUMMARY.md
index 98cd8abf..b0944bfc 100644
--- a/booksrc/SUMMARY.md
+++ b/booksrc/SUMMARY.md
@@ -258,6 +258,7 @@
   - [sorry: 証明したことにする](./Tactic/Sorry.md)
   - [split: if/match 式を分解](./Tactic/Split.md)
   - [suffices: 十分条件に帰着](./Tactic/Suffices.md)
+  - [symm: 対称な関係の向きを反転する](./Tactic/Symm.md)
   - [tauto: トートロジーを示す](./Tactic/Tauto.md)
   - [trans: 推移律を利用する](./Tactic/Trans.md)
   - [trivial: 基本的なタクティクを試す](./Tactic/Trivial.md)

From 17c242a503094fcf9d04044ea12d71207e821790 Mon Sep 17 00:00:00 2001
From: Seasawher <47292598+Seasawher@users.noreply.github.com>
Date: Wed, 27 May 2026 01:57:43 +0900
Subject: [PATCH 2/3] =?UTF-8?q?=E3=82=BF=E3=82=AF=E3=83=86=E3=82=A3?=
 =?UTF-8?q?=E3=82=AF=E6=97=A9=E8=A6=8B=E8=A1=A8=E3=81=8B=E3=82=89=E5=89=8A?=
 =?UTF-8?q?=E9=99=A4=E3=81=99=E3=82=8B?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 LeanByExample/Tactic/README.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/LeanByExample/Tactic/README.lean b/LeanByExample/Tactic/README.lean
index 75b217a2..b6232f44 100644
--- a/LeanByExample/Tactic/README.lean
+++ b/LeanByExample/Tactic/README.lean
@@ -13,7 +13,6 @@ Lean で利用可能なタクティクは多岐にわたるので、ここによ
 |-----------|------|
 | [`rw`](./Rw.md) | `A = B` という等式を使って書き換えを行いたいとき |
 | [`rfl`](./Rfl.md) | `A = B` という等式を定義に展開することで示したいとき |
-| [`symm`](./Symm.md) | `A = B` などの対称な関係の向きを反転したいとき |
 | [`congr`](./Congr.md) | `f a = f b` を `a = b` に帰着して示したいとき |
 | [`calc`](./Calc.md) | 等式を連鎖させて `a = b` を示したいとき |
 

From d2619367419c385f1b1790fe92602fd06260a7b9 Mon Sep 17 00:00:00 2001
From: Seasawher <47292598+Seasawher@users.noreply.github.com>
Date: Wed, 27 May 2026 02:00:55 +0900
Subject: [PATCH 3/3] =?UTF-8?q?=E6=96=87=E7=AB=A0=E6=A0=A1=E6=AD=A3?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 LeanByExample/Tactic/Symm.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/LeanByExample/Tactic/Symm.lean b/LeanByExample/Tactic/Symm.lean
index 769d78f9..3f864215 100644
--- a/LeanByExample/Tactic/Symm.lean
+++ b/LeanByExample/Tactic/Symm.lean
@@ -1,6 +1,6 @@
 /- # symm
 
-`symm` は、等式や同値などの対称な関係の向きを反転するタクティクです。
+`symm` は、等式や同値性などの対称な関係の向きを反転するタクティクです。
 
 たとえばゴールが `b = a` であるとき、`symm` を実行するとゴールは `a = b` に変わります。-/
 
@@ -29,7 +29,7 @@ example (h : a = b) (ha : a + c = 0) : b + c = 0 := by
 
 /- ## 同値関係にも使える
 
-`symm` は等式だけではなく、命題の同値 `↔` にも使えます。-/
+`symm` は等式だけではなく、命題の同値性 `↔` にも使えます。-/
 
 example {P Q : Prop} (h : Q ↔ P) : P ↔ Q := by
   symm
@@ -50,7 +50,7 @@ example {P Q : Prop} (h : P ↔ Q) (hq : Q) : P := by
 
 /- ## カスタマイズ
 
-一般の二項関係で `symm` を使いたい場合は、その関係が対称であることを示す定理に `[symm]` 属性を付与します。-/
+一般の二項関係に対して `symm` を使いたい場合は、その関係が対称であることを示す定理に `[symm]` 属性を付与します。-/
 
 /-- 2つの自然数の差が高々1であることを表す関係 -/
 def Close (x y : Nat) : Prop :=