From 09f7921e4fe74cadcc4444ac2cb6ff033e9937f2 Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Sat, 31 Aug 2024 04:08:27 +0900
Subject: [PATCH] =?UTF-8?q?simp=20at=20*=20=E3=81=8C=E9=80=9A=E3=82=89?=
 =?UTF-8?q?=E3=81=9A=20simp=5Fall=20=E3=81=8C=E9=80=9A=E3=82=8B=E4=BE=8B?=
 =?UTF-8?q?=20Fixes=20#619?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Examples/Tactic/Simp.lean | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/Examples/Tactic/Simp.lean b/Examples/Tactic/Simp.lean
index 6961ca7c..04a9f9e3 100644
--- a/Examples/Tactic/Simp.lean
+++ b/Examples/Tactic/Simp.lean
@@ -123,6 +123,12 @@ example {x y : Nat} : 0 < 1 + x ∧ x + y + 2 ≥ y + 1 := by
   simp_arith
 
 /- ## simp_all
-`simp_all` は `simp [*] at *` の強化版で、ローカルコンテキストとゴールをこれ以上単純化できなくなるまですべて単純化します。-/
+`simp_all` はローカルコンテキストとゴールをこれ以上単純化できなくなるまですべて単純化します。-/
+
+example {P Q : Prop} (hP : P) (hQ : Q) : P ∧ (Q ∧ (P → Q)) := by
+  -- simp at * は失敗する
+  fail_if_success simp at *
+
+  simp_all
 
 end Simp --#