diff --git a/src/Init/Lean/Meta/ExprDefEq.lean b/src/Init/Lean/Meta/ExprDefEq.lean
index fd7f22dfb1..d26113a375 100644
--- a/src/Init/Lean/Meta/ExprDefEq.lean
+++ b/src/Init/Lean/Meta/ExprDefEq.lean
@@ -438,21 +438,21 @@ end CheckAssignment
 private def checkAssignmentFailure (mvarId : Name) (fvars : Array Expr) (v : Expr) (ex : CheckAssignment.Exception) : MetaM (Option Expr) :=
 match ex with
 | CheckAssignment.Exception.occursCheck => do
-  trace! `Meta.isDefEq.assignment.occursCheck
+  trace! `Meta.isDefEq.assign.occursCheck
     (mkMVar mvarId ++ fvars ++ " := " ++ v);
   pure none
 | CheckAssignment.Exception.useFOApprox =>
   pure none
 | CheckAssignment.Exception.outOfScopeFVar fvarId => do
-  trace! `Meta.isDefEq.assignment.outOfScopeFVar
+  trace! `Meta.isDefEq.assign.outOfScopeFVar
     (mkFVar fvarId ++ " @ " ++ mkMVar mvarId ++ fvars ++ " := " ++ v);
   pure none
 | CheckAssignment.Exception.readOnlyMVarWithBiggerLCtx nestedMVarId => do
-  trace! `Meta.isDefEq.assignment.readOnlyMVarWithBiggerLCtx
+  trace! `Meta.isDefEq.assign.readOnlyMVarWithBiggerLCtx
     (mkMVar nestedMVarId ++ " @ " ++ mkMVar mvarId ++ fvars ++ " := " ++ v);
   pure none
 | CheckAssignment.Exception.mvarTypeNotWellFormedInSmallerLCtx nestedMVarId => do
-  trace! `Meta.isDefEq.assignment.mvarTypeNotWellFormedInSmallerLCtx
+  trace! `Meta.isDefEq.assign.mvarTypeNotWellFormedInSmallerLCtx
     (mkMVar nestedMVarId ++ " @ " ++ mkMVar mvarId ++ fvars ++ " := " ++ v);
   pure none
 | CheckAssignment.Exception.unknownExprMVar mvarId =>
@@ -669,13 +669,13 @@ private partial def processAssignmentAux (mvar : Expr) (mvarDecl : MetavarDecl)
       | none => useFOApprox ()
       | some v => do
         v ← mkLambda args v;
-        let finalize : Unit → MetaM Bool := fun _ => do {
+        let finalize : Unit → MetaM Bool := fun _ => traceCtx `Meta.isDefEq.assign.checkTypes $ do {
            -- must check whether types are definitionally equal or not, before assigning and returning true
            mvarType ← inferType mvar;
            vType    ← inferType v;
            condM (usingTransparency TransparencyMode.default $ isExprDefEqAux mvarType vType)
              (do assignExprMVar mvarId v; pure true)
-             (do trace! `Meta.isDefEq.assignment.typeMismatch (mvar ++ " : " ++ mvarType ++ " := " ++ v ++ " : " ++ vType);
+             (do trace! `Meta.isDefEq.assign.typeMismatch (mvar ++ " : " ++ mvarType ++ " := " ++ v ++ " : " ++ vType);
                  pure false)
         };
         if args.any (fun arg => mvarDecl.lctx.containsFVar arg) then
@@ -683,7 +683,7 @@ private partial def processAssignmentAux (mvar : Expr) (mvarDecl : MetavarDecl)
              a type incorrect term. See discussion at A2 -/
           condM (isTypeCorrect v)
             (finalize ())
-            (do trace! `Meta.isDefEq.assignment.typeError (mvar ++ " := " ++ v);
+            (do trace! `Meta.isDefEq.assign.typeError (mvar ++ " := " ++ v);
                 useFOApprox ())
         else
           finalize ()
@@ -691,9 +691,11 @@ private partial def processAssignmentAux (mvar : Expr) (mvarDecl : MetavarDecl)
 /-- Tries to solve `?m a₁ ... aₙ =?= v` by assigning `?m`.
     It assumes `?m` is unassigned. -/
 private def processAssignment (mvarApp : Expr) (v : Expr) : MetaM Bool :=
-do let mvar := mvarApp.getAppFn;
-   mvarDecl ← getMVarDecl mvar.mvarId!;
-   processAssignmentAux mvar mvarDecl v 0 mvarApp.getAppArgs
+traceCtx `Meta.isDefEq.assign $ do
+  trace! `Meta.isDefEq.assign (mvarApp ++ " := " ++ v);
+  let mvar := mvarApp.getAppFn;
+  mvarDecl ← getMVarDecl mvar.mvarId!;
+  processAssignmentAux mvar mvarDecl v 0 mvarApp.getAppArgs
 
 private def isDeltaCandidate (t : Expr) : MetaM (Option ConstantInfo) :=
 match t.getAppFn with