diff --git a/LeanByExample/Reference/Tactic/Aesop.lean b/LeanByExample/Reference/Tactic/Aesop.lean
index 5f1249c2..261dc0f6 100644
--- a/LeanByExample/Reference/Tactic/Aesop.lean
+++ b/LeanByExample/Reference/Tactic/Aesop.lean
@@ -3,8 +3,7 @@
 
 `aesop` は汎用的かつ強力な自動証明のためのタクティクです。
 
-Automated Extensible Search for Obvious Proofs (自明な証明の拡張可能な自動探索)からその名があります。様々なタクティクやルールを使用しながら最良優先探索を行い、ルーチンな証明を自動で終わらせます。
-
+Automated Extensible Search for Obvious Proofs (自明な証明の拡張可能な自動探索)からその名があります。様々なタクティクやルールを使用しながら最良優先探索を行い、証明を自動で終わらせようとします。
 -/
 import Aesop -- `aesop` を使用するため
 import Mathlib.Tactic.Says
@@ -22,6 +21,9 @@ example {f : X → Y} {g : Y → Z} (hgfinj : Injective (g ∘ f)) : Injective f
   rw [Injective]
   show ∀ ⦃a₁ a₂ : X⦄, f a₁ = f a₂ → a₁ = a₂
 
+  -- `simp_all` では示せない
+  fail_if_success simp_all
+
   -- 示すべきことがまだまだあるように見えるが、一発で証明が終わる
   aesop
 
@@ -38,7 +40,9 @@ example {f : X → Y} {g : Y → Z} (hgfinj : Injective (g ∘ f)) : Injective f
     apply hgfinj
     simp_all only [comp_apply]
 
-/- なお上記の例により、`aesop` が組み込みのルールとして `simp` 補題や `intro` タクティク等を使用することがわかります。-/
+/- なお上記の例により、`aesop` が実行の過程で `simp_all` タクティクや `intro` タクティク等を使用することがわかります。
+特に、`aesop` は `simp_all` の強化版であるということができます。
+実際には `aesop` は `simp_all` よりずっと多くの機能を持ちますが、固有の機能については [`add_aesop_rules`](#{root}/Reference/Declarative/AddAesopRules.md) のページを参照してください。-/
 
 /- ## カスタマイズ
 `aesop` はユーザがカスタマイズ可能です。補題やタクティクを登録することで、証明可能な命題を増やすことができます。