From 3267506bf7c7313968450fde468339c3fd8199a0 Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Sun, 24 Sep 2023 15:16:31 +0900
Subject: [PATCH] =?UTF-8?q?convert=20=E8=BF=BD=E5=8A=A0?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Examples/Convert.lean | 18 ++++++++++++++++++
 src/SUMMARY.md        |  1 +
 src/convert.md        |  9 +++++++++
 3 files changed, 28 insertions(+)
 create mode 100644 Examples/Convert.lean
 create mode 100644 src/convert.md

diff --git a/Examples/Convert.lean b/Examples/Convert.lean
new file mode 100644
index 00000000..0fc14afb
--- /dev/null
+++ b/Examples/Convert.lean
@@ -0,0 +1,18 @@
+import Mathlib.Tactic.Convert
+
+variable (a b c: Nat)
+
+
+-- ANCHOR: first
+example (f : Nat → Nat) (h : f (a + b) = 0) (hc: a + b = c) : f (c) = 0 := by
+  -- `h` はゴールと等しくないので失敗する
+  try exact [h]
+
+  -- `h` とゴールの差分を新たなゴールにする
+  convert h
+
+  -- ゴールが `⊢ c = a + b` に変わっている
+  show c = a + b
+
+  rw [hc]
+-- ANCHOR_END: first
diff --git a/src/SUMMARY.md b/src/SUMMARY.md
index 353812a0..920790ed 100644
--- a/src/SUMMARY.md
+++ b/src/SUMMARY.md
@@ -16,6 +16,7 @@
 - [constructor: 論理積∧を示す](./constructor.md)
 - [contradiction: 矛盾](./contradiction.md)
 - [conv: 変換モードに入る](./conv.md)
+- [convert: 惜しい補題を使う](./convert.md)
 - [done: 証明終了を宣言](./done.md)
 - [exact: 証明を直接構成](./exact.md)
 - [exists: 存在∃を示す](./exists.md)
diff --git a/src/convert.md b/src/convert.md
new file mode 100644
index 00000000..75262d8f
--- /dev/null
+++ b/src/convert.md
@@ -0,0 +1,9 @@
+# convert
+
+needs: `import Mathlib.Tactic.Convert`
+
+ローカルコンテキストに現在のゴールに近いけれども等しくはない `h` があるとき，`exact h` としても失敗します．しかし `convert h` は成功する可能性があり，成功した場合は `h` とゴールの差分を新たなゴールとします．
+
+```lean
+{{#include ../Examples/Convert.lean:first}}
+```
\ No newline at end of file