diff --git a/src/Lean/Meta/Injective.lean b/src/Lean/Meta/Injective.lean
index da56406f05..d4d5cef408 100644
--- a/src/Lean/Meta/Injective.lean
+++ b/src/Lean/Meta/Injective.lean
@@ -158,9 +158,13 @@ def mkInjectiveTheorems (declName : Name) : MetaM Unit := do
       -- See https://github.com/leanprover/lean4/issues/2188
       withLCtx {} {} do
       for ctor in info.ctors do
-        let ctorVal ← getConstInfoCtor ctor
-        if ctorVal.numFields > 0 then
-          mkInjectiveTheorem ctorVal
-          mkInjectiveEqTheorem ctorVal
+        withTraceNode `Meta.injective (fun _ => return m!"{ctor}") do
+          let ctorVal ← getConstInfoCtor ctor
+          if ctorVal.numFields > 0 then
+            mkInjectiveTheorem ctorVal
+            mkInjectiveEqTheorem ctorVal
+
+builtin_initialize
+  registerTraceClass `Meta.injective
 
 end Lean.Meta
diff --git a/src/Lean/Meta/SizeOf.lean b/src/Lean/Meta/SizeOf.lean
index b313fc13f1..be337143d0 100644
--- a/src/Lean/Meta/SizeOf.lean
+++ b/src/Lean/Meta/SizeOf.lean
@@ -471,42 +471,43 @@ register_builtin_option genSizeOf : Bool := {
 
 register_builtin_option genSizeOfSpec : Bool := {
   defValue := true
-  descr    := "generate `SizeOf` specificiation theorems for automatically generated instances"
+  descr    := "generate `SizeOf` specification theorems for automatically generated instances"
 }
 
 def mkSizeOfInstances (typeName : Name) : MetaM Unit := do
   if (← getEnv).contains ``SizeOf && genSizeOf.get (← getOptions) && !(← isInductivePredicate typeName) then
-    let indInfo ← getConstInfoInduct typeName
-    unless indInfo.isUnsafe do
-      let (fns, recMap) ← mkSizeOfFns typeName
-      for indTypeName in indInfo.all, fn in fns do
-        let indInfo ← getConstInfoInduct indTypeName
-        forallTelescopeReducing indInfo.type fun xs _ =>
-          let params := xs[:indInfo.numParams]
-          withInstImplicitAsImplict params do
-            let indices := xs[indInfo.numParams:]
-            mkLocalInstances params fun localInsts => do
-              let us := indInfo.levelParams.map mkLevelParam
-              let indType := mkAppN (mkConst indTypeName us) xs
-              let sizeOfIndType ← mkAppM ``SizeOf #[indType]
-              withLocalDeclD `m indType fun m => do
-                let v ← mkLambdaFVars #[m] <| mkAppN (mkConst fn us) (params ++ localInsts ++ indices ++ #[m])
-                let sizeOfMk ← mkAppM ``SizeOf.mk #[v]
-                let instDeclName := indTypeName ++ `_sizeOf_inst
-                let instDeclType ← mkForallFVars (xs ++ localInsts) sizeOfIndType
-                let instDeclValue ← mkLambdaFVars (xs ++ localInsts) sizeOfMk
-                trace[Meta.sizeOf] ">> {instDeclName} : {instDeclType}"
-                addDecl <| Declaration.defnDecl {
-                  name        := instDeclName
-                  levelParams := indInfo.levelParams
-                  type        := instDeclType
-                  value       := instDeclValue
-                  safety      := .safe
-                  hints       := .abbrev
-                }
-                addInstance instDeclName AttributeKind.global (eval_prio default)
-      if genSizeOfSpec.get (← getOptions) then
-        mkSizeOfSpecTheorems indInfo.all.toArray fns recMap
+    withTraceNode `Meta.sizeOf (fun _ => return m!"{typeName}") do
+      let indInfo ← getConstInfoInduct typeName
+      unless indInfo.isUnsafe do
+        let (fns, recMap) ← mkSizeOfFns typeName
+        for indTypeName in indInfo.all, fn in fns do
+          let indInfo ← getConstInfoInduct indTypeName
+          forallTelescopeReducing indInfo.type fun xs _ =>
+            let params := xs[:indInfo.numParams]
+            withInstImplicitAsImplict params do
+              let indices := xs[indInfo.numParams:]
+              mkLocalInstances params fun localInsts => do
+                let us := indInfo.levelParams.map mkLevelParam
+                let indType := mkAppN (mkConst indTypeName us) xs
+                let sizeOfIndType ← mkAppM ``SizeOf #[indType]
+                withLocalDeclD `m indType fun m => do
+                  let v ← mkLambdaFVars #[m] <| mkAppN (mkConst fn us) (params ++ localInsts ++ indices ++ #[m])
+                  let sizeOfMk ← mkAppM ``SizeOf.mk #[v]
+                  let instDeclName := indTypeName ++ `_sizeOf_inst
+                  let instDeclType ← mkForallFVars (xs ++ localInsts) sizeOfIndType
+                  let instDeclValue ← mkLambdaFVars (xs ++ localInsts) sizeOfMk
+                  trace[Meta.sizeOf] ">> {instDeclName} : {instDeclType}"
+                  addDecl <| Declaration.defnDecl {
+                    name        := instDeclName
+                    levelParams := indInfo.levelParams
+                    type        := instDeclType
+                    value       := instDeclValue
+                    safety      := .safe
+                    hints       := .abbrev
+                  }
+                  addInstance instDeclName AttributeKind.global (eval_prio default)
+        if genSizeOfSpec.get (← getOptions) then
+          mkSizeOfSpecTheorems indInfo.all.toArray fns recMap
 
 builtin_initialize
   registerTraceClass `Meta.sizeOf