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] =?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 での存在量化の定義は次のようになっています。-/
 --#--