diff --git a/Lean/Egg/Tests/Ambient MVar.lean b/Lean/Egg/Tests/Ambient MVar.lean
index c38dac0..cae1e79 100644
--- a/Lean/Egg/Tests/Ambient MVar.lean	
+++ b/Lean/Egg/Tests/Ambient MVar.lean	
@@ -1,7 +1,9 @@
 import Egg
 import Lean
 
-example (h : ∀ x : Prop, True = x) : True = True := by
+variable (h : ∀ x : Prop, True = x)
+
+example : True = True := by
   apply Eq.trans
   · egg [h]
   · rfl -- This assigns the mvar resulting from `Eq.trans`.
@@ -13,7 +15,7 @@ h : ∀ (x : Prop), True = x
 ⊢ Prop
 -/
 #guard_msgs in
-example (h : ∀ x : Prop, True = x) : True = True := by
+example : True = True := by
   apply Eq.trans
   · egg [h]
   · egg [h]
diff --git a/Lean/Egg/Tests/Basic.lean b/Lean/Egg/Tests/Basic.lean
index 4f8529d..ff88c33 100644
--- a/Lean/Egg/Tests/Basic.lean
+++ b/Lean/Egg/Tests/Basic.lean
@@ -1,18 +1,23 @@
 import Egg
 
-example : True := by
-  fail_if_success have : true = false := by egg
-  constructor
+/-- error: egg failed to prove goal -/
+#guard_msgs in
+example : true = false := by
+  egg
 
+/--
+error: expected goal to be of type '=' or '↔', but found:
+True
+-/
+#guard_msgs in
 example : True := by
-  fail_if_success have : True := by egg
-  constructor
+  egg
 
-example : True := by
-  fail_if_success have : true = true := by egg [true]
-  constructor
+/-- error: egg requires arguments to be theorems or definitions -/
+#guard_msgs in
+example : true = true := by
+  egg [true]
 
-set_option trace.egg true in
 example : 0 = 0 := by
   egg
 
diff --git a/Lean/Egg/Tests/BlockInvalidMatches.lean b/Lean/Egg/Tests/BlockInvalidMatches.lean
index c7fb2f8..edcd697 100644
--- a/Lean/Egg/Tests/BlockInvalidMatches.lean
+++ b/Lean/Egg/Tests/BlockInvalidMatches.lean
@@ -17,12 +17,11 @@ example : False := by
   contradiction
 
 -- This test covers Condition (2) of valid matches.
+/-- error: egg failed to prove goal -/
+#guard_msgs in
 set_option egg.blockInvalidMatches true in
-example : True := by
-  fail_if_success -- This fails because egg could not find a proof.
-    have : (fun x => (fun a => (fun a => a) a) 0) = (fun x => x) := by
-      egg (config := { exitPoint := some .beforeProof }) [thm]
-  constructor
+example : (fun x => (fun a => (fun a => a) a) 0) = (fun x => x) := by
+  egg (config := { exitPoint := some .beforeProof }) [thm₁]
 
 -- This theorem is only applicable in the backward direction.
 theorem thm₂ : ∀ x y : Nat, x = (fun _ => x) y :=
@@ -30,7 +29,7 @@ theorem thm₂ : ∀ x y : Nat, x = (fun _ => x) y :=
 
 -- This test covers Condition (1) of valid matches.
 set_option egg.blockInvalidMatches true in
-example : True := by
-  fail_if_success -- This fails because egg could not find a proof.
-    have : (fun x => x) = (fun _ : Nat => (fun x => x) 1) := by egg [thm₂]
-  constructor
+/-- error: egg failed to prove goal -/
+#guard_msgs in
+example : (fun x => x) = (fun _ : Nat => (fun x => x) 1) := by
+  egg [thm₂]
diff --git a/Lean/Egg/Tests/Eta.lean b/Lean/Egg/Tests/Eta.lean
index a8e11b4..2f0b5bc 100644
--- a/Lean/Egg/Tests/Eta.lean
+++ b/Lean/Egg/Tests/Eta.lean
@@ -5,9 +5,10 @@ set_option egg.genEtaRw true
 set_option egg.genBetaRw false
 
 set_option egg.genEtaRw false in
