fix(tests/lean): tests

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;
         }
     }
 }

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 : ℕ,

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