diff --git a/src/frontends/lean/old_elaborator.cpp b/src/frontends/lean/old_elaborator.cpp
index f0b74ca779..d61142caf6 100644
--- a/src/frontends/lean/old_elaborator.cpp
+++ b/src/frontends/lean/old_elaborator.cpp
@@ -1876,7 +1876,7 @@ void old_elaborator::display_unsolved_tactic_state(expr const & mvar, tactic_sta
         flycheck_error err(ios());
         if (!err.enabled() || save_error(pip(), pos)) {
             display_error_pos(out.get_stream(), out.get_options(), pip(), pos);
-            out << " " << fmt << "\ntactic state:\n" << ts.pp(ios().get_formatter_factory()) << endl;
+            out << " " << fmt << "\nstate:\n" << ts.pp(ios().get_formatter_factory()) << endl;
         }
     }
 }
diff --git a/tests/lean/ctx.lean.expected.out b/tests/lean/ctx.lean.expected.out
index bf632da29b..b573f2d7d1 100644
--- a/tests/lean/ctx.lean.expected.out
+++ b/tests/lean/ctx.lean.expected.out
@@ -1,4 +1,5 @@
 ctx.lean:3:0: error: don't know how to synthesize placeholder
+state:
 A : Type,
 B : Type,
 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 : ℕ,
diff --git a/tests/lean/tactic_failure.lean.expected.out b/tests/lean/tactic_failure.lean.expected.out
index 9c1b674dba..ae55b99fb7 100644
--- a/tests/lean/tactic_failure.lean.expected.out
+++ b/tests/lean/tactic_failure.lean.expected.out
@@ -1,4 +1,5 @@
 tactic_failure.lean:4:0: error: assumption tactic failed
+state:
 A : Type,
 B : Type,
 Hb : B