diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean
index 050e6b41df..10c7ce4911 100644
--- a/src/Lean/Elab/BuiltinNotation.lean
+++ b/src/Lean/Elab/BuiltinNotation.lean
@@ -250,21 +250,21 @@ def expandCDot? (stx : Syntax) : MacroM (Option Syntax) := do
   - `(· + ·)`
   - `(f · a b)` -/
 private def elabCDot (stx : Syntax) (expectedType? : Option Expr) : TermElabM Expr := do
-  match (← liftMacroM $ expandCDot? stx) with
+  match (← liftMacroM <| expandCDot? stx) with
   | some stx' => withMacroExpansion stx stx' (elabTerm stx' expectedType?)
   | none      => elabTerm stx expectedType?
 
-@[builtinTermElab paren] def elabParen : TermElab := fun stx expectedType? =>
+@[builtinTermElab paren] def elabParen : TermElab := fun stx expectedType? => do
   match stx with
-  | `(())           => pure $ Lean.mkConst `Unit.unit
-  | `(($e : $type)) => do
+  | `(())           => return Lean.mkConst `Unit.unit
+  | `(($e : $type)) =>
     let type ← withSynthesize (mayPostpone := true) $ elabType type
     let e ← elabCDot e type
     ensureHasType type e
   | `(($e))         => elabCDot e expectedType?
-  | `(($e, $es,*))  => do
-    let pairs ← liftMacroM $ mkPairs (#[e] ++ es)
-    withMacroExpansion stx pairs (elabTerm pairs expectedType?)
+  | `(($e, $es,*))  =>
+    let pairs ← liftMacroM <| mkPairs (#[e] ++ es)
+    withMacroExpansion stx pairs (elabCDot pairs expectedType?)
   | _ => throwError "unexpected parentheses notation"
 
 @[builtinTermElab subst] def elabSubst : TermElab := fun stx expectedType? => do
diff --git a/tests/lean/cdotTuple.lean b/tests/lean/cdotTuple.lean
new file mode 100644
index 0000000000..e73f133087
--- /dev/null
+++ b/tests/lean/cdotTuple.lean
@@ -0,0 +1,11 @@
+#eval [1, 2, 3].map (·, 1)
+
+#eval (·, ·) 1 2
+
+#eval (., ., .) 1 2 3
+
+theorem ex1 : [1, 2, 3].map (·, 1) = [(1, 1), (2, 1), (3, 1)] :=
+  rfl
+
+theorem ex2 : (., .) 1 2 = (1, 2) :=
+  rfl
diff --git a/tests/lean/cdotTuple.lean.expected.out b/tests/lean/cdotTuple.lean.expected.out
new file mode 100644
index 0000000000..f6c65f23a8
--- /dev/null
+++ b/tests/lean/cdotTuple.lean.expected.out
@@ -0,0 +1,3 @@
+[(1, 1), (2, 1), (3, 1)]
+(1, 2)
+(1, 2, 3)