diff --git a/tests/lean/1163.lean.expected.out b/tests/lean/1163.lean.expected.out
index babe41d425..2e3c5a1c10 100644
--- a/tests/lean/1163.lean.expected.out
+++ b/tests/lean/1163.lean.expected.out
@@ -1,2 +1,7 @@
 1163.lean:6:8-6:15: warning: declaration uses 'sorry'
 1163.lean:11:8-11:15: warning: declaration uses 'sorry'
+1163.lean:13:16-13:17: error: failed to synthesize instance
+  OfNat Bool 0
+1163.lean:15:8-15:15: warning: declaration uses 'sorry'
+1163.lean:18:18-18:19: error: failed to synthesize instance
+  OfNat Bool 0
diff --git a/tests/lean/301.lean.expected.out b/tests/lean/301.lean.expected.out
index fb73864610..89ffd24870 100644
--- a/tests/lean/301.lean.expected.out
+++ b/tests/lean/301.lean.expected.out
@@ -1,3 +1,4 @@
+301.lean:1:9-1:17: warning: declaration uses 'sorry'
 301.lean:1:9-1:17: error: missing cases:
 (Nat.succ _)
 301.lean:1:21-1:24: error: type mismatch
diff --git a/tests/lean/690.lean.expected.out b/tests/lean/690.lean.expected.out
index f1f79aa1b8..96436742c8 100644
--- a/tests/lean/690.lean.expected.out
+++ b/tests/lean/690.lean.expected.out
@@ -1,5 +1,4 @@
 690.lean:3:2-3:29: error: too many variable names provided at alternative 'step', #3 provided, but #2 expected
-690.lean:1:0-1:7: warning: declaration uses 'sorry'
 690.lean:6:0-6:7: warning: declaration uses 'sorry'
 case step
 a b m✝ : Nat
diff --git a/tests/lean/autoBoundImplicits1.lean.expected.out b/tests/lean/autoBoundImplicits1.lean.expected.out
index c7524ba123..3432f83ab4 100644
--- a/tests/lean/autoBoundImplicits1.lean.expected.out
+++ b/tests/lean/autoBoundImplicits1.lean.expected.out
@@ -2,14 +2,12 @@ myid 10 : Nat
 myid true : Bool
 autoBoundImplicits1.lean:16:4-16:11: warning: declaration uses 'sorry'
 autoBoundImplicits1.lean:20:25-20:29: error: unknown identifier 'size'
-autoBoundImplicits1.lean:20:4-20:12: warning: declaration uses 'sorry'
 autoBoundImplicits1.lean:24:23-24:24: error: unknown identifier 'α'
 autoBoundImplicits1.lean:24:25-24:26: error: unknown identifier 'n'
 autoBoundImplicits1.lean:24:33-24:34: error: unknown identifier 'α'
 autoBoundImplicits1.lean:24:37-24:38: error: unknown identifier 'β'
 autoBoundImplicits1.lean:24:46-24:47: error: unknown identifier 'β'
 autoBoundImplicits1.lean:24:48-24:49: error: unknown identifier 'n'
-autoBoundImplicits1.lean:24:4-24:12: warning: declaration uses 'sorry'
 @f : {α : Type} → {n : Nat} → Vec α n → Vec α n
 f mkVec : Vec ?m 0
 f mkVec : Vec Nat 0
diff --git a/tests/lean/bintreeGoal.lean.expected.out b/tests/lean/bintreeGoal.lean.expected.out
index 4742d593b9..931710e735 100644
--- a/tests/lean/bintreeGoal.lean.expected.out
+++ b/tests/lean/bintreeGoal.lean.expected.out
@@ -17,4 +17,3 @@ ihr : BST right → Tree.find? (Tree.insert right k v) k = some v
 : BST right
 : ForallTree (fun k v => key < k) right
 ⊢ BST left
-bintreeGoal.lean:60:8-60:27: warning: declaration uses 'sorry'
diff --git a/tests/lean/doLetLoop.lean.expected.out b/tests/lean/doLetLoop.lean.expected.out
index 167310acf4..d7d4ca5282 100644
--- a/tests/lean/doLetLoop.lean.expected.out
+++ b/tests/lean/doLetLoop.lean.expected.out
@@ -1 +1,2 @@
 doLetLoop.lean:4:0: error: unexpected end of input
+doLetLoop.lean:2:4-2:5: warning: declaration uses 'sorry'
diff --git a/tests/lean/doSeqRightIssue.lean.expected.out b/tests/lean/doSeqRightIssue.lean.expected.out
index 3fa59fec5a..405f86ef10 100644
--- a/tests/lean/doSeqRightIssue.lean.expected.out
+++ b/tests/lean/doSeqRightIssue.lean.expected.out
@@ -1 +1,3 @@
 doSeqRightIssue.lean:5:23-5:24: error: unknown universe level 'v'
