diff --git a/tests/lean/revert_fail.lean.expected.out b/tests/lean/revert_fail.lean.expected.out
index a27c500602..6ac2c7c0d4 100644
--- a/tests/lean/revert_fail.lean.expected.out
+++ b/tests/lean/revert_fail.lean.expected.out
@@ -13,8 +13,12 @@ revert_fail.lean:6:0: error: failed to add declaration '14.0' to environment, va
 remark: set 'formatter.hide_full_terms' to false to see the complete term
   λ (A : Type) (n : nat) (v : …),
     ?M_1
-revert_fail.lean:11:2: error: tactic failed
+revert_fail.lean:11:2: error:invalid tactic, there are no goals to be solved
+proof state:
 no goals
+revert_fail.lean:12:0: error: don't know how to synthesize placeholder
+n : nat
+⊢ n = n
 revert_fail.lean:12:0: error: failed to add declaration '14.1' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
   λ (n : nat),
diff --git a/tests/lean/rewrite_fail.lean.expected.out b/tests/lean/rewrite_fail.lean.expected.out
index 0ffde02422..2ecd71ab47 100644
--- a/tests/lean/rewrite_fail.lean.expected.out
+++ b/tests/lean/rewrite_fail.lean.expected.out
@@ -15,8 +15,12 @@ rewrite_fail.lean:6:0: error: failed to add declaration '14.0' to environment, v
 remark: set 'formatter.hide_full_terms' to false to see the complete term
   λ (a b : ℕ) (Ha : …) (Hb : …),
     ?M_1
-rewrite_fail.lean:11:2: error: tactic failed
+rewrite_fail.lean:11:2: error:invalid tactic, there are no goals to be solved
+proof state:
 no goals
+rewrite_fail.lean:12:0: error: don't know how to synthesize placeholder
+a : ℕ
+⊢ a = a
 rewrite_fail.lean:12:0: error: failed to add declaration '14.1' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
   λ (a : ℕ),