tauto を追加する

Examples.lean

@@ -37,5 +37,6 @@ import Examples.Simp
 import Examples.Sorry
 import Examples.Split
 import Examples.Suffices
+import Examples.Tauto
 import Examples.Trivial
 import Examples.Wlog

Examples/Tauto.lean

@@ -0,0 +1,29 @@
+import Aesop
+import Mathlib.Tactic.LibrarySearch
+import Mathlib.Tactic.Tauto
+
+variable (P Q R : Prop)
+
+-- ANCHOR: first
+-- 含意の導入
+example (h : P) : Q → P := by
+  tauto
+
+-- フレーゲの3段論法
+example : (P → (Q → R)) → ((P → Q) → (P → R)) := by
+  tauto
+
+-- 排中律
+example : P ∨ ¬ P := by
+  -- `aesop` では示すことができない
+  try aesop
+
+  tauto
+
+-- 対偶
+example (h : P → Q) : ¬ Q → ¬ P := by
+  -- `exact?` では示すことができない
+  try exact?
+
+  tauto
+-- ANCHOR_END: first

src/SUMMARY.md

@@ -46,5 +46,6 @@
 - [sorry: 証明したことにする](./sorry.md)
 - [split: if 式を含む命題を示す](./split.md)
 - [suffices: 十分条件に帰着](./suffices.md)
+- [tauto: トートロジーを示す](./tauto.md)
 - [trivial: 自明](./trivial.md)
 - [wlog: 一般性を失わずに特殊化](./wlog.md)

src/tauto.md

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