choose を使わない例を示す

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

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}}
+```