From 0fe4627860ec8bc851905bf600faafebc356e972 Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Tue, 17 Dec 2024 00:00:10 +0900
Subject: [PATCH] =?UTF-8?q?zify=20=E3=82=92=E7=B4=B9=E4=BB=8B=E3=81=99?=
 =?UTF-8?q?=E3=82=8B=20Fixes=20#1193?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 LeanByExample/Reference/Tactic/Zify.lean | 18 ++++++++++++++++++
 booksrc/SUMMARY.md                       |  1 +
 2 files changed, 19 insertions(+)
 create mode 100644 LeanByExample/Reference/Tactic/Zify.lean

diff --git a/LeanByExample/Reference/Tactic/Zify.lean b/LeanByExample/Reference/Tactic/Zify.lean
new file mode 100644
index 00000000..86433a61
--- /dev/null
+++ b/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
diff --git a/booksrc/SUMMARY.md b/booksrc/SUMMARY.md
index d948fa4b..b1b7ae05 100644
--- a/booksrc/SUMMARY.md
+++ b/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部: チュートリアル