tauto のコード例をそのまま実行できる形式に修正

Examples/Tauto.lean

@@ -1,10 +1,11 @@
 import Aesop
-import Mathlib.Tactic.LibrarySearch
-import Mathlib.Tactic.Tauto
+import Mathlib.Tactic.LibrarySearch -- `exact?` を使うため
+import Mathlib.Tactic.Tauto -- `tauto` を使うのに必要
 
 variable (P Q R : Prop)
 
--- ANCHOR: first
+/-! ## tauto -/
+
 -- 含意の導入
 example (h : P) : Q → P := by
   tauto
@@ -13,17 +14,28 @@ example (h : P) : Q → P := by
 example : (P → (Q → R)) → ((P → Q) → (P → R)) := by
   tauto
 
+/-! ## aesop との比較 -/
+
+variable (α : Type) (S : α → Prop)
+
 -- 排中律
 example : P ∨ ¬ P := by
   -- `aesop` では示すことができない
   try aesop
 
   tauto
 
+example : ¬(∀ x, S x) → (∃ x, ¬ S x) := by
+  -- `tauto` では示せない
+  try tauto
+
+  aesop
+
+/-! ## exact? との比較 -/
+
 -- 対偶
 example (h : P → Q) : ¬ Q → ¬ P := by
   -- `exact?` では示すことができない
   try exact?
 
   tauto
--- ANCHOR_END: first

src/tauto.md

@@ -1,11 +1,9 @@
 # tauto
 
-needs: `import Mathlib.Tactic.Tauto`
-
 named after: トートロジー(tautology)
 
 `tauto` は， トートロジー(恒真式)であることに基づいてゴールを閉じるタクティクです． ゴールを閉じることができなければエラーになります．
 
 ```lean
-{{#include ../Examples/Tauto.lean:first}}
-```
+{{#include ../Examples/Tauto.lean}}
+```