From 05f30e8152150d73407ff9c92c17839039342766 Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Wed, 1 Nov 2023 22:35:33 +0900
Subject: [PATCH] =?UTF-8?q?tauto=20=E3=81=AE=E3=82=B3=E3=83=BC=E3=83=89?=
 =?UTF-8?q?=E4=BE=8B=E3=82=92=E3=81=9D=E3=81=AE=E3=81=BE=E3=81=BE=E5=AE=9F?=
 =?UTF-8?q?=E8=A1=8C=E3=81=A7=E3=81=8D=E3=82=8B=E5=BD=A2=E5=BC=8F=E3=81=AB?=
 =?UTF-8?q?=E4=BF=AE=E6=AD=A3?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Examples/Tauto.lean | 20 ++++++++++++++++----
 src/tauto.md        |  6 ++----
 2 files changed, 18 insertions(+), 8 deletions(-)

diff --git a/Examples/Tauto.lean b/Examples/Tauto.lean
index 4be7d16e..58427abf 100644
--- a/Examples/Tauto.lean
+++ b/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,6 +14,10 @@ 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` では示すことができない
@@ -20,10 +25,17 @@ example : P ∨ ¬ P := by
 
   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
diff --git a/src/tauto.md b/src/tauto.md
index 79b8c4d2..0a9657fe 100644
--- a/src/tauto.md
+++ b/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}}
+```
\ No newline at end of file