From d2e5e63c2468b61dacfd56ad57fb8e246f33e132 Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Tue, 31 Dec 2024 19:16:12 +0900
Subject: [PATCH 1/2] =?UTF-8?q?`use`=20=E3=82=BF=E3=82=AF=E3=83=86?=
 =?UTF-8?q?=E3=82=A3=E3=82=AF=E3=82=92=E7=B4=B9=E4=BB=8B=E3=81=99=E3=82=8B?=
 =?UTF-8?q?=20Fixes=20#242?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 LeanByExample/Tactic/Exists.lean |  2 +-
 LeanByExample/Tactic/Use.lean    | 64 ++++++++++++++++++++++++++++++++
 booksrc/SUMMARY.md               |  1 +
 3 files changed, 66 insertions(+), 1 deletion(-)
 create mode 100644 LeanByExample/Tactic/Use.lean

diff --git a/LeanByExample/Tactic/Exists.lean b/LeanByExample/Tactic/Exists.lean
index a1e44c6b..002d0a40 100644
--- a/LeanByExample/Tactic/Exists.lean
+++ b/LeanByExample/Tactic/Exists.lean
@@ -2,7 +2,7 @@
 
 `exists` タクティクは、「～を満たす `x` が存在する」という命題を示すために、証拠になる `x` を具体的に示します。
 
-ゴールが `⊢ ∃ x, P x` のとき、`x : X` がローカルコンテキストにあれば、`exists x` によりゴールが `P x` に変わります。同時に、`P x` が自明な場合は証明が終了します。-/
+ゴールが `⊢ ∃ x, P x` のとき、`x : X` がローカルコンテキストにあれば、`exists x` によりゴールが `⊢ P x` に変わります。同時に、`P x` が自明な場合は証明が終了します。-/
 import Lean --#
 
 example : ∃ x : Nat, 3 * x + 1 = 7 := by
diff --git a/LeanByExample/Tactic/Use.lean b/LeanByExample/Tactic/Use.lean
new file mode 100644
index 00000000..6feae263
--- /dev/null
+++ b/LeanByExample/Tactic/Use.lean
@@ -0,0 +1,64 @@
+/- # use
+
+`use` タクティクは、「～を満たす `x` が存在する」という命題を示すために、証拠になる `x` を具体的に示します。
+
+ゴールが `⊢ ∃ x, P x` のとき、`x : X` がローカルコンテキストにあれば、`use x` によりゴールが `⊢ P x` に変わります。同時に、`P x` が自明な場合は証明が終了します。
+-/
+import Mathlib.Tactic.Use
+import Mathlib.Tactic.Linarith
+
+#guard_msgs (drop warning) in --#
+example {α : Type} (P : α → Prop) (x : α) : ∃ y, P y := by
+  use x
+  -- ゴールが `P x` に変わる
+  guard_target =ₛ P x
+
+  sorry
+
+/- ## exists との違い
+これだけの説明だと [`exists`](./Exists.md) タクティクと同じに見えますが、`use` タクティクには `exists` より優れている点があります。
+
+### discharger が指定できる
+`use` は、証拠を与えた後にゴールを閉じるために使うタクティク（`discharger` と呼ばれます）を指定することができます。
+-/
+
+example (x : Rat) (h : 3 * x + 6 > 6) : ∃ (y : Rat), y > 0 := by
+  exists x
+  linarith
+
+example (x : Rat) (h : 3 * x + 6 > 6) : ∃ (y : Rat), y > 0 := by
+  -- `discharger` として `linarith` を指定することができる
+  use (discharger := linarith) x
+
+/- ### Exists 以外の構造体にも使用できる
+`exists` は、ゴールの型が `Exists` であるという想定をしているため、フィールドの数が３以上であるような構造体に対して使うとエラーになります。
+-/
+
+/-- 例示のための構造体。フィールドの数が `Exists` より多い -/
+structure Foo where
+  x : Int
+  pos : x > 0
+  sq : x ^ 2 = 9
+
+/-- `Foo` の項を具体的に与える例 -/
+example : Foo := ⟨3, by simp, by simp⟩
+
+/--
+error: invalid constructor ⟨...⟩, insufficient number of arguments, constructs 'Foo.mk' has #3 explicit fields, but only #2 provided
+-/
+#guard_msgs in
+  example : Foo := by
+    exists 3
+
+/- しかし、`use` タクティクであれば対応することができます。 -/
+
+example : Foo := by
+  -- 最初のフィールドを `3` で埋めるように指示する
+  use 3
+
+  -- 残りのフィールドは `simp` で証明することができる
+  all_goals simp
+
+example : Foo := by
+  -- `discharger` を指定するバージョン
+  use (discharger := simp) 3
diff --git a/booksrc/SUMMARY.md b/booksrc/SUMMARY.md
index cdad4e84..34872969 100644
--- a/booksrc/SUMMARY.md
+++ b/booksrc/SUMMARY.md
@@ -196,6 +196,7 @@
   - [trivial: 基本的なタクティクを試す](./Tactic/Trivial.md)
   - [try: 失敗をエラーにしない](./Tactic/Try.md)
   - [unfold: 定義に展開](./Tactic/Unfold.md)
+  - [use: 存在∃を示す](./Tactic/Use.md)
   - [with_reducible: 透過度指定](./Tactic/WithReducible.md)
   - [wlog: 一般性を失わずに特殊化](./Tactic/Wlog.md)
   - [zify: 整数にキャストする](./Tactic/Zify.md)

From be8e033a7f7f2ce614f95671ac9732e0e2ce4fcd Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Tue, 31 Dec 2024 19:18:11 +0900
Subject: [PATCH 2/2] =?UTF-8?q?`exists`=20=E3=81=8B=E3=82=89=20`use`=20?=
 =?UTF-8?q?=E3=81=B8=E3=81=AE=E3=83=AA=E3=83=B3=E3=82=AF=E3=82=92=E5=BC=B5?=
 =?UTF-8?q?=E3=82=8B?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 LeanByExample/Tactic/Exists.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/LeanByExample/Tactic/Exists.lean b/LeanByExample/Tactic/Exists.lean
index 002d0a40..79e14f2b 100644
--- a/LeanByExample/Tactic/Exists.lean
+++ b/LeanByExample/Tactic/Exists.lean
@@ -8,6 +8,8 @@ import Lean --#
 example : ∃ x : Nat, 3 * x + 1 = 7 := by
   exists 2
 
+/- 上位互換にあたるタクティクに [`use`](./Use.md) タクティクがあります。 -/
+
 /- ## 舞台裏
 なお Lean での存在量化の定義は次のようになっています。-/
 --#--