feat(frontends/lean/builtin_exprs): name hypothesis in suffices

closes #817

src/frontends/lean/builtin_exprs.cpp

@@ -529,10 +529,30 @@ static expr parse_show(parser & p, unsigned, expr const *, pos_info const & pos)
 
 static expr parse_suffices_to_show(parser & p, unsigned, expr const *, pos_info const & pos) {
     auto prop_pos = p.pos();
-    expr from  = p.parse_expr();
+    name id;
+    expr from;
+    if (p.curr_is_identifier()) {
+        id = p.get_name_val();
+        p.next();
+        if (p.curr_is_token(get_colon_tk())) {
+            p.next();
+            from = p.parse_expr();
+        } else {
+            expr left = p.id_to_expr(id, prop_pos);
+            id        = get_this_tk();
+            unsigned rbp = 0;
+            while (rbp < p.curr_expr_lbp()) {
+                left = p.parse_led(left);
+            }
+            from = left;
+        }
+    } else {
+        id    = get_this_tk();
+        from  = p.parse_expr();
+    }
     expr to    = p.save_pos(mk_expr_placeholder(), prop_pos);
     expr prop  = p.save_pos(mk_arrow(from, to), prop_pos);
-    expr local = p.save_pos(mk_local(get_this_tk(), from), prop_pos);
+    expr local = p.save_pos(mk_local(id, from), prop_pos);
     p.check_token_next(get_comma_tk(), "invalid 'suffices' declaration, ',' expected");
     expr body;
     {

tests/lean/run/817.lean

@@ -0,0 +1,10 @@
+variables A B : Prop
+premises (H₁ : A) (H₂ : A → B)
+
+example : B :=
+suffices A ∧ (A → B), from and.right this (and.left this),
+and.intro H₁ H₂
+
+example : B :=
+suffices H : A ∧ (A → B), from and.right H (and.left H),
+and.intro H₁ H₂