diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 42220d53d0..3b24ca2d8d 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -399,7 +399,7 @@ void elaborator::validate_overloads(buffer<expr> const & fns, expr const & ref)
             format msg("invalid overloaded application, "
                        "elaborator has special support for '");
             msg += pp(fn_i);
-            msg += format(" (it is handled as an \"eliminator\"), "
+            msg += format("' (it is handled as an \"eliminator\"), "
                           "but this kind of constant cannot be overloaded "
                           "(solution: use fully qualified names) ");
             msg += pp_overloads(fns);
diff --git a/tests/lean/acc.lean.expected.out b/tests/lean/acc.lean.expected.out
index 8a07895d1d..f618989829 100644
--- a/tests/lean/acc.lean.expected.out
+++ b/tests/lean/acc.lean.expected.out
@@ -1,3 +1,2 @@
 acc.rec :
-  Π {A} {R} {C},
-    (Π x, (∀ y, R y x → acc A R y) → (Π y, R y x → C y) → C x) → (Π {a}, acc A R a → C a)
+  Π {A} {R} {C}, (Π x, (∀ y, R y x → acc A R y) → (Π y, R y x → C y) → C x) → (Π {a}, acc A R a → C a)
diff --git a/tests/lean/bug1.lean.expected.out b/tests/lean/bug1.lean.expected.out
index 9df9a7d849..8d0f42d086 100644
--- a/tests/lean/bug1.lean.expected.out
+++ b/tests/lean/bug1.lean.expected.out
@@ -1,19 +1,13 @@
 bug1.lean:9:7: error: type mismatch at definition 'and_intro1', has type
-  ∀ p q,
-    p → q → (∀ c, (p → q → c) → c)
+  ∀ p q, p → q → (∀ c, (p → q → c) → c)
 but is expected to have type
-  ∀ p q,
-    p → q → a
+  ∀ p q, p → q → a
 bug1.lean:13:7: error: type mismatch at definition 'and_intro2', has type
-  ∀ p q,
-    p → q → (∀ c, (p → q → c) → c)
+  ∀ p q, p → q → (∀ c, (p → q → c) → c)
 but is expected to have type
-  ∀ p q,
-    p → q → p ∧ p
+  ∀ p q, p → q → p ∧ p
 bug1.lean:17:7: error: type mismatch at definition 'and_intro3', has type
-  ∀ p q,
-    p → q → (∀ c, (p → q → c) → c)
+  ∀ p q, p → q → (∀ c, (p → q → c) → c)
 but is expected to have type
-  ∀ p q,
-    p → q → q ∧ p
+  ∀ p q, p → q → q ∧ p
 and_intro4 : ∀ p q, p → q → p ∧ q
diff --git a/tests/lean/defeq_simp2.lean.expected.out b/tests/lean/defeq_simp2.lean.expected.out
index 4af3519976..ba51b40230 100644
--- a/tests/lean/defeq_simp2.lean.expected.out
+++ b/tests/lean/defeq_simp2.lean.expected.out
@@ -1,5 +1,4 @@
 f a (foo1 a) = f a (foo2 a)
 f a (foo1 a) = f a (foo1 a)
 f a (foo2 a) = f a (foo2 a)
-(λ x, f x (id (id (id (foo1 x))))) = λ x,
-  f x (foo2 x)
+(λ x, f x (id (id (id (foo1 x))))) = λ x, f x (foo2 x)
diff --git a/tests/lean/error_pos_bug.lean.expected.out b/tests/lean/error_pos_bug.lean.expected.out
index 568be2869c..7f64326549 100644
--- a/tests/lean/error_pos_bug.lean.expected.out
+++ b/tests/lean/error_pos_bug.lean.expected.out
@@ -1,6 +1,5 @@
 error_pos_bug.lean:9:0: error: type error in placeholder assigned to
-  λ a b c,
-    a
+  λ a b c, a
 placeholder has type
   Category
 but is expected to have type
diff --git a/tests/lean/generalize1.lean.expected.out b/tests/lean/generalize1.lean.expected.out
index fbd0252a6b..f3a2a5562a 100644
--- a/tests/lean/generalize1.lean.expected.out
+++ b/tests/lean/generalize1.lean.expected.out
@@ -1,3 +1,2 @@
 a b c : ℕ
-⊢ ∀ (y x : ℕ),
-    x = y → y = x
+⊢ ∀ (y x : ℕ), x = y → y = x
diff --git a/tests/lean/let1.lean.expected.out b/tests/lean/let1.lean.expected.out
index 10554547fb..564328adbd 100644
--- a/tests/lean/let1.lean.expected.out
+++ b/tests/lean/let1.lean.expected.out
@@ -2,14 +2,10 @@ let bool := Prop,
     and := λ p q, Π c, (p → q → c) → c,
     and_intro := λ p q H1 H2 c H, H H1 H2
 in and_intro :
-  ∀ p q,
-    p → q → (∀ c, (p → q → c) → c)
+  ∀ p q, p → q → (∀ c, (p → q → c) → c)
 let1.lean:19:19: error: type mismatch at term
-  λ p q H1 H2 c H,
-    H H1 H2
+  λ p q H1 H2 c H, H H1 H2
 has type
-  ∀ p q,
-    p → q → (∀ c, (p → q → c) → c)
+  ∀ p q, p → q → (∀ c, (p → q → c) → c)
 but is expected to have type
-  ∀ p q,
-    p → q → (λ p q, ∀ c, (p → q → c) → c) q p
+  ∀ p q, p → q → (λ p q, ∀ c, (p → q → c) → c) q p
diff --git a/tests/lean/rev_tac1.lean.expected.out b/tests/lean/rev_tac1.lean.expected.out
index db345dfb1a..262ccf2490 100644
--- a/tests/lean/rev_tac1.lean.expected.out
+++ b/tests/lean/rev_tac1.lean.expected.out
@@ -1,5 +1,4 @@
 3
 b : ℕ,
 H : b > 0
-⊢ ∀ a,
-    a > 0 → a > b → a = b → true
+⊢ ∀ a, a > 0 → a > b → a = b → true