diff --git a/src/Lean/Elab.lean b/src/Lean/Elab.lean
index 7b518d0b23..b56422ff40 100644
--- a/src/Lean/Elab.lean
+++ b/src/Lean/Elab.lean
@@ -24,6 +24,7 @@ import Lean.Elab.Inductive
 import Lean.Elab.Structure
 import Lean.Elab.Print
 import Lean.Elab.MutualDef
+import Lean.Elab.AuxDef
 import Lean.Elab.PreDefinition
 import Lean.Elab.Deriving
 import Lean.Elab.DeclarationRange
diff --git a/src/Lean/Elab/AuxDef.lean b/src/Lean/Elab/AuxDef.lean
new file mode 100644
index 0000000000..fd7cedc7e2
--- /dev/null
+++ b/src/Lean/Elab/AuxDef.lean
@@ -0,0 +1,32 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gabriel Ebner
+-/
+import Lean.Elab.Command
+
+namespace Lean.Elab.Command
+open Lean.Parser.Command
+open Lean.Parser.Term
+
+/--
+Declares an auxiliary definition with an automatically generated name.
+For example, `aux_def foo : Nat := 42` creates a definition
+with an internal, unused name based on the suggestion `foo`.
+-/
+scoped syntax (name := aux_def) docComment ? attributes ? "aux_def" ident+ ":" term ":=" term : command
+
+@[builtinCommandElab «aux_def»]
+def elabAuxDef : CommandElab
+  | `($[$doc?:docComment]? $[$attrs?:attributes]? aux_def $[$suggestion:ident]* : $ty := $body) => do
+    let id := suggestion.map (·.getId.eraseMacroScopes) |>.foldl (· ++ ·) Name.anonymous
+    let id := `_aux ++ (← getMainModule) ++ `_ ++ id
+    let id := String.intercalate "_" <| id.components.map (·.toString)
+    let ns ← getCurrNamespace
+    -- make sure we only add a single component so that scoped workes
+    let id ← mkAuxName (ns.mkStr id) 1
+    let id := id.replacePrefix ns Name.anonymous -- TODO: replace with def _root_.id
+    elabCommand <|
+      ← `($[$doc?:docComment]? $[$attrs?:attributes]?
+          def $(mkIdent id):ident : $ty := $body)
+  | _ => throwUnsupportedSyntax