Lean.Elab.AuxDef
source
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.
aux_def foo : Nat := 42
foo