From 17e76c0634d5992b8b55ed8316dd45924161a783 Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Sun, 24 Sep 2023 15:40:13 +0900
Subject: [PATCH] =?UTF-8?q?=E3=82=B3=E3=83=BC=E3=83=89=E4=BE=8B=E3=81=AB?=
 =?UTF-8?q?=E3=81=8A=E3=81=84=E3=81=A6=EF=BC=8C=E4=BB=AE=E5=AE=9A=E3=82=84?=
 =?UTF-8?q?=E3=82=B4=E3=83=BC=E3=83=AB=E3=81=AE=E7=8A=B6=E6=85=8B=E3=82=92?=
 =?UTF-8?q?=E3=82=BF=E3=82=AF=E3=83=86=E3=82=A3=E3=82=AF=E3=81=A7=E8=A3=9C?=
 =?UTF-8?q?=E8=B6=B3=E3=81=99=E3=82=8B?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Examples/Apply.lean    | 4 +++-
 Examples/ByCases.lean  | 8 +++++++-
 Examples/ByContra.lean | 3 ++-
 Examples/Intro.lean    | 9 +++++++++
 4 files changed, 21 insertions(+), 3 deletions(-)

diff --git a/Examples/Apply.lean b/Examples/Apply.lean
index 0b18c218..392a8cde 100644
--- a/Examples/Apply.lean
+++ b/Examples/Apply.lean
@@ -1,9 +1,11 @@
 -- ANCHOR: first
 -- `P → Q` かつ `P` ならば `Q`
 example (h: P → Q) (hP: P) : Q := by
-  -- ゴールが `P` に変わる
   apply h
 
+  -- ゴールが `P` に変わっている
+  show P
+
   exact hP
 -- ANCHOR_END: first
 
diff --git a/Examples/ByCases.lean b/Examples/ByCases.lean
index 50db0772..e020b04a 100644
--- a/Examples/ByCases.lean
+++ b/Examples/ByCases.lean
@@ -1,3 +1,5 @@
+import Std.Tactic.GuardExpr
+
 -- ANCHOR: first
 example (P: Prop) : ¬¬P → P := by
   intro hnnP
@@ -7,9 +9,13 @@ example (P: Prop) : ¬¬P → P := by
 
   case inl =>
     -- `P` が成り立つとき
+    guard_hyp hP : P
+
     assumption
 
   case inr =>
-    -- `P` が成り立たないとき
+    -- `¬ P` が成り立つとき
+    guard_hyp hP : ¬P
+
     contradiction
 -- ANCHOR_END: first
\ No newline at end of file
diff --git a/Examples/ByContra.lean b/Examples/ByContra.lean
index e3023c50..ec34678c 100644
--- a/Examples/ByContra.lean
+++ b/Examples/ByContra.lean
@@ -6,8 +6,9 @@ example (h: ¬Q → ¬P) : P → Q := by
   -- `P` であると仮定する
   intro hP
 
-  -- `¬Q` であると仮定する
+  -- `¬Q` であると仮定して矛盾を導きたい
   by_contra hnQ
+  show False
 
   -- `¬ Q → ¬ P` と `¬Q` から `¬P` が導かれる
   have := h hnQ
diff --git a/Examples/Intro.lean b/Examples/Intro.lean
index f8885c87..f9f686d6 100644
--- a/Examples/Intro.lean
+++ b/Examples/Intro.lean
@@ -3,6 +3,9 @@ example (hPQ: P → Q) (hQR: Q → R) : P → R := by
   -- 示したいことが `P → R` なので，`P` だと仮定する
   intro hP
 
+  -- `R` を示したい
+  show R
+
   -- 仮定 `hPQ : P → Q` と `hP : P` から `Q` が導かれる
   have hQ : Q := hPQ hP
 
@@ -17,6 +20,9 @@ example (P Q : Nat → Prop) (h : ∀ n, P n ↔ Q n) : ∀ y, P (y + 1) → Q (
   -- そして `P (y + 1) → Q(y + 1)` を示したいので，`P (y + 1)` を仮定する
   intro y hyP
 
+  -- `Q (y + 1)` を示せば良い
+  show Q (y + 1)
+
   -- 同値を使ってゴールを書き換える
   rw [← h]
 
@@ -32,6 +38,9 @@ example (h: P → Q) : ¬Q → ¬P := by
   -- さらに `intro` を行って仮定 `hP : P` を導入する
   intro hnQ hP
 
+  -- 矛盾を示したい
+  show False
+
   -- `hP : P` と `h : P → Q` から `Q` が導かれる
   have hQ : Q := h hP