diff --git a/tests/lean/matchErrorLocation.lean.expected.out b/tests/lean/matchErrorLocation.lean.expected.out
index 7d9fb9f4b0..398a2c1ff8 100644
--- a/tests/lean/matchErrorLocation.lean.expected.out
+++ b/tests/lean/matchErrorLocation.lean.expected.out
@@ -2,7 +2,7 @@ matchErrorLocation.lean:5:10: error: type mismatch
   h he
 has type
   False
-but it is expected to have type
+but is expected to have type
   α
 failed to synthesize instance
   CoeT False (h he) α
diff --git a/tests/lean/server/diags.lean.expected.out b/tests/lean/server/diags.lean.expected.out
index 555894a201..543f5fa12d 100644
--- a/tests/lean/server/diags.lean.expected.out
+++ b/tests/lean/server/diags.lean.expected.out
@@ -1,7 +1,7 @@
 Content-Length: 221
 
-{"result":{"serverInfo":{"version":"0.0.1","name":"Lean 4 server"},"capabilities":{"textDocumentSync":{"willSaveWaitUntil":false,"willSave":false,"openClose":true,"change":2},"hoverProvider":true}},"jsonrpc":"2.0","id":0}Content-Length: 1020
+{"result":{"serverInfo":{"version":"0.0.1","name":"Lean 4 server"},"capabilities":{"textDocumentSync":{"willSaveWaitUntil":false,"willSave":false,"openClose":true,"change":2},"hoverProvider":true}},"jsonrpc":"2.0","id":0}Content-Length: 1017
 
