diff --git a/tests/lean/attribute_bug1.lean.expected.out b/tests/lean/attribute_bug1.lean.expected.out
index f04d7f7c8c..3a50dab17b 100644
--- a/tests/lean/attribute_bug1.lean.expected.out
+++ b/tests/lean/attribute_bug1.lean.expected.out
@@ -1,9 +1,9 @@
-attribute_bug1.lean:7:0: error: simplify tactic failed to simplify
+attribute_bug1.lean:7:3: error: simplify tactic failed to simplify
 state:
 n : ℕ
 ⊢ f n = n + 1
 constant fdef : ∀ (n : ℕ), f n = n + 1
-attribute_bug1.lean:19:0: error: simplify tactic failed to simplify
+attribute_bug1.lean:19:3: error: simplify tactic failed to simplify
 state:
 n : ℕ
 ⊢ f n = n + 1
diff --git a/tests/lean/by_contradiction.lean.expected.out b/tests/lean/by_contradiction.lean.expected.out
index 3a1e7b6104..bbbe8b0a40 100644
--- a/tests/lean/by_contradiction.lean.expected.out
+++ b/tests/lean/by_contradiction.lean.expected.out
@@ -8,7 +8,7 @@ a_1 : ¬¬a = b,
 H : ¬a = b
 ⊢ false
 -------
-by_contradiction.lean:22:0: error: tactic by_contradiction failed, target is not a negation nor a decidable proposition (remark: when 'local attribute classical.prop_decidable [instance]' is used all propositions are decidable)
+by_contradiction.lean:22:3: error: tactic by_contradiction failed, target is not a negation nor a decidable proposition (remark: when 'local attribute classical.prop_decidable [instance]' is used all propositions are decidable)
 state:
 p q : Prop,
 a : ¬¬p
diff --git a/tests/lean/ctx_error_msgs.lean.expected.out b/tests/lean/ctx_error_msgs.lean.expected.out
index cdd24d50fe..bba957dec5 100644
--- a/tests/lean/ctx_error_msgs.lean.expected.out
+++ b/tests/lean/ctx_error_msgs.lean.expected.out
@@ -1,4 +1,4 @@
-ctx_error_msgs.lean:4:0: error: infer type failed, function expected at
+ctx_error_msgs.lean:4:3: error: infer type failed, function expected at
   f a
 term
   f
@@ -7,16 +7,16 @@ has type
 state:
 f a : ℕ
 ⊢ true
-ctx_error_msgs.lean:11:0: error: infer type failed, unknown variable
+ctx_error_msgs.lean:11:3: error: infer type failed, unknown variable
   a
 state:
 ⊢ true
-ctx_error_msgs.lean:18:0: error: infer type failed, incorrect number of universe levels
+ctx_error_msgs.lean:18:3: error: infer type failed, incorrect number of universe levels
   eq
 state:
 a : ℕ
 ⊢ true
-ctx_error_msgs.lean:23:0: error: infer type failed, incorrect number of universe levels
+ctx_error_msgs.lean:23:3: error: infer type failed, incorrect number of universe levels
   eq.{0 0}
 state:
 a : ℕ
diff --git a/tests/lean/focus_tac.lean.expected.out b/tests/lean/focus_tac.lean.expected.out
index 7b9daf6e32..a25e3b95f7 100644
--- a/tests/lean/focus_tac.lean.expected.out
+++ b/tests/lean/focus_tac.lean.expected.out
@@ -8,7 +8,7 @@ x : ℕ := ?m_1
 --- inside focus tac ---
 a : ℕ
 ⊢ ℕ
-focus_tac.lean:4:0: error: focus tactic failed, focused goal has not been solved
+focus_tac.lean:4:3: error: focus tactic failed, focused goal has not been solved
 state:
 a : ℕ
 ⊢ ℕ
diff --git a/tests/lean/format_thunk1.lean.expected.out b/tests/lean/format_thunk1.lean.expected.out
index a7963f4f92..0c4bc5af1f 100644
--- a/tests/lean/format_thunk1.lean.expected.out
+++ b/tests/lean/format_thunk1.lean.expected.out
@@ -1,4 +1,4 @@
-format_thunk1.lean:4:0: error: invalid definev tactic, value has type
+format_thunk1.lean:4:3: error: invalid definev tactic, value has type
   ℕ
 but is expected to have type
   string
diff --git a/tests/lean/set_attr1.lean.expected.out b/tests/lean/set_attr1.lean.expected.out
index fcec2e3e40..a5e7ab33f3 100644
--- a/tests/lean/set_attr1.lean.expected.out
+++ b/tests/lean/set_attr1.lean.expected.out
@@ -1,4 +1,4 @@
-set_attr1.lean:14:0: error: tactic failed, there are unsolved goals
+set_attr1.lean:14:3: error: tactic failed, there are unsolved goals
 state:
 n : ℕ
 ⊢ f n = n + 1
diff --git a/tests/lean/subst_bug.lean.expected.out b/tests/lean/subst_bug.lean.expected.out
index 9cddcb88b9..e739c2e29a 100644
--- a/tests/lean/subst_bug.lean.expected.out
+++ b/tests/lean/subst_bug.lean.expected.out
@@ -1,4 +1,4 @@
-subst_bug.lean:4:0: error: tactic failed, there are unsolved goals
+subst_bug.lean:4:3: error: tactic failed, there are unsolved goals
 state:
 b2 : bool
 ⊢ ff && b2 = ff
diff --git a/tests/lean/tactic_failure.lean.expected.out b/tests/lean/tactic_failure.lean.expected.out
index c8c173b7cf..b9ea71e8c4 100644
--- a/tests/lean/tactic_failure.lean.expected.out
+++ b/tests/lean/tactic_failure.lean.expected.out
@@ -1,4 +1,4 @@
-tactic_failure.lean:4:0: error: assumption tactic failed
+tactic_failure.lean:4:3: error: assumption tactic failed
 state:
 A B : Type,
 Hb : B
diff --git a/tests/lean/unify_tac1.lean.expected.out b/tests/lean/unify_tac1.lean.expected.out
index c836c5b68e..197a97230d 100644
--- a/tests/lean/unify_tac1.lean.expected.out
+++ b/tests/lean/unify_tac1.lean.expected.out
@@ -1,4 +1,4 @@
-unify_tac1.lean:12:0: error: is_def_eq failed
+unify_tac1.lean:12:3: error: is_def_eq failed
 state:
 A : Type,
 a : A,