diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean
index e79f54e7a7..7c297c4fec 100644
--- a/src/Lean/Elab/BuiltinNotation.lean
+++ b/src/Lean/Elab/BuiltinNotation.lean
@@ -43,23 +43,20 @@ open Meta
 
 @[builtinMacro Lean.Parser.Term.have] def expandHave : Macro := fun stx =>
   let stx := stx.setArg 4 (mkNullNode #[mkAtomFrom stx ";"]) -- HACK
+  let mkId (x? : Option Syntax) : Syntax :=
+    x?.getD <| mkIdentFrom stx `this
   match stx with
-  | `(have $type from $val; $body)              => let thisId := mkIdentFrom stx `this; `(let! $thisId : $type := $val; $body)
-  | `(have $type by $tac:tacticSeq; $body)      => `(have $type from by $tac:tacticSeq; $body)
-  | `(have $type := $val; $body)                => let thisId := mkIdentFrom stx `this; `(let! $thisId : $type := $val; $body)
-  | `(have $x : $type from $val; $body)         => `(let! $x:ident : $type := $val; $body)
-  | `(have $x : $type by $tac:tacticSeq; $body) => `(have $x : $type from by $tac:tacticSeq; $body)
-  | `(have $x : $type := $val; $body)           => `(let! $x:ident : $type := $val; $body)
-  | _                                           => Macro.throwUnsupported
+  | `(have $[$x :]? $type from $val $[;]? $body)              => let x := mkId x; `(let! $x : $type := $val; $body)
+  | `(have $[$x :]? $type := $val $[;]? $body)                => let x := mkId x; `(let! $x : $type := $val; $body)
+  | `(have $[$x :]? $type by $tac:tacticSeq $[;]? $body)      => `(have $[$x :]? $type from by $tac:tacticSeq; $body)
+  | _                                                         => Macro.throwUnsupported
 
 @[builtinMacro Lean.Parser.Term.suffices] def expandSuffices : Macro := fun stx =>
   let stx := stx.setArg 4 (mkNullNode #[mkAtomFrom stx ";"]) -- HACK
   match stx with
-  | `(suffices $type from $val; $body)              => `(have $type from $body; $val)
-  | `(suffices $type by $tac:tacticSeq; $body)      => `(have $type from $body; by $tac:tacticSeq)
-  | `(suffices $x : $type from $val; $body)         => `(have $x:ident : $type from $body; $val)
-  | `(suffices $x : $type by $tac:tacticSeq; $body) => `(have $x:ident : $type from $body; by $tac:tacticSeq)
-  | _                                           => Macro.throwUnsupported
+  | `(suffices $[$x :]? $type from $val $[;]? $body)         => `(have $[$x :]? $type from $body; $val)
+  | `(suffices $[$x :]? $type by $tac:tacticSeq $[;]? $body) => `(have $[$x :]? $type from $body; by $tac:tacticSeq)
+  | _                                                        => Macro.throwUnsupported
 
 private def elabParserMacroAux (prec : Syntax) (e : Syntax) : TermElabM Syntax := do
   let (some declName) ← getDeclName?
diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean
index 7abc1021e9..92dd3946e5 100644
--- a/src/Lean/Elab/Syntax.lean
+++ b/src/Lean/Elab/Syntax.lean
@@ -378,26 +378,23 @@ def elabNoKindMacroRulesAux (alts : Array Syntax) : CommandElabM Syntax := do
 
 @[builtinCommandElab «macro_rules»] def elabMacroRules : CommandElab :=
   adaptExpander fun stx => match stx with
-  | `(macro_rules $alts:matchAlt*)           => elabNoKindMacroRulesAux alts
-  | `(macro_rules | $alts:matchAlt*)         => elabNoKindMacroRulesAux alts
-  | `(macro_rules [$kind] $alts:matchAlt*)   => do elabMacroRulesAux ((← getCurrNamespace) ++ kind.getId) alts
-  | `(macro_rules [$kind] | $alts:matchAlt*) => do elabMacroRulesAux ((← getCurrNamespace) ++ kind.getId) alts
-  | _                                        => throwUnsupportedSyntax
+  | `(macro_rules $[|]? $alts:matchAlt*)         => elabNoKindMacroRulesAux alts
+  | `(macro_rules [$kind] $[|]? $alts:matchAlt*) => do elabMacroRulesAux ((← getCurrNamespace) ++ kind.getId) alts
+  | _                                            => throwUnsupportedSyntax
 
 -- TODO: cleanup after we have support for optional syntax at `match_syntax`
 @[builtinMacro Lean.Parser.Command.mixfix] def expandMixfix : Macro := fun stx =>
   withAttrKindGlobal stx fun stx =>
     match stx with
-    | `(infix:$prec $op => $f)   => `(infixl:$prec $op => $f)
-    | `(infixr:$prec $op => $f)  => `(notation:$prec lhs $op:strLit rhs:$prec => $f lhs rhs)
-    | `(infixl:$prec $op => $f)  =>  let prec1 : Syntax := quote (prec.toNat+1); `(notation:$prec lhs $op:strLit rhs:$prec1 => $f lhs rhs)
-    | `(prefix:$prec $op => $f)  => `(notation:$prec $op:strLit arg:$prec => $f arg)
-    | `(postfix:$prec $op => $f) => `(notation:$prec arg $op:strLit => $f arg)
-    | `(infix:$prec [$prio] $op => $f)   => `(infixl:$prec [$prio] $op => $f)
-    | `(infixr:$prec [$prio] $op => $f)  => `(notation:$prec [$prio] lhs $op:strLit rhs:$prec => $f lhs rhs)
-    | `(infixl:$prec [$prio] $op => $f)  =>  let prec1 : Syntax := quote (prec.toNat+1); `(notation:$prec [$prio] lhs $op:strLit rhs:$prec1 => $f lhs rhs)
-    | `(prefix:$prec [$prio] $op => $f)  => `(notation:$prec [$prio] $op:strLit arg:$prec => $f arg)
-    | `(postfix:$prec [$prio] $op => $f) => `(notation:$prec [$prio] arg $op:strLit => $f arg)
+    | `(infix $[: $prec]? $[[$prio]]? $op => $f)   => `(infixl $[: $prec]? $[[$prio]]? $op => $f)
+    | `(infixr $[: $prec]? $[[$prio]]? $op => $f)  => `(notation $[: $prec]? $[[$prio]]? lhs $op:strLit rhs $[: $prec]? => $f lhs rhs)
+    | `(infixl $[: $prec]? $[[$prio]]? $op => $f)  =>
+       let prec1 : Syntax := match (prec : Option Syntax) with
+         | some prec => quote (prec.toNat+1)
+         | none      => quote 0
+       `(notation $[: $prec]? $[[$prio]]? lhs $op:strLit rhs:$prec1 => $f lhs rhs)
+    | `(prefix $[: $prec]? $[[$prio]]? $op => $f)  => `(notation $[: $prec]? $[[$prio]]? $op:strLit arg $[: $prec]? => $f arg)
+    | `(postfix $[: $prec]? $[[$prio]]? $op => $f) => `(notation $[: $prec]? $[[$prio]]? arg $op:strLit => $f arg)
     | _ => Macro.throwUnsupported
 where
   -- set "global" `attrKind`, apply `f`, and restore `attrKind` to result
@@ -463,7 +460,10 @@ def mkSimpleDelab (vars : Array Syntax) (pat qrhs : Syntax) : OptionT CommandEla
        | _        => throw ())
 
 private def expandNotationAux (ref : Syntax)
-    (currNamespace : Name) (attrKind : AttributeKind) (prec? : Option Syntax) (prio : Nat) (items : Array Syntax) (rhs : Syntax) : CommandElabM Syntax := do
+    (currNamespace : Name) (attrKind : AttributeKind) (prec? : Option Syntax) (prio? : Option Syntax) (items : Array Syntax) (rhs : Syntax) : CommandElabM Syntax := do
+  let prio := match prio? with
+    | some prio => prio.isNatLit?.getD 0
+    | _         => 0
   -- build parser
   let syntaxParts ← items.mapM expandNotationItemIntoSyntaxItem
   let cat := mkIdentFrom ref `term
@@ -477,13 +477,10 @@ private def expandNotationAux (ref : Syntax)
      So, we must include current namespace when we create a pattern for the following `macro_rules` commands. -/
   let fullKind := currNamespace ++ kind
   let pat := Syntax.node fullKind patArgs
-  let stxDecl ← match prec?, attrKind with
-    | none,      AttributeKind.global => `(syntax [$(mkIdentFrom ref kind):ident, $(quote prio):numLit] $syntaxParts* : $cat)
-    | some prec, AttributeKind.global => `(syntax:$prec [$(mkIdentFrom ref kind):ident, $(quote prio):numLit] $syntaxParts* : $cat)
-    | none,      AttributeKind.scoped => `(scoped syntax [$(mkIdentFrom ref kind):ident, $(quote prio):numLit] $syntaxParts* : $cat)
-    | some prec, AttributeKind.scoped => `(scoped syntax:$prec [$(mkIdentFrom ref kind):ident, $(quote prio):numLit] $syntaxParts* : $cat)
-    | none,      AttributeKind.local  => `(local syntax [$(mkIdentFrom ref kind):ident, $(quote prio):numLit] $syntaxParts* : $cat)
-    | some prec, AttributeKind.local  => `(local syntax:$prec [$(mkIdentFrom ref kind):ident, $(quote prio):numLit] $syntaxParts* : $cat)
+  let stxDecl ← match attrKind with
+    | AttributeKind.global => `(syntax $[: $prec?]? [$(mkIdentFrom ref kind):ident, $(quote prio):numLit] $syntaxParts* : $cat)
+    | AttributeKind.scoped => `(scoped syntax $[: $prec? ]? [$(mkIdentFrom ref kind):ident, $(quote prio):numLit] $syntaxParts* : $cat)
+    | AttributeKind.local  => `(local syntax $[: $prec? ]? [$(mkIdentFrom ref kind):ident, $(quote prio):numLit] $syntaxParts* : $cat)
   let macroDecl ← `(macro_rules | `($pat) => `($qrhs))
   match (← mkSimpleDelab vars pat qrhs |>.run) with
   | some delabDecl => mkNullNode #[stxDecl, macroDecl, delabDecl]
@@ -495,10 +492,7 @@ private def expandNotationAux (ref : Syntax)
     let stx := stx.setArg 0 mkAttrKindGlobal
     let currNamespace ← getCurrNamespace
     match stx with
-    | `(notation:$prec $items* => $rhs)                => expandNotationAux stx currNamespace attrKind prec 0 items rhs
-    | `(notation $items:notationItem* => $rhs)         => expandNotationAux stx currNamespace attrKind none 0 items rhs
-    | `(notation:$prec [$prio] $items* => $rhs)        => expandNotationAux stx currNamespace attrKind prec (prio.isNatLit?.getD 0) items rhs
-    | `(notation [$prio] $items:notationItem* => $rhs) => expandNotationAux stx currNamespace attrKind none (prio.isNatLit?.getD 0) items rhs
+    | `(notation $[: $prec? ]? $[[ $prio? ]]? $items* => $rhs) => expandNotationAux stx currNamespace attrKind prec? prio? items rhs
     | _ => throwUnsupportedSyntax
 
 /- Convert `macro` argument into a `syntax` command item -/
diff --git a/tests/lean/run/suffices.lean b/tests/lean/run/suffices.lean
index bf17ccd3e8..fcf8d8c486 100644
--- a/tests/lean/run/suffices.lean
+++ b/tests/lean/run/suffices.lean
@@ -14,3 +14,13 @@ theorem ex3 (Ha : a) (Hab : a → b) (Hbc : b → c) : c := by
   suffices b by apply Hbc; assumption
   suffices a by apply Hab; assumption
   assumption
+
+theorem ex4 (Ha : a) (Hab : a → b) (Hbc : b → c) : c :=
+  suffices h1 : b from Hbc h1
+  suffices h2 : a from Hab h2
+  Ha
+
+theorem ex5 (Ha : a) (Hab : a → b) (Hbc : b → c) : c := by
+  suffices h1 : b by apply Hbc; assumption
+  suffices h2 : a by apply Hab; exact h2
+  assumption