diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean
index 2a4c870b9e..f5f06fd4c0 100644
--- a/library/init/meta/interactive.lean
+++ b/library/init/meta/interactive.lean
@@ -258,6 +258,9 @@ meta def exacts : parse pexpr_list_or_texpr → tactic unit
 | [] := done
 | (t :: ts) := exact t >> exacts ts
 
+/-- A synonym for `exact` that allows writing `have/show ..., from ...` in tactic mode. -/
+meta def «from» := exact
+
 /--
 `revert h₁ ... hₙ` applies to any goal with hypotheses `h₁` ... `hₙ`.
 It moves the hypotheses and its dependencies to the goal target.
diff --git a/library/init/meta/smt/interactive.lean b/library/init/meta/smt/interactive.lean
index 917dfb4f0e..ed3aa26cf6 100644
--- a/library/init/meta/smt/interactive.lean
+++ b/library/init/meta/smt/interactive.lean
@@ -77,6 +77,8 @@ tactic.interactive.change q none (loc.ns [])
 meta def exact (q : parse texpr) : smt_tactic unit :=
 tactic.interactive.exact q
 
+meta def «from» := exact
+
 meta def «assume» (p : parse parse_binders) : smt_tactic unit :=
 tactic.interactive.assume p
 
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index b309a0a73f..3d3474e66f 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -1387,7 +1387,7 @@ expr parser::parse_notation(parse_table t, expr * left) {
         sstream msg;
         msg << "invalid expression";
         if (p != pos()) {
-            msg << "starting at " << p.first << ":" << p.second;
+            msg << " starting at " << p.first << ":" << p.second;
         }
         return parser_error_or_expr({msg, pos()});
     }