chore: duplicate

closes #3373

src/Lean/Elab/Binders.lean

@@ -782,6 +782,9 @@ def elabLetDeclCore (stx : Syntax) (expectedType? : Option Expr) (useLetExpr : B
 @[builtin_term_elab «let_tmp»] def elabLetTmpDecl : TermElab :=
   fun stx expectedType? => elabLetDeclCore stx expectedType? (useLetExpr := true) (elabBodyFirst := false) (usedLetOnly := true)
 
-builtin_initialize registerTraceClass `Elab.let
+builtin_initialize
+  registerTraceClass `Elab.let
+  registerTraceClass `Elab.let.decl
+  registerTraceClass `Elab.autoParam
 
 end Lean.Elab.Term

src/Lean/Elab/MutualDef.lean

@@ -993,5 +993,8 @@ def elabMutualDef (ds : Array Syntax) : CommandElabM Unit := do
       snap.new.resolve <| .ofTyped { defs, diagnostics := .empty : DefsParsedSnapshot }
     runTermElabM fun vars => Term.elabMutualDef vars views
 
+builtin_initialize
+  registerTraceClass `Elab.definition.mkClosure
+
 end Command
 end Lean.Elab

src/Lean/Elab/Quotation.lean

@@ -690,5 +690,6 @@ builtin_initialize
   registerTraceClass `Elab.match_syntax
   registerTraceClass `Elab.match_syntax.alt (inherited := true)
   registerTraceClass `Elab.match_syntax.result (inherited := true)
+  registerTraceClass `Elab.match_syntax.onMatch
 
 end Lean.Elab.Term.Quotation

src/Lean/Elab/StructInst.lean

@@ -957,6 +957,8 @@ private def elabStructInstAux (stx : Syntax) (expectedType? : Option Expr) (sour
     else
       elabStructInstAux stx expectedType? sourceView
 
-builtin_initialize registerTraceClass `Elab.struct
+builtin_initialize
+  registerTraceClass `Elab.struct
+  registerTraceClass `Elab.struct.modifyOp
 
 end Lean.Elab.Term.StructInst

src/Lean/Elab/Syntax.lean

@@ -442,4 +442,7 @@ def strLitToPattern (stx: Syntax) : MacroM Syntax :=
   | some str => return mkAtomFrom stx str
   | none     => Macro.throwUnsupported
 
+builtin_initialize
+  registerTraceClass `Elab.defaultInstance
+
 end Lean.Elab.Command

src/Lean/Elab/Term.lean

@@ -1916,4 +1916,7 @@ def isIncrementalElab [Monad m] [MonadEnv m] [MonadLiftT IO m] (decl : Name) : m
 
 export Term (TermElabM)
 
+builtin_initialize
+  registerTraceClass `Elab.implicitForall
+
 end Lean.Elab

src/Lean/Meta/DecLevel.lean

@@ -70,4 +70,7 @@ def decLevel (u : Level) : MetaM Level := do
 def getDecLevel (type : Expr) : MetaM Level := do
   decLevel (← getLevel type)
 
+builtin_initialize
+  registerTraceClass `Meta.isLevelDefEq.step
+
 end Lean.Meta

src/Lean/Meta/SizeOf.lean

@@ -514,5 +514,9 @@ def mkSizeOfInstances (typeName : Name) : MetaM Unit := do
 
 builtin_initialize
   registerTraceClass `Meta.sizeOf
+  registerTraceClass `Meta.sizeOf.minor
+  registerTraceClass `Meta.sizeOf.minor.step
+  registerTraceClass `Meta.sizeOf.aux
+  registerTraceClass `Meta.sizeOf.loop
 
 end Lean.Meta

src/Lean/Meta/Tactic/Simp/SimpAll.lean

@@ -152,4 +152,7 @@ def simpAll (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray :=
         throwError "simp_all made no progress"
     return (r, { s with })
 
+builtin_initialize
+  registerTraceClass `Meta.Tactic.simp.all
+
 end Lean.Meta

src/Lean/PrettyPrinter/Delaborator/Basic.lean

@@ -437,6 +437,8 @@ def delab (e : Expr) (optionsPerPos : OptionsPerPos := {}) : MetaM Term := do
   let (stx, _) ← delabCore e optionsPerPos Delaborator.delab
   return stx
 
-builtin_initialize registerTraceClass `PrettyPrinter.delab
+builtin_initialize
+  registerTraceClass `PrettyPrinter.delab
+  registerTraceClass `PrettyPrinter.delab.input
 
 end Lean.PrettyPrinter