-{"params":{"version":1,"uri":"file:///home/wojtek/Programming/C%2B%2B/lean4/src/Lean/Server/testDiags.txt","diagnostics":[{"source":"Lean 4 server","severity":3,"range":{"start":{"line":4,"character":0},"end":{"line":4,"character":0}},"message":"n : Nat"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":8,"character":0},"end":{"line":8,"character":0}},"message":"s : String"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":12,"character":0},"end":{"line":12,"character":0}},"message":"Hello world!\n"},{"source":"Lean 4 server","severity":1,"range":{"start":{"line":14,"character":31},"end":{"line":14,"character":31}},"message":"type mismatch\n  \"NotANat\"\nhas type\n  String\nbut it is expected to have type\n  Nat\nfailed to synthesize instance\n  CoeT String \"NotANat\" Nat"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":22,"character":0},"end":{"line":22,"character":0}},"message":"MyNs.u : Unit"}]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}Content-Length: 38
+{"params":{"version":1,"uri":"file:///home/wojtek/Programming/C%2B%2B/lean4/src/Lean/Server/testDiags.txt","diagnostics":[{"source":"Lean 4 server","severity":3,"range":{"start":{"line":4,"character":0},"end":{"line":4,"character":0}},"message":"n : Nat"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":8,"character":0},"end":{"line":8,"character":0}},"message":"s : String"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":12,"character":0},"end":{"line":12,"character":0}},"message":"Hello world!\n"},{"source":"Lean 4 server","severity":1,"range":{"start":{"line":14,"character":31},"end":{"line":14,"character":31}},"message":"type mismatch\n  \"NotANat\"\nhas type\n  String\nbut is expected to have type\n  Nat\nfailed to synthesize instance\n  CoeT String \"NotANat\" Nat"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":22,"character":0},"end":{"line":22,"character":0}},"message":"MyNs.u : Unit"}]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}Content-Length: 38
 
 {"result":null,"jsonrpc":"2.0","id":1}
diff --git a/tests/lean/server/edits.lean.expected.out b/tests/lean/server/edits.lean.expected.out
index d4961aec43..56efc9d8bc 100644
--- a/tests/lean/server/edits.lean.expected.out
+++ b/tests/lean/server/edits.lean.expected.out
@@ -1,8 +1,8 @@
 Content-Length: 221
 
-{"result":{"serverInfo":{"version":"0.0.1","name":"Lean 4 server"},"capabilities":{"textDocumentSync":{"willSaveWaitUntil":false,"willSave":false,"openClose":true,"change":2},"hoverProvider":true}},"jsonrpc":"2.0","id":0}Content-Length: 1020
+{"result":{"serverInfo":{"version":"0.0.1","name":"Lean 4 server"},"capabilities":{"textDocumentSync":{"willSaveWaitUntil":false,"willSave":false,"openClose":true,"change":2},"hoverProvider":true}},"jsonrpc":"2.0","id":0}Content-Length: 1017
 
-{"params":{"version":1,"uri":"file:///home/wojtek/Programming/C%2B%2B/lean4/src/Lean/Server/testDiags.txt","diagnostics":[{"source":"Lean 4 server","severity":3,"range":{"start":{"line":4,"character":0},"end":{"line":4,"character":0}},"message":"n : Nat"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":8,"character":0},"end":{"line":8,"character":0}},"message":"s : String"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":12,"character":0},"end":{"line":12,"character":0}},"message":"Hello world!\n"},{"source":"Lean 4 server","severity":1,"range":{"start":{"line":14,"character":31},"end":{"line":14,"character":31}},"message":"type mismatch\n  \"NotANat\"\nhas type\n  String\nbut it is expected to have type\n  Nat\nfailed to synthesize instance\n  CoeT String \"NotANat\" Nat"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":22,"character":0},"end":{"line":22,"character":0}},"message":"MyNs.u : Unit"}]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}Content-Length: 184
+{"params":{"version":1,"uri":"file:///home/wojtek/Programming/C%2B%2B/lean4/src/Lean/Server/testDiags.txt","diagnostics":[{"source":"Lean 4 server","severity":3,"range":{"start":{"line":4,"character":0},"end":{"line":4,"character":0}},"message":"n : Nat"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":8,"character":0},"end":{"line":8,"character":0}},"message":"s : String"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":12,"character":0},"end":{"line":12,"character":0}},"message":"Hello world!\n"},{"source":"Lean 4 server","severity":1,"range":{"start":{"line":14,"character":31},"end":{"line":14,"character":31}},"message":"type mismatch\n  \"NotANat\"\nhas type\n  String\nbut is expected to have type\n  Nat\nfailed to synthesize instance\n  CoeT String \"NotANat\" Nat"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":22,"character":0},"end":{"line":22,"character":0}},"message":"MyNs.u : Unit"}]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}Content-Length: 184
 
 {"params":{"version":1,"uri":"file:///home/wojtek/Programming/C%2B%2B/lean4/src/Lean/Server/testDiags.txt","diagnostics":[]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}Content-Length: 883
 
@@ -44,4 +44,4 @@ Content-Length: 221
 
 {"params":{"version":11,"uri":"file:///home/wojtek/Programming/C%2B%2B/lean4/src/Lean/Server/testDiags.txt","diagnostics":[{"source":"Lean 4 server","severity":3,"range":{"start":{"line":4,"character":0},"end":{"line":4,"character":0}},"message":"n : Nat"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":8,"character":0},"end":{"line":8,"character":0}},"message":"s : String"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":12,"character":0},"end":{"line":12,"character":0}},"message":"Hello world!\n"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":22,"character":0},"end":{"line":22,"character":0}},"message":"MyNs.u : Unit"}]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}Content-Length: 38
 
-{"result":null,"jsonrpc":"2.0","id":1}
+{"result":null,"jsonrpc":"2.0","id":1}
diff --git a/tests/lean/shadow.lean.expected.out b/tests/lean/shadow.lean.expected.out
index 6c63276508..d5cae92dbb 100644
--- a/tests/lean/shadow.lean.expected.out
+++ b/tests/lean/shadow.lean.expected.out
@@ -2,7 +2,7 @@ shadow.lean:6:0: error: type mismatch
   h
 has type
   x✝ = x✝
-but it is expected to have type
+but is expected to have type
   x = x
 failed to synthesize instance
   CoeT (x✝ = x✝) h (x = x)
@@ -10,7 +10,7 @@ shadow.lean:10:0: error: type mismatch
   h
 has type
   x = x
-but it is expected to have type
+but is expected to have type
   x = x
 failed to synthesize instance
   CoeT (x = x) h (x = x)
diff --git a/tests/lean/struct1.lean.expected.out b/tests/lean/struct1.lean.expected.out
index a49ab6694f..9ab7d5af83 100644
--- a/tests/lean/struct1.lean.expected.out
+++ b/tests/lean/struct1.lean.expected.out
@@ -10,7 +10,7 @@ struct1.lean:35:6: error: type mismatch
   true
 has type
   Bool
-but it is expected to have type
+but is expected to have type
   Nat
 failed to synthesize instance
   CoeT Bool true Nat
@@ -19,7 +19,7 @@ struct1.lean:41:12: error: type mismatch
   true
 has type
   Bool
-but it is expected to have type
+but is expected to have type
   Nat
 failed to synthesize instance
   CoeT Bool true Nat
diff --git a/tests/lean/typeMismatch.lean.expected.out b/tests/lean/typeMismatch.lean.expected.out
index f6c965a379..a73d8f455b 100644
--- a/tests/lean/typeMismatch.lean.expected.out
+++ b/tests/lean/typeMismatch.lean.expected.out
@@ -2,11 +2,11 @@ typeMismatch.lean:7:0: error: type mismatch
   IO.println ""
 has type
   EIO IO.Error Unit
-but it is expected to have type
+but is expected to have type
   IO Nat
 typeMismatch.lean:12:0: error: type mismatch
   Meta.isDefEq x x
 has type
   ReaderT Meta.Context (StateRefT Meta.State CoreM) Bool
-but it is expected to have type
+but is expected to have type
   MetaM Unit