feat(init/meta/interactive): add from synonym for exact

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.

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
 

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