exists タクティクの説明のミスを修正

Author: Seasawher

LeanByExample/Tactic/Exists.lean

@@ -1,8 +1,8 @@
 /- # exists
 
-`exists` は、「～という `x` が存在する」という命題を示すために、「この `x` を使え」と指示するコマンドです。
+`exists` タクティクは、「～を満たす `x` が存在する」という命題を示すために、証拠になる `x` を具体的に示します。
 
-ゴールが `⊢ ∃ x, P x` のとき、`x: X` がローカルコンテキストにあれば、`exists x` によりゴールが `P x` に変わります。同時に、`P x` が自明な場合は証明が終了します。-/
+ゴールが `⊢ ∃ x, P x` のとき、`x : X` がローカルコンテキストにあれば、`exists x` によりゴールが `P x` に変わります。同時に、`P x` が自明な場合は証明が終了します。-/
 import Lean --#
 
 example : ∃ x : Nat, 3 * x + 1 = 7 := by