convert 追加

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

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)

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