+doSeqRightIssue.lean:8:0-9:40: warning: declaration uses 'sorry'
+doSeqRightIssue.lean:7:8-7:10: warning: declaration uses 'sorry'
diff --git a/tests/lean/inductionErrors.lean.expected.out b/tests/lean/inductionErrors.lean.expected.out
index b2d7a9c9c7..ffe26b71ac 100644
--- a/tests/lean/inductionErrors.lean.expected.out
+++ b/tests/lean/inductionErrors.lean.expected.out
@@ -28,6 +28,4 @@ inductionErrors.lean:55:2-55:16: error: alternative 'cons' is not needed
 inductionErrors.lean:60:2-60:40: error: invalid alternative name 'upper2'
 inductionErrors.lean:66:2-66:28: error: invalid occurrence of wildcard alternative, it must be the last alternative
 inductionErrors.lean:74:2-74:34: error: unused alternative
-inductionErrors.lean:69:8-69:12: warning: declaration uses 'sorry'
 inductionErrors.lean:80:2-80:53: error: unused alternative
-inductionErrors.lean:76:8-76:12: warning: declaration uses 'sorry'
diff --git a/tests/lean/matchErrorMsg.lean.expected.out b/tests/lean/matchErrorMsg.lean.expected.out
index c648dae646..8b7335959a 100644
--- a/tests/lean/matchErrorMsg.lean.expected.out
+++ b/tests/lean/matchErrorMsg.lean.expected.out
@@ -1,2 +1,3 @@
+matchErrorMsg.lean:2:1-4:16: warning: declaration uses 'sorry'
 matchErrorMsg.lean:2:1-2:6: error: missing cases:
 (Prod.mk Nat.zero (Nat.succ _))
diff --git a/tests/lean/matchMissingCasesAsStuckError.lean.expected.out b/tests/lean/matchMissingCasesAsStuckError.lean.expected.out
index 08f8c89841..4fd440fedc 100644
--- a/tests/lean/matchMissingCasesAsStuckError.lean.expected.out
+++ b/tests/lean/matchMissingCasesAsStuckError.lean.expected.out
@@ -1,2 +1,3 @@
+matchMissingCasesAsStuckError.lean:2:2-3:24: warning: declaration uses 'sorry'
 matchMissingCasesAsStuckError.lean:2:2-2:7: error: missing cases:
 none
diff --git a/tests/lean/matchUnknownFVarBug.lean.expected.out b/tests/lean/matchUnknownFVarBug.lean.expected.out
index cd7e2626a9..ebb11bf6e9 100644
--- a/tests/lean/matchUnknownFVarBug.lean.expected.out
+++ b/tests/lean/matchUnknownFVarBug.lean.expected.out
@@ -1,3 +1,4 @@
+matchUnknownFVarBug.lean:2:2-3:19: warning: declaration uses 'sorry'
 matchUnknownFVarBug.lean:2:2-2:7: error: missing cases:
 (some (Nat.succ _)), (some _)
 (some (Nat.succ _)), none
diff --git a/tests/lean/patvar.lean.expected.out b/tests/lean/patvar.lean.expected.out
index e3376f8187..63bedd8635 100644
--- a/tests/lean/patvar.lean.expected.out
+++ b/tests/lean/patvar.lean.expected.out
@@ -1,3 +1,4 @@
+patvar.lean:3:0-3:22: warning: declaration uses 'sorry'
 patvar.lean:3:0-3:22: error: missing cases:
 (List.cons _ _)
 patvar.lean:10:0-10:16: error: missing cases:
diff --git a/tests/lean/substBadMotive.lean.expected.out b/tests/lean/substBadMotive.lean.expected.out
index 1dddba6055..2b9f320e85 100644
--- a/tests/lean/substBadMotive.lean.expected.out
+++ b/tests/lean/substBadMotive.lean.expected.out
@@ -1,9 +1,4 @@
 substBadMotive.lean:7:4-7:16: warning: declaration uses 'sorry'
 substBadMotive.lean:9:23-9:44: error: invalid `▸` notation, failed to compute motive for the substitution
 substBadMotive.lean:15:22-15:43: error: invalid `▸` notation, failed to compute motive for the substitution
-substBadMotive.lean:13:4-13:15: warning: declaration uses 'sorry'
-substBadMotive.lean:13:4-13:15: warning: declaration uses 'sorry'
 substBadMotive.lean:34:30-34:53: error: invalid `▸` notation, failed to compute motive for the substitution
-substBadMotive.lean:21:4-21:15: warning: declaration uses 'sorry'
-substBadMotive.lean:21:4-21:15: warning: declaration uses 'sorry'
-substBadMotive.lean:21:4-21:15: warning: declaration uses 'sorry'
diff --git a/tests/lean/tooManyVarsAtInduction.lean.expected.out b/tests/lean/tooManyVarsAtInduction.lean.expected.out
index 1ae8b973f3..8a67c4411c 100644
--- a/tests/lean/tooManyVarsAtInduction.lean.expected.out
+++ b/tests/lean/tooManyVarsAtInduction.lean.expected.out
@@ -1,4 +1,2 @@
 tooManyVarsAtInduction.lean:3:2-3:31: error: too many variable names provided at alternative 'succ', #4 provided, but #2 expected
-tooManyVarsAtInduction.lean:1:8-1:11: warning: declaration uses 'sorry'
 tooManyVarsAtInduction.lean:8:2-8:22: error: too many variable names provided at alternative 'succ', #2 provided, but #1 expected
-tooManyVarsAtInduction.lean:6:8-6:11: warning: declaration uses 'sorry'