+/-- error: egg failed to prove goal -/
+#guard_msgs in
 example : (fun x => Nat.succ x) = Nat.succ := by
-  fail_if_success egg
-  rfl
+  egg
 
 example : (fun x => Nat.succ x) = Nat.succ := by
   egg
@@ -44,9 +45,10 @@ example : (eta 10 Nat.succ Nat) = Nat.succ := by
   egg
 
 set_option egg.genEtaRw false in
+/-- error: egg failed to prove goal -/
+#guard_msgs in
 example (a : Nat) (h : ∀ b : Nat, b.succ.add a = 0) : (10 |> fun x => Nat.succ x).add a = 0 := by
-  fail_if_success egg [h]
-  apply h
+  egg [h]
 
 example (a : Nat) (h : ∀ b : Nat, b.succ.add a = 0) : (10 |> fun x => Nat.succ x).add a = 0 := by
   egg [h]
diff --git a/Lean/Egg/Tests/NatLit.lean b/Lean/Egg/Tests/NatLit.lean
index 6a7e733..16ce886 100644
--- a/Lean/Egg/Tests/NatLit.lean
+++ b/Lean/Egg/Tests/NatLit.lean
@@ -68,9 +68,10 @@ example : 12345 % 0 = 12345 := by
   egg
 
 set_option egg.natReduceRws false in
+/-- error: egg failed to prove goal -/
+#guard_msgs in
 example (h : ∀ f : Nat → Nat, f (1 + 1) = x) : id 2 = x := by
-  fail_if_success egg [h]
-  apply h
+  egg [h]
 
 example (h : ∀ f : Nat → Nat, f (1 + 1) = x) : id 2 = x := by
   egg [h]
diff --git a/Lean/Egg/Tests/ShiftCapturedBVars.lean b/Lean/Egg/Tests/ShiftCapturedBVars.lean
index 62617a8..ac28af0 100644
--- a/Lean/Egg/Tests/ShiftCapturedBVars.lean
+++ b/Lean/Egg/Tests/ShiftCapturedBVars.lean
@@ -23,7 +23,7 @@ example : False := by
   contradiction
 
 set_option egg.shiftCapturedBVars true in
-example : True := by
-  fail_if_success -- This fails because egg could not find a proof.
-    have : (fun x => (x, 5).fst) = (fun _ : Nat => (fun x => x) 1) := by egg [thm₁]
-  constructor
+/-- error: egg failed to prove goal -/
+#guard_msgs in
+example : (fun x => (x, 5).fst) = (fun _ : Nat => (fun x => x) 1) := by
+  egg [thm₁]
diff --git a/Lean/Egg/Tests/Star.lean b/Lean/Egg/Tests/Star.lean
index 1a7774d..409b296 100644
--- a/Lean/Egg/Tests/Star.lean
+++ b/Lean/Egg/Tests/Star.lean
@@ -2,21 +2,25 @@ import Egg
 
 -- Tests for the `*` argument.
 
-example : True := by
-  fail_if_success have : true = false := by egg [*]
-  constructor
+/-- error: egg failed to prove goal -/
+#guard_msgs in
+example : true = false := by
+  egg [*]
 
+/-- error: egg failed to prove goal -/
+#guard_msgs in
 example (_ : true = true) : [true] ++ [] = [true] := by
-  fail_if_success egg [*]
-  rfl
+  egg [*]
 
+/-- error: duplicate '*' in arguments to egg -/
+#guard_msgs in
 example : 0 = 0 := by
-  fail_if_success egg [*, *]
-  rfl
+  egg [*, *]
 
+/-- error: duplicate '*' in arguments to egg -/
+#guard_msgs in
 example (h : 0 = 0) : 0 = 0 := by
-  fail_if_success egg [*, h, *]
-  rfl
+  egg [*, h, *]
 
 example : 0 = 0 := by
   egg [*]