diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean
index 44fedc59a2..f482ecfedf 100644
--- a/src/Lean/Elab/Declaration.lean
+++ b/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
diff --git a/src/Lean/Elab/DefView.lean b/src/Lean/Elab/DefView.lean
index 359acccd68..017e73a43e 100644
--- a/src/Lean/Elab/DefView.lean
+++ b/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
diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean
index dfa349c143..d851971323 100644
--- a/src/Lean/Elab/Do.lean
+++ b/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}"
 
diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean
index 4df9673a1e..7525a0b92d 100644
--- a/src/Lean/Elab/Syntax.lean
+++ b/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}"