chore: remove workarounds

src/Lean/Elab/Declaration.lean

@@ -226,7 +226,7 @@ fun stx => do
   let elemsNew := #[]
   let modified := false
   for elem in stx[1].getArgs do
-    match (← Lean.expandMacro? elem) with -- TODO: remove workaround
+    match (← expandMacro? elem) with
     | some elemNew => elemsNew := elemsNew.push elemNew; modified := true
     | none         => elemsNew := elemsNew.push elem
   if modified then

src/Lean/Elab/DefView.lean

@@ -131,8 +131,7 @@ else if declKind == `Lean.Parser.Command.«example» then
 else
   throwError "unexpected kind of definition"
 
-@[init] private def regTraceClasses_1 : IO Unit := do -- TODO: remove _1
-registerTraceClass `Elab.definition
+initialize registerTraceClass `Elab.definition
 
 end Command
 end Lean.Elab

src/Lean/Elab/Do.lean

@@ -1458,7 +1458,7 @@ partial def doSeqToCode : List Syntax → M CodeBlock
       else
         mkSeq term <$> doSeqToCode doElems
     else
-      match (← liftMacroM $ Lean.expandMacro? doElem) with -- TODO: remove Lean.
+      match (← liftMacroM $ expandMacro? doElem) with
       | some doElem => doSeqToCode (doElem::doElems)
       | none => throwError! "unexpected do-element\n{doElem}"
 

src/Lean/Elab/Syntax.lean

@@ -163,7 +163,7 @@ partial def toParserDescrAux : Syntax → ToParserDescrM Syntax
     let d₂ ← withoutLeftRec $ toParserDescrAux stx[2]
     `(ParserDescr.orelse $d₁ $d₂)
   else
-    let stxNew? ← liftM (liftMacroM (Lean.expandMacro? stx) : TermElabM _) -- TODO: Remove `Lean.` from `Lean.expandMacro?`
+    let stxNew? ← liftM (liftMacroM (expandMacro? stx) : TermElabM _)
     match stxNew? with
     | some stxNew => toParserDescrAux stxNew
     | none => throwErrorAt! stx "unexpected syntax kind of category `syntax`: {kind}"