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