choose 追加

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

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

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)

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