From 4052c8a089b034715afcd582ccc7bb1306a4b1f7 Mon Sep 17 00:00:00 2001
From: aconite-ac <aconitefield@gmail.com>
Date: Tue, 3 Oct 2023 20:36:27 +0900
Subject: [PATCH 1/2] =?UTF-8?q?choose=20=E3=82=92=E4=BD=BF=E3=82=8F?=
 =?UTF-8?q?=E3=81=AA=E3=81=84=E4=BE=8B=E3=82=92=E7=A4=BA=E3=81=99?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Examples/Choose.lean | 21 +++++++++++++++++++++
 src/choose.md        |  8 ++++++++
 2 files changed, 29 insertions(+)

diff --git a/Examples/Choose.lean b/Examples/Choose.lean
index d7f671d7..d1027827 100644
--- a/Examples/Choose.lean
+++ b/Examples/Choose.lean
@@ -14,3 +14,24 @@ example (f : X → Y) (hf : ∀ y, ∃ x, f x = y) : ∃ g : Y → X, ∀ y, f (
 
   exact ⟨g, hg⟩
 -- ANCHOR_END: first
+
+
+-- ANCHOR: no_choose
+variable (P : X → Y → Prop)
+
+noncomputable example (h : ∀ x, ∃ y, P x y) : ∃ f : X → Y, ∀ x, P x (f x) := by
+  -- `f` を作る
+  let f' : (x : X) → {y // P x y} := fun x ↦
+    have hne_st : Nonempty {y // P x y} :=
+      let ⟨y, py⟩ := h x; ⟨⟨y, py⟩⟩
+    Classical.choice hne_st
+
+  let f : X → Y := fun x ↦ (f' x).val
+
+  -- 上記で作った関数が条件を満たすことを示す
+  have h₁ : ∀ x, P x (f x) := by
+    intro x
+    exact (f' x).property
+
+  exists f
+-- ANCHOR_END: no_choose
\ No newline at end of file
diff --git a/src/choose.md b/src/choose.md
index 350b61aa..5ad82ea7 100644
--- a/src/choose.md
+++ b/src/choose.md
@@ -6,4 +6,12 @@ needs: `import Mathlib.Tactic.Choose`
 
 ```lean
 {{#include ../Examples/Choose.lean:first}}
+```
+
+## 補足
+
+`choose` が自動で示してくれることは選択公理 `Classical.choice` を使って手動で示すことができます．たとえば次のようになります．
+
+```lean
+{{#include ../Examples/Choose.lean:no_choose}}
 ```
\ No newline at end of file

From 36890a6156d22513b78232dc7b164ce3fa181917 Mon Sep 17 00:00:00 2001
From: aconite-ac <aconitefield@gmail.com>
Date: Tue, 3 Oct 2023 20:37:34 +0900
Subject: [PATCH 2/2] =?UTF-8?q?``choose.md``=E5=86=85=E3=81=AE=E3=80=8C?=
 =?UTF-8?q?=E9=81=B8=E6=8A=9E=E5=85=AC=E7=90=86=E3=80=8D=E3=82=92=E3=80=8C?=
 =?UTF-8?q?=E9=81=B8=E6=8A=9E=E5=8E=9F=E7=90=86=E3=80=8D=E3=81=AB=E7=BD=AE?=
 =?UTF-8?q?=E6=8F=9B?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/choose.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/choose.md b/src/choose.md
index 5ad82ea7..1dc5bf5e 100644
--- a/src/choose.md
+++ b/src/choose.md
@@ -10,7 +10,7 @@ needs: `import Mathlib.Tactic.Choose`
 
 ## 補足
 
-`choose` が自動で示してくれることは選択公理 `Classical.choice` を使って手動で示すことができます．たとえば次のようになります．
+`choose` が自動で示してくれることは選択原理 `Classical.choice` を使って手動で示すことができます．たとえば次のようになります．
 
 ```lean
 {{#include ../Examples/Choose.lean:no_choose}}