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

---
 Examples.lean        |  1 +
 Examples/Choose.lean | 16 ++++++++++++++++
 src/SUMMARY.md       |  1 +
 src/choose.md        |  9 +++++++++
 4 files changed, 27 insertions(+)
 create mode 100644 Examples/Choose.lean
 create mode 100644 src/choose.md

diff --git a/Examples.lean b/Examples.lean
index 947244d9..a2520509 100644
--- a/Examples.lean
+++ b/Examples.lean
@@ -6,6 +6,7 @@ import Examples.By
 import Examples.ByCases
 import Examples.ByContra
 import Examples.Cases
+import Examples.Choose
 import Examples.Constructor
 import Examples.Contradiction
 import Examples.Convert
diff --git a/Examples/Choose.lean b/Examples/Choose.lean
new file mode 100644
index 00000000..d7f671d7
--- /dev/null
+++ b/Examples/Choose.lean
@@ -0,0 +1,16 @@
+import Mathlib.Tactic.Choose
+
+variable (X Y : Type)
+
+
+-- ANCHOR: first
+example (f : X → Y) (hf : ∀ y, ∃ x, f x = y) : ∃ g : Y → X, ∀ y, f (g y) = y := by
+  -- 写像 `g : Y → X` を構成する
+  choose g hg using hf
+
+  -- `g` が満たす条件がローカルコンテキストに追加される
+  guard_hyp g: Y → X
+  guard_hyp hg: ∀ (y : Y), f (g y) = y
+
+  exact ⟨g, hg⟩
+-- ANCHOR_END: first
diff --git a/src/SUMMARY.md b/src/SUMMARY.md
index 920790ed..4d5feba4 100644
--- a/src/SUMMARY.md
+++ b/src/SUMMARY.md
@@ -13,6 +13,7 @@
 - [by: タクティクモードに入る](./by.md)
 - [calc: 計算モードに入る](./calc.md)
 - [cases: 論理和∨を使う](./cases.md)
+- [choose: ∀x∃yP(x,y)から写像を作る](./choose.md)
 - [constructor: 論理積∧を示す](./constructor.md)
 - [contradiction: 矛盾](./contradiction.md)
 - [conv: 変換モードに入る](./conv.md)
diff --git a/src/choose.md b/src/choose.md
new file mode 100644
index 00000000..350b61aa
--- /dev/null
+++ b/src/choose.md
@@ -0,0 +1,9 @@
+# choose
+
+needs: `import Mathlib.Tactic.Choose`
+
+`h : ∀ x, ∃ y, P(x, y)` が成り立っているときに，`choose f hf using h` は写像 `f: X → Y` と `f` が満たす性質 `hf : ∀ x, P(x, f x)` のペアを作ります．
+
+```lean
+{{#include ../Examples/Choose.lean:first}}
+```
\ No newline at end of file