Merge pull request #1214 from lean-ja/Seasawher/issue1193

zify を紹介する

LeanByExample/Reference/Tactic/Zify.lean

@@ -0,0 +1,18 @@
+/- # zify
+
+`zify` タクティクは、自然数 `Nat` についての命題を整数 `Int` についての命題に変換します。
+-/
+import Mathlib.Tactic.Zify -- `zify` タクティクを使うのに必要
+import Mathlib.Tactic.GCongr
+
+example (x : Nat) (h : x ≥ 5) : 15 ≤ 3 * x := by
+  -- 仮定とゴールを整数の不等式に変換する
+  zify at h ⊢
+
+  -- 整数についての命題に変換した
+  guard_hyp h : x ≥ (5 : Int)
+  guard_target = (15 : Int) ≤ 3 * ↑x
+
+  calc
+    (15 : Int) = 3 * 5 := by rfl
+    _ ≤ 3 * ↑x := by gcongr; decide

booksrc/SUMMARY.md

@@ -195,6 +195,7 @@
   - [unfold: 定義に展開](./Reference/Tactic/Unfold.md)
   - [with_reducible: 透過度指定](./Reference/Tactic/WithReducible.md)
   - [wlog: 一般性を失わずに特殊化](./Reference/Tactic/Wlog.md)
+  - [zify: 整数にキャストする](./Reference/Tactic/Zify.md)
 
 # 第2部: チュートリアル