diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean
index bd4e26695021..d6ac8824411f 100644
--- a/src/Lean/Meta/SynthInstance.lean
+++ b/src/Lean/Meta/SynthInstance.lean
@@ -573,7 +573,7 @@ def generate : SynthM Unit := do
             modify fun s => { s with generatorStack := s.generatorStack.pop }
             return
     discard do withMCtx mctx do
-      withTraceNode `Meta.synthInstance
+      withTraceNode `Meta.synthInstance.apply
         (return m!"{exceptOptionEmoji ·} apply {inst.val} to {← instantiateMVars (← inferType mvar)}") do
       modifyTop fun gNode => { gNode with currInstanceIdx := idx }
       if let some (mctx, subgoals) ← tryResolve mvar inst then
@@ -982,6 +982,7 @@ register_builtin_option trace.Meta.synthInstance : Bool := {
 
 builtin_initialize
   registerTraceClass `Meta.synthPending
+  registerTraceClass `Meta.synthInstance.apply (inherited := true)
   registerTraceClass `Meta.synthInstance.instances (inherited := true)
   registerTraceClass `Meta.synthInstance.tryResolve (inherited := true)
   registerTraceClass `Meta.synthInstance.answer (inherited := true)
diff --git a/tests/elab/366.lean.out.expected b/tests/elab/366.lean.out.expected
index 190dcd528ad8..3e6d9425c756 100644
--- a/tests/elab/366.lean.out.expected
+++ b/tests/elab/366.lean.out.expected
@@ -1,7 +1,7 @@
 [Meta.synthInstance] ✅️ Inhabited Nat
   [Meta.synthInstance] new goal Inhabited Nat
     [Meta.synthInstance.instances] #[@instInhabitedOfMonad, instInhabitedNat]
-  [Meta.synthInstance] ✅️ apply instInhabitedNat to Inhabited Nat
+  [Meta.synthInstance.apply] ✅️ apply instInhabitedNat to Inhabited Nat
     [Meta.synthInstance.tryResolve] ✅️ Inhabited Nat ≟ Inhabited Nat
     [Meta.synthInstance.answer] ✅️ Inhabited Nat
   [Meta.synthInstance] result instInhabitedNat
diff --git a/tests/elab/815b.lean.out.expected b/tests/elab/815b.lean.out.expected
index 98375589cbc2..19902e99f4ed 100644
--- a/tests/elab/815b.lean.out.expected
+++ b/tests/elab/815b.lean.out.expected
@@ -8,15 +8,15 @@
 [Meta.synthInstance] ✅️ IsSmooth fun g a => f (g a) d
   [Meta.synthInstance] new goal IsSmooth fun g a => f (g a) d
     [Meta.synthInstance.instances] #[@identity, @const, @parm, @comp, @diag, @swap, inst✝]
-  [Meta.synthInstance] ❌️ apply inst✝ to IsSmooth fun g a => f (g a) d
+  [Meta.synthInstance.apply] ❌️ apply inst✝ to IsSmooth fun g a => f (g a) d
     [Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g a => f (g a) d ≟ IsSmooth f
-  [Meta.synthInstance] ✅️ apply @swap to IsSmooth fun g a => f (g a) d
+  [Meta.synthInstance.apply] ✅️ apply @swap to IsSmooth fun g a => f (g a) d
     [Meta.synthInstance.tryResolve] ✅️ IsSmooth fun g a => f (g a) d ≟ IsSmooth fun b a => f (b a) d
     [Meta.synthInstance] new goal ∀ (a : α), IsSmooth fun g => f (g a) d
       [Meta.synthInstance.instances] #[@identity, @const, @parm, @comp, @diag, inst✝]
-  [Meta.synthInstance] ❌️ apply inst✝ to ∀ (a : α), IsSmooth fun g => f (g a) d
+  [Meta.synthInstance.apply] ❌️ apply inst✝ to ∀ (a : α), IsSmooth fun g => f (g a) d
     [Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => f (g a) d ≟ IsSmooth f
-  [Meta.synthInstance] ✅️ apply @diag to ∀ (a : α), IsSmooth fun g => f (g a) d
+  [Meta.synthInstance.apply] ✅️ apply @diag to ∀ (a : α), IsSmooth fun g => f (g a) d
     [Meta.synthInstance.tryResolve] ✅️ IsSmooth fun g => f (g a) d ≟ IsSmooth fun a_1 => f (a_1 a) d
     [Meta.synthInstance.unusedArgs] ∀ (a : α), IsSmooth f
         has unused arguments, reduced type
@@ -25,7 +25,7 @@
           fun redf a => redf
     [Meta.synthInstance] new goal IsSmooth f
       [Meta.synthInstance.instances] #[inst✝]
-  [Meta.synthInstance] ✅️ apply inst✝ to IsSmooth f
+  [Meta.synthInstance.apply] ✅️ apply inst✝ to IsSmooth f
     [Meta.synthInstance.tryResolve] ✅️ IsSmooth f ≟ IsSmooth f
     [Meta.synthInstance.answer] ✅️ IsSmooth f
   [Meta.synthInstance.resume] propagating IsSmooth f to subgoal IsSmooth f of ∀ (a : α), IsSmooth fun g => f (g a) d
@@ -45,23 +45,23 @@
           fun redf a => redf
     [Meta.synthInstance] new goal ∀ (b : β), IsSmooth (f b)
       [Meta.synthInstance.instances] #[inst✝]
-  [Meta.synthInstance] ❌️ apply inst✝ to ∀ (b : β), IsSmooth (f b)
+  [Meta.synthInstance.apply] ❌️ apply inst✝ to ∀ (b : β), IsSmooth (f b)
     [Meta.synthInstance.tryResolve] ❌️ IsSmooth (f b) ≟ IsSmooth f
-  [Meta.synthInstance] ❌️ apply @comp to ∀ (a : α), IsSmooth fun g => f (g a) d
+  [Meta.synthInstance.apply] ❌️ apply @comp to ∀ (a : α), IsSmooth fun g => f (g a) d
     [Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => f (g a) d ≟ IsSmooth fun a_1 => ?m a (?m a a_1)
-  [Meta.synthInstance] ✅️ apply @parm to ∀ (a : α), IsSmooth fun g => f (g a) d
+  [Meta.synthInstance.apply] ✅️ apply @parm to ∀ (a : α), IsSmooth fun g => f (g a) d
     [Meta.synthInstance.tryResolve] ✅️ IsSmooth fun g => f (g a) d ≟ IsSmooth fun a_1 => f (a_1 a) d
     [Meta.synthInstance] new goal ∀ (a : α), IsSmooth fun g => f (g a)
       [Meta.synthInstance.instances] #[@identity, @const, @parm, @comp, @diag, @swap, inst✝]
-  [Meta.synthInstance] ❌️ apply inst✝ to ∀ (a : α), IsSmooth fun g => f (g a)
+  [Meta.synthInstance.apply] ❌️ apply inst✝ to ∀ (a : α), IsSmooth fun g => f (g a)
     [Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => f (g a) ≟ IsSmooth f
-  [Meta.synthInstance] ✅️ apply @swap to ∀ (a : α), IsSmooth fun g => f (g a)
+  [Meta.synthInstance.apply] ✅️ apply @swap to ∀ (a : α), IsSmooth fun g => f (g a)
     [Meta.synthInstance.tryResolve] ✅️ IsSmooth fun g => f (g a) ≟ IsSmooth fun b a_1 => f (b a) a_1
     [Meta.synthInstance] new goal ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
       [Meta.synthInstance.instances] #[@identity, @const, @parm, @comp, @diag, inst✝]
-  [Meta.synthInstance] ❌️ apply inst✝ to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
+  [Meta.synthInstance.apply] ❌️ apply inst✝ to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
     [Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => f (g a✝) a ≟ IsSmooth f
-  [Meta.synthInstance] ✅️ apply @diag to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
+  [Meta.synthInstance.apply] ✅️ apply @diag to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
     [Meta.synthInstance.tryResolve] ✅️ IsSmooth fun g => f (g a✝) a ≟ IsSmooth fun a_1 => f (a_1 a✝) a
     [Meta.synthInstance.unusedArgs] ∀ (a : α) (a : δ), IsSmooth f
         has unused arguments, reduced type
@@ -76,23 +76,23 @@
           ∀ (b : β), IsSmooth (f b)
         Transformer
           fun redf a a_1 => redf
-  [Meta.synthInstance] ❌️ apply @comp to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
+  [Meta.synthInstance.apply] ❌️ apply @comp to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
     [Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => f (g a✝) a ≟ IsSmooth fun a_1 => ?m a✝ a (?m a✝ a a_1)
-  [Meta.synthInstance] ✅️ apply @parm to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
+  [Meta.synthInstance.apply] ✅️ apply @parm to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
     [Meta.synthInstance.tryResolve] ✅️ IsSmooth fun g => f (g a✝) a ≟ IsSmooth fun a_1 => f (a_1 a✝) a
     [Meta.synthInstance.unusedArgs] ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a)
         has unused arguments, reduced type
           ∀ (a : α), IsSmooth fun g => f (g a)
         Transformer
           fun redf a a_1 => redf a
-  [Meta.synthInstance] ❌️ apply @const to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
+  [Meta.synthInstance.apply] ❌️ apply @const to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
     [Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => f (g a✝) a ≟ IsSmooth fun a_1 => ?m a✝ a
-  [Meta.synthInstance] ❌️ apply @identity to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
+  [Meta.synthInstance.apply] ❌️ apply @identity to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
     [Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => f (g a✝) a ≟ IsSmooth fun a => a
-  [Meta.synthInstance] ❌️ apply @diag to ∀ (a : α), IsSmooth fun g => f (g a)
+  [Meta.synthInstance.apply] ❌️ apply @diag to ∀ (a : α), IsSmooth fun g => f (g a)
     [Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g =>
           f (g a) ≟ IsSmooth fun a_1 => ?m a (?m a a_1) (?m a a_1)
-  [Meta.synthInstance] ✅️ apply @comp to ∀ (a : α), IsSmooth fun g => f (g a)
+  [Meta.synthInstance.apply] ✅️ apply @comp to ∀ (a : α), IsSmooth fun g => f (g a)
     [Meta.synthInstance.tryResolve] ✅️ IsSmooth fun g => f (g a) ≟ IsSmooth fun a_1 => f (a_1 a)
     [Meta.synthInstance.unusedArgs] ∀ (a : α), IsSmooth f
         has unused arguments, reduced type
@@ -104,13 +104,13 @@
     [Meta.synthInstance.resume] size: 1
     [Meta.synthInstance] new goal ∀ (a : α), IsSmooth fun g => g a
       [Meta.synthInstance.instances] #[@identity, @const, @parm, @comp, @diag, inst✝]
-  [Meta.synthInstance] ❌️ apply inst✝ to ∀ (a : α), IsSmooth fun g => g a
+  [Meta.synthInstance.apply] ❌️ apply inst✝ to ∀ (a : α), IsSmooth fun g => g a
     [Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => g a ≟ IsSmooth f
-  [Meta.synthInstance] ❌️ apply @diag to ∀ (a : α), IsSmooth fun g => g a
+  [Meta.synthInstance.apply] ❌️ apply @diag to ∀ (a : α), IsSmooth fun g => g a
     [Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => g a ≟ IsSmooth fun a_1 => ?m a (?m a a_1) (?m a a_1)
-  [Meta.synthInstance] ❌️ apply @comp to ∀ (a : α), IsSmooth fun g => g a
+  [Meta.synthInstance.apply] ❌️ apply @comp to ∀ (a : α), IsSmooth fun g => g a
     [Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => g a ≟ IsSmooth fun a_1 => ?m a (?m a a_1)
-  [Meta.synthInstance] ✅️ apply @parm to ∀ (a : α), IsSmooth fun g => g a
+  [Meta.synthInstance.apply] ✅️ apply @parm to ∀ (a : α), IsSmooth fun g => g a
     [Meta.synthInstance.tryResolve] ✅️ IsSmooth fun g => g a ≟ IsSmooth fun a_1 => a_1 a
     [Meta.synthInstance.unusedArgs] ∀ (a : α), IsSmooth fun g => g
         has unused arguments, reduced type
@@ -119,19 +119,19 @@
           fun redf a => redf
     [Meta.synthInstance] new goal IsSmooth fun g => g
       [Meta.synthInstance.instances] #[@identity, @const, @parm, @comp, @diag, @swap, inst✝]
-  [Meta.synthInstance] ❌️ apply inst✝ to IsSmooth fun g => g
+  [Meta.synthInstance.apply] ❌️ apply inst✝ to IsSmooth fun g => g
     [Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => g ≟ IsSmooth f
-  [Meta.synthInstance] ✅️ apply @swap to IsSmooth fun g => g
+  [Meta.synthInstance.apply] ✅️ apply @swap to IsSmooth fun g => g
     [Meta.synthInstance.tryResolve] ✅️ IsSmooth fun g => g ≟ IsSmooth fun b a => b a
-  [Meta.synthInstance] ❌️ apply @diag to IsSmooth fun g => g
+  [Meta.synthInstance.apply] ❌️ apply @diag to IsSmooth fun g => g
     [Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => g ≟ IsSmooth fun a => ?m (?m a) (?m a)
-  [Meta.synthInstance] ❌️ apply @comp to IsSmooth fun g => g
+  [Meta.synthInstance.apply] ❌️ apply @comp to IsSmooth fun g => g
     [Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => g ≟ IsSmooth fun a => ?m (?m a)
-  [Meta.synthInstance] ❌️ apply @parm to IsSmooth fun g => g
+  [Meta.synthInstance.apply] ❌️ apply @parm to IsSmooth fun g => g
     [Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => g ≟ IsSmooth fun a => ?m a ?m
-  [Meta.synthInstance] ❌️ apply @const to IsSmooth fun g => g
+  [Meta.synthInstance.apply] ❌️ apply @const to IsSmooth fun g => g
     [Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => g ≟ IsSmooth fun a => ?m
-  [Meta.synthInstance] ✅️ apply @identity to IsSmooth fun g => g
+  [Meta.synthInstance.apply] ✅️ apply @identity to IsSmooth fun g => g
     [Meta.synthInstance.tryResolve] ✅️ IsSmooth fun g => g ≟ IsSmooth fun a => a
     [Meta.synthInstance.answer] ✅️ IsSmooth fun g => g
   [Meta.synthInstance.resume] propagating IsSmooth fun a =>
diff --git a/tests/elab/infoFromFailure.lean b/tests/elab/infoFromFailure.lean
index 02db4d600d35..4a039e2fb0d2 100644
--- a/tests/elab/infoFromFailure.lean
+++ b/tests/elab/infoFromFailure.lean
@@ -17,51 +17,51 @@ info: B.foo "hello" : String × String
 trace: [Meta.synthInstance] ❌️ Add String
   [Meta.synthInstance] new goal Add String
     [Meta.synthInstance.instances] #[@Lean.Grind.AddCommMonoid.toAdd, @Lean.Grind.Semiring.toAdd]
-  [Meta.synthInstance] ✅️ apply @Lean.Grind.Semiring.toAdd to Add String
+  [Meta.synthInstance.apply] ✅️ apply @Lean.Grind.Semiring.toAdd to Add String
     [Meta.synthInstance.tryResolve] ✅️ Add String ≟ Add String
     [Meta.synthInstance] new goal Lean.Grind.Semiring String
       [Meta.synthInstance.instances] #[@Lean.Grind.Ring.toSemiring, @Lean.Grind.CommSemiring.toSemiring]
-  [Meta.synthInstance] ✅️ apply @Lean.Grind.CommSemiring.toSemiring to Lean.Grind.Semiring String
+  [Meta.synthInstance.apply] ✅️ apply @Lean.Grind.CommSemiring.toSemiring to Lean.Grind.Semiring String
     [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.Semiring String ≟ Lean.Grind.Semiring String
     [Meta.synthInstance] new goal Lean.Grind.CommSemiring String
       [Meta.synthInstance.instances] #[@Lean.Grind.CommRing.toCommSemiring]
-  [Meta.synthInstance] ✅️ apply @Lean.Grind.CommRing.toCommSemiring to Lean.Grind.CommSemiring String
+  [Meta.synthInstance.apply] ✅️ apply @Lean.Grind.CommRing.toCommSemiring to Lean.Grind.CommSemiring String
     [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.CommSemiring String ≟ Lean.Grind.CommSemiring String
     [Meta.synthInstance] new goal Lean.Grind.CommRing String
       [Meta.synthInstance.instances] #[@Lean.Grind.Field.toCommRing]
-  [Meta.synthInstance] ✅️ apply @Lean.Grind.Field.toCommRing to Lean.Grind.CommRing String
+  [Meta.synthInstance.apply] ✅️ apply @Lean.Grind.Field.toCommRing to Lean.Grind.CommRing String
     [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.CommRing String ≟ Lean.Grind.CommRing String
     [Meta.synthInstance] no instances for Lean.Grind.Field String
       [Meta.synthInstance.instances] #[]
-  [Meta.synthInstance] ✅️ apply @Lean.Grind.Ring.toSemiring to Lean.Grind.Semiring String
+  [Meta.synthInstance.apply] ✅️ apply @Lean.Grind.Ring.toSemiring to Lean.Grind.Semiring String
     [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.Semiring String ≟ Lean.Grind.Semiring String
     [Meta.synthInstance] new goal Lean.Grind.Ring String
       [Meta.synthInstance.instances] #[@Lean.Grind.CommRing.toRing]
-  [Meta.synthInstance] ✅️ apply @Lean.Grind.CommRing.toRing to Lean.Grind.Ring String
+  [Meta.synthInstance.apply] ✅️ apply @Lean.Grind.CommRing.toRing to Lean.Grind.Ring String
     [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.Ring String ≟ Lean.Grind.Ring String
-  [Meta.synthInstance] ✅️ apply @Lean.Grind.AddCommMonoid.toAdd to Add String
+  [Meta.synthInstance.apply] ✅️ apply @Lean.Grind.AddCommMonoid.toAdd to Add String
     [Meta.synthInstance.tryResolve] ✅️ Add String ≟ Add String
     [Meta.synthInstance] new goal Lean.Grind.AddCommMonoid String
       [Meta.synthInstance.instances] #[@Lean.Grind.AddCommGroup.toAddCommMonoid, @Lean.Grind.NatModule.toAddCommMonoid]
-  [Meta.synthInstance] ✅️ apply @Lean.Grind.NatModule.toAddCommMonoid to Lean.Grind.AddCommMonoid String
+  [Meta.synthInstance.apply] ✅️ apply @Lean.Grind.NatModule.toAddCommMonoid to Lean.Grind.AddCommMonoid String
     [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.AddCommMonoid String ≟ Lean.Grind.AddCommMonoid String
     [Meta.synthInstance] new goal Lean.Grind.NatModule String
       [Meta.synthInstance.instances] #[@Lean.Grind.IntModule.toNatModule, @Lean.Grind.Semiring.toNatModule]
-  [Meta.synthInstance] ✅️ apply @Lean.Grind.Semiring.toNatModule to Lean.Grind.NatModule String
+  [Meta.synthInstance.apply] ✅️ apply @Lean.Grind.Semiring.toNatModule to Lean.Grind.NatModule String
     [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.NatModule String ≟ Lean.Grind.NatModule String
-  [Meta.synthInstance] ✅️ apply @Lean.Grind.IntModule.toNatModule to Lean.Grind.NatModule String
+  [Meta.synthInstance.apply] ✅️ apply @Lean.Grind.IntModule.toNatModule to Lean.Grind.NatModule String
     [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.NatModule String ≟ Lean.Grind.NatModule String
     [Meta.synthInstance] new goal Lean.Grind.IntModule String
       [Meta.synthInstance.instances] #[@Lean.Grind.Ring.toIntModule]
-  [Meta.synthInstance] ✅️ apply @Lean.Grind.Ring.toIntModule to Lean.Grind.IntModule String
+  [Meta.synthInstance.apply] ✅️ apply @Lean.Grind.Ring.toIntModule to Lean.Grind.IntModule String
     [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.IntModule String ≟ Lean.Grind.IntModule String
-  [Meta.synthInstance] ✅️ apply @Lean.Grind.AddCommGroup.toAddCommMonoid to Lean.Grind.AddCommMonoid String
+  [Meta.synthInstance.apply] ✅️ apply @Lean.Grind.AddCommGroup.toAddCommMonoid to Lean.Grind.AddCommMonoid String
     [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.AddCommMonoid String ≟ Lean.Grind.AddCommMonoid String
     [Meta.synthInstance] new goal Lean.Grind.AddCommGroup String
       [Meta.synthInstance.instances] #[@Lean.Grind.IntModule.toAddCommGroup, @Lean.Grind.Ring.toAddCommGroup]
-  [Meta.synthInstance] ✅️ apply @Lean.Grind.Ring.toAddCommGroup to Lean.Grind.AddCommGroup String
+  [Meta.synthInstance.apply] ✅️ apply @Lean.Grind.Ring.toAddCommGroup to Lean.Grind.AddCommGroup String
     [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.AddCommGroup String ≟ Lean.Grind.AddCommGroup String
-  [Meta.synthInstance] ✅️ apply @Lean.Grind.IntModule.toAddCommGroup to Lean.Grind.AddCommGroup String
+  [Meta.synthInstance.apply] ✅️ apply @Lean.Grind.IntModule.toAddCommGroup to Lean.Grind.AddCommGroup String
     [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.AddCommGroup String ≟ Lean.Grind.AddCommGroup String
   [Meta.synthInstance] result <not-available>
 -/
@@ -74,51 +74,51 @@ trace: [Meta.synthInstance] ❌️ Add String
 trace: [Meta.synthInstance] ❌️ Add Bool
   [Meta.synthInstance] new goal Add Bool
     [Meta.synthInstance.instances] #[@Lean.Grind.AddCommMonoid.toAdd, @Lean.Grind.Semiring.toAdd]
-  [Meta.synthInstance] ✅️ apply @Lean.Grind.Semiring.toAdd to Add Bool
+  [Meta.synthInstance.apply] ✅️ apply @Lean.Grind.Semiring.toAdd to Add Bool
     [Meta.synthInstance.tryResolve] ✅️ Add Bool ≟ Add Bool
     [Meta.synthInstance] new goal Lean.Grind.Semiring Bool
       [Meta.synthInstance.instances] #[@Lean.Grind.Ring.toSemiring, @Lean.Grind.CommSemiring.toSemiring]
-  [Meta.synthInstance] ✅️ apply @Lean.Grind.CommSemiring.toSemiring to Lean.Grind.Semiring Bool
+  [Meta.synthInstance.apply] ✅️ apply @Lean.Grind.CommSemiring.toSemiring to Lean.Grind.Semiring Bool
     [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.Semiring Bool ≟ Lean.Grind.Semiring Bool
     [Meta.synthInstance] new goal Lean.Grind.CommSemiring Bool
       [Meta.synthInstance.instances] #[@Lean.Grind.CommRing.toCommSemiring]
-  [Meta.synthInstance] ✅️ apply @Lean.Grind.CommRing.toCommSemiring to Lean.Grind.CommSemiring Bool
+  [Meta.synthInstance.apply] ✅️ apply @Lean.Grind.CommRing.toCommSemiring to Lean.Grind.CommSemiring Bool
     [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.CommSemiring Bool ≟ Lean.Grind.CommSemiring Bool
     [Meta.synthInstance] new goal Lean.Grind.CommRing Bool
       [Meta.synthInstance.instances] #[@Lean.Grind.Field.toCommRing]
-  [Meta.synthInstance] ✅️ apply @Lean.Grind.Field.toCommRing to Lean.Grind.CommRing Bool
+  [Meta.synthInstance.apply] ✅️ apply @Lean.Grind.Field.toCommRing to Lean.Grind.CommRing Bool
     [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.CommRing Bool ≟ Lean.Grind.CommRing Bool
     [Meta.synthInstance] no instances for Lean.Grind.Field Bool
       [Meta.synthInstance.instances] #[]
-  [Meta.synthInstance] ✅️ apply @Lean.Grind.Ring.toSemiring to Lean.Grind.Semiring Bool
+  [Meta.synthInstance.apply] ✅️ apply @Lean.Grind.Ring.toSemiring to Lean.Grind.Semiring Bool
     [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.Semiring Bool ≟ Lean.Grind.Semiring Bool
     [Meta.synthInstance] new goal Lean.Grind.Ring Bool
       [Meta.synthInstance.instances] #[@Lean.Grind.CommRing.toRing]
-  [Meta.synthInstance] ✅️ apply @Lean.Grind.CommRing.toRing to Lean.Grind.Ring Bool
+  [Meta.synthInstance.apply] ✅️ apply @Lean.Grind.CommRing.toRing to Lean.Grind.Ring Bool
     [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.Ring Bool ≟ Lean.Grind.Ring Bool
-  [Meta.synthInstance] ✅️ apply @Lean.Grind.AddCommMonoid.toAdd to Add Bool
+  [Meta.synthInstance.apply] ✅️ apply @Lean.Grind.AddCommMonoid.toAdd to Add Bool
     [Meta.synthInstance.tryResolve] ✅️ Add Bool ≟ Add Bool
     [Meta.synthInstance] new goal Lean.Grind.AddCommMonoid Bool
       [Meta.synthInstance.instances] #[@Lean.Grind.AddCommGroup.toAddCommMonoid, @Lean.Grind.NatModule.toAddCommMonoid]
-  [Meta.synthInstance] ✅️ apply @Lean.Grind.NatModule.toAddCommMonoid to Lean.Grind.AddCommMonoid Bool
+  [Meta.synthInstance.apply] ✅️ apply @Lean.Grind.NatModule.toAddCommMonoid to Lean.Grind.AddCommMonoid Bool
     [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.AddCommMonoid Bool ≟ Lean.Grind.AddCommMonoid Bool
     [Meta.synthInstance] new goal Lean.Grind.NatModule Bool
       [Meta.synthInstance.instances] #[@Lean.Grind.IntModule.toNatModule, @Lean.Grind.Semiring.toNatModule]
-  [Meta.synthInstance] ✅️ apply @Lean.Grind.Semiring.toNatModule to Lean.Grind.NatModule Bool
+  [Meta.synthInstance.apply] ✅️ apply @Lean.Grind.Semiring.toNatModule to Lean.Grind.NatModule Bool
     [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.NatModule Bool ≟ Lean.Grind.NatModule Bool
-  [Meta.synthInstance] ✅️ apply @Lean.Grind.IntModule.toNatModule to Lean.Grind.NatModule Bool
+  [Meta.synthInstance.apply] ✅️ apply @Lean.Grind.IntModule.toNatModule to Lean.Grind.NatModule Bool
     [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.NatModule Bool ≟ Lean.Grind.NatModule Bool
     [Meta.synthInstance] new goal Lean.Grind.IntModule Bool
       [Meta.synthInstance.instances] #[@Lean.Grind.Ring.toIntModule]
-  [Meta.synthInstance] ✅️ apply @Lean.Grind.Ring.toIntModule to Lean.Grind.IntModule Bool
+  [Meta.synthInstance.apply] ✅️ apply @Lean.Grind.Ring.toIntModule to Lean.Grind.IntModule Bool
     [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.IntModule Bool ≟ Lean.Grind.IntModule Bool
-  [Meta.synthInstance] ✅️ apply @Lean.Grind.AddCommGroup.toAddCommMonoid to Lean.Grind.AddCommMonoid Bool
+  [Meta.synthInstance.apply] ✅️ apply @Lean.Grind.AddCommGroup.toAddCommMonoid to Lean.Grind.AddCommMonoid Bool
     [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.AddCommMonoid Bool ≟ Lean.Grind.AddCommMonoid Bool
     [Meta.synthInstance] new goal Lean.Grind.AddCommGroup Bool
       [Meta.synthInstance.instances] #[@Lean.Grind.IntModule.toAddCommGroup, @Lean.Grind.Ring.toAddCommGroup]
-  [Meta.synthInstance] ✅️ apply @Lean.Grind.Ring.toAddCommGroup to Lean.Grind.AddCommGroup Bool
+  [Meta.synthInstance.apply] ✅️ apply @Lean.Grind.Ring.toAddCommGroup to Lean.Grind.AddCommGroup Bool
     [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.AddCommGroup Bool ≟ Lean.Grind.AddCommGroup Bool
-  [Meta.synthInstance] ✅️ apply @Lean.Grind.IntModule.toAddCommGroup to Lean.Grind.AddCommGroup Bool
+  [Meta.synthInstance.apply] ✅️ apply @Lean.Grind.IntModule.toAddCommGroup to Lean.Grind.AddCommGroup Bool
     [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.AddCommGroup Bool ≟ Lean.Grind.AddCommGroup Bool
   [Meta.synthInstance] result <not-available>
 -/
diff --git a/tests/elab/setOptionTermTactic.lean.out.expected b/tests/elab/setOptionTermTactic.lean.out.expected
index cd2d9b2c3e31..1878862a008f 100644
--- a/tests/elab/setOptionTermTactic.lean.out.expected
+++ b/tests/elab/setOptionTermTactic.lean.out.expected
@@ -1,7 +1,7 @@
 [Meta.synthInstance] 💥️ OfNat ?m 1
   [Meta.synthInstance] new goal OfNat ?m 1
     [Meta.synthInstance.instances] #[@Lean.Grind.Semiring.ofNat, @One.toOfNat1, @Int16.instOfNat, @UInt64.instOfNat, @Rat.instOfNat, @Int8.instOfNat, @instOfNatFloat, @BitVec.instOfNat, Dyadic.instOfNat, @Int64.instOfNat, @instOfNat, @Id.instOfNat, @UInt16.instOfNat, instOfNatNat, @UInt32.instOfNat, @UInt8.instOfNat, @Fin.instOfNat, @ISize.instOfNat, @instOfNatFloat32, @Int32.instOfNat, @USize.instOfNat]
-  [Meta.synthInstance] 💥️ apply @USize.instOfNat to OfNat ?m 1
+  [Meta.synthInstance.apply] 💥️ apply @USize.instOfNat to OfNat ?m 1
     [Meta.synthInstance.tryResolve] 💥️ OfNat ?m 1 ≟ OfNat USize ?m
 [Meta.Tactic.simp.rewrite] Nat.add_succ:1000:
       x + 1
diff --git a/tests/elab/synth1.lean.out.expected b/tests/elab/synth1.lean.out.expected
index 7172d31f199f..f14ac0db0901 100644
--- a/tests/elab/synth1.lean.out.expected
+++ b/tests/elab/synth1.lean.out.expected
@@ -1,11 +1,11 @@
 [Meta.synthInstance] ✅️ MonadEvalT MetaM Elab.Command.CommandElabM
   [Meta.synthInstance] new goal MonadEvalT MetaM Elab.Command.CommandElabM
     [Meta.synthInstance.instances] #[instMonadEvalTOfMonadEval, instMonadEvalT]
-  [Meta.synthInstance] ❌️ apply instMonadEvalT to MonadEvalT MetaM Elab.Command.CommandElabM
-  [Meta.synthInstance] ✅️ apply instMonadEvalTOfMonadEval to MonadEvalT MetaM Elab.Command.CommandElabM
+  [Meta.synthInstance.apply] ❌️ apply instMonadEvalT to MonadEvalT MetaM Elab.Command.CommandElabM
+  [Meta.synthInstance.apply] ✅️ apply instMonadEvalTOfMonadEval to MonadEvalT MetaM Elab.Command.CommandElabM
     [Meta.synthInstance] new goal MonadEval _tc.1 Elab.Command.CommandElabM
       [Meta.synthInstance.instances] #[@instMonadEvalOfMonadLift, Elab.Command.instMonadEvalTermElabMCommandElabM]
-  [Meta.synthInstance] ✅️ apply Elab.Command.instMonadEvalTermElabMCommandElabM to MonadEval Elab.TermElabM
+  [Meta.synthInstance.apply] ✅️ apply Elab.Command.instMonadEvalTermElabMCommandElabM to MonadEval Elab.TermElabM
         Elab.Command.CommandElabM
     [Meta.synthInstance.answer] ✅️ MonadEval Elab.TermElabM Elab.Command.CommandElabM
   [Meta.synthInstance.resume] propagating MonadEval Elab.TermElabM
@@ -14,15 +14,15 @@
     [Meta.synthInstance.resume] size: 1
     [Meta.synthInstance] new goal MonadEvalT MetaM Elab.TermElabM
       [Meta.synthInstance.instances] #[instMonadEvalTOfMonadEval, instMonadEvalT]
-  [Meta.synthInstance] ❌️ apply instMonadEvalT to MonadEvalT MetaM Elab.TermElabM
-  [Meta.synthInstance] ✅️ apply instMonadEvalTOfMonadEval to MonadEvalT MetaM Elab.TermElabM
+  [Meta.synthInstance.apply] ❌️ apply instMonadEvalT to MonadEvalT MetaM Elab.TermElabM
+  [Meta.synthInstance.apply] ✅️ apply instMonadEvalTOfMonadEval to MonadEvalT MetaM Elab.TermElabM
     [Meta.synthInstance] new goal MonadEval _tc.1 Elab.TermElabM
       [Meta.synthInstance.instances] #[@instMonadEvalOfMonadLift]
-  [Meta.synthInstance] ✅️ apply @instMonadEvalOfMonadLift to MonadEval ?m Elab.TermElabM
+  [Meta.synthInstance.apply] ✅️ apply @instMonadEvalOfMonadLift to MonadEval ?m Elab.TermElabM
     [Meta.synthInstance] new goal MonadLift _tc.1 Elab.TermElabM
       [Meta.synthInstance.instances] #[@ReaderT.instMonadLift]
-  [Meta.synthInstance] ✅️ apply @ReaderT.instMonadLift to MonadLift (StateRefT' IO.RealWorld Elab.Term.State MetaM)
-        Elab.TermElabM
+  [Meta.synthInstance.apply] ✅️ apply @ReaderT.instMonadLift to MonadLift
+        (StateRefT' IO.RealWorld Elab.Term.State MetaM) Elab.TermElabM
     [Meta.synthInstance.answer] ✅️ MonadLift (StateRefT' IO.RealWorld Elab.Term.State MetaM) Elab.TermElabM
   [Meta.synthInstance.resume] propagating MonadLift (StateRefT' IO.RealWorld Elab.Term.State MetaM)
         (ReaderT Elab.Term.Context
@@ -37,16 +37,16 @@
     [Meta.synthInstance.resume] size: 2
     [Meta.synthInstance] new goal MonadEvalT MetaM (StateRefT' IO.RealWorld Elab.Term.State MetaM)
       [Meta.synthInstance.instances] #[instMonadEvalTOfMonadEval, instMonadEvalT]
-  [Meta.synthInstance] ❌️ apply instMonadEvalT to MonadEvalT MetaM (StateRefT' IO.RealWorld Elab.Term.State MetaM)
-  [Meta.synthInstance] ✅️ apply instMonadEvalTOfMonadEval to MonadEvalT MetaM
+  [Meta.synthInstance.apply] ❌️ apply instMonadEvalT to MonadEvalT MetaM (StateRefT' IO.RealWorld Elab.Term.State MetaM)
+  [Meta.synthInstance.apply] ✅️ apply instMonadEvalTOfMonadEval to MonadEvalT MetaM
         (StateRefT' IO.RealWorld Elab.Term.State MetaM)
     [Meta.synthInstance] new goal MonadEval _tc.1 (StateRefT' IO.RealWorld Elab.Term.State MetaM)
       [Meta.synthInstance.instances] #[@instMonadEvalOfMonadLift]
-  [Meta.synthInstance] ✅️ apply @instMonadEvalOfMonadLift to MonadEval ?m
+  [Meta.synthInstance.apply] ✅️ apply @instMonadEvalOfMonadLift to MonadEval ?m
         (StateRefT' IO.RealWorld Elab.Term.State MetaM)
     [Meta.synthInstance] new goal MonadLift _tc.1 (StateRefT' IO.RealWorld Elab.Term.State MetaM)
       [Meta.synthInstance.instances] #[@StateRefT'.instMonadLift]
-  [Meta.synthInstance] ✅️ apply @StateRefT'.instMonadLift to MonadLift MetaM
+  [Meta.synthInstance.apply] ✅️ apply @StateRefT'.instMonadLift to MonadLift MetaM
         (StateRefT' IO.RealWorld Elab.Term.State MetaM)
     [Meta.synthInstance.answer] ✅️ MonadLift MetaM (StateRefT' IO.RealWorld Elab.Term.State MetaM)
   [Meta.synthInstance.resume] propagating MonadLift MetaM
@@ -64,7 +64,7 @@
     [Meta.synthInstance.resume] size: 2
     [Meta.synthInstance] new goal MonadEvalT MetaM MetaM
       [Meta.synthInstance.instances] #[instMonadEvalTOfMonadEval, instMonadEvalT]
-  [Meta.synthInstance] ✅️ apply instMonadEvalT to MonadEvalT MetaM MetaM
+  [Meta.synthInstance.apply] ✅️ apply instMonadEvalT to MonadEvalT MetaM MetaM
     [Meta.synthInstance.answer] ✅️ MonadEvalT MetaM MetaM
   [Meta.synthInstance.resume] propagating MonadEvalT MetaM
         MetaM to subgoal MonadEvalT MetaM MetaM of MonadEvalT MetaM (StateRefT' IO.RealWorld Elab.Term.State MetaM)
@@ -84,16 +84,16 @@
 [Meta.synthInstance] ✅️ HasCoerce Nat Prop
   [Meta.synthInstance] new goal HasCoerce Nat Prop
     [Meta.synthInstance.instances] #[@coerceTrans]
-  [Meta.synthInstance] ✅️ apply @coerceTrans to HasCoerce Nat Prop
+  [Meta.synthInstance.apply] ✅️ apply @coerceTrans to HasCoerce Nat Prop
     [Meta.synthInstance] new goal HasCoerce _tc.0 Prop
       [Meta.synthInstance.instances] #[@coerceTrans, coerceBoolToProp]
-  [Meta.synthInstance] ✅️ apply coerceBoolToProp to HasCoerce Bool Prop
+  [Meta.synthInstance.apply] ✅️ apply coerceBoolToProp to HasCoerce Bool Prop
     [Meta.synthInstance.answer] ✅️ HasCoerce Bool Prop
   [Meta.synthInstance.resume] propagating HasCoerce Bool Prop to subgoal HasCoerce Bool Prop of HasCoerce Nat Prop
     [Meta.synthInstance.resume] size: 1
     [Meta.synthInstance] new goal HasCoerce Nat Bool
       [Meta.synthInstance.instances] #[@coerceTrans, coerceNatToBool]
-  [Meta.synthInstance] ✅️ apply coerceNatToBool to HasCoerce Nat Bool
+  [Meta.synthInstance.apply] ✅️ apply coerceNatToBool to HasCoerce Nat Bool
     [Meta.synthInstance.answer] ✅️ HasCoerce Nat Bool
   [Meta.synthInstance.resume] propagating HasCoerce Nat Bool to subgoal HasCoerce Nat Bool of HasCoerce Nat Prop
     [Meta.synthInstance.resume] size: 2
@@ -103,11 +103,11 @@
 [Meta.synthInstance] ✅️ MonadEvalT MetaM Elab.Command.CommandElabM
   [Meta.synthInstance] new goal MonadEvalT MetaM Elab.Command.CommandElabM
     [Meta.synthInstance.instances] #[instMonadEvalTOfMonadEval, instMonadEvalT]
-  [Meta.synthInstance] ❌️ apply instMonadEvalT to MonadEvalT MetaM Elab.Command.CommandElabM
-  [Meta.synthInstance] ✅️ apply instMonadEvalTOfMonadEval to MonadEvalT MetaM Elab.Command.CommandElabM
+  [Meta.synthInstance.apply] ❌️ apply instMonadEvalT to MonadEvalT MetaM Elab.Command.CommandElabM
+  [Meta.synthInstance.apply] ✅️ apply instMonadEvalTOfMonadEval to MonadEvalT MetaM Elab.Command.CommandElabM
     [Meta.synthInstance] new goal MonadEval _tc.1 Elab.Command.CommandElabM
       [Meta.synthInstance.instances] #[@instMonadEvalOfMonadLift, Elab.Command.instMonadEvalTermElabMCommandElabM]
-  [Meta.synthInstance] ✅️ apply Elab.Command.instMonadEvalTermElabMCommandElabM to MonadEval Elab.TermElabM
+  [Meta.synthInstance.apply] ✅️ apply Elab.Command.instMonadEvalTermElabMCommandElabM to MonadEval Elab.TermElabM
         Elab.Command.CommandElabM
     [Meta.synthInstance.answer] ✅️ MonadEval Elab.TermElabM Elab.Command.CommandElabM
   [Meta.synthInstance.resume] propagating MonadEval Elab.TermElabM
@@ -116,15 +116,15 @@
     [Meta.synthInstance.resume] size: 1
     [Meta.synthInstance] new goal MonadEvalT MetaM Elab.TermElabM
       [Meta.synthInstance.instances] #[instMonadEvalTOfMonadEval, instMonadEvalT]
-  [Meta.synthInstance] ❌️ apply instMonadEvalT to MonadEvalT MetaM Elab.TermElabM
-  [Meta.synthInstance] ✅️ apply instMonadEvalTOfMonadEval to MonadEvalT MetaM Elab.TermElabM
+  [Meta.synthInstance.apply] ❌️ apply instMonadEvalT to MonadEvalT MetaM Elab.TermElabM
+  [Meta.synthInstance.apply] ✅️ apply instMonadEvalTOfMonadEval to MonadEvalT MetaM Elab.TermElabM
     [Meta.synthInstance] new goal MonadEval _tc.1 Elab.TermElabM
       [Meta.synthInstance.instances] #[@instMonadEvalOfMonadLift]
-  [Meta.synthInstance] ✅️ apply @instMonadEvalOfMonadLift to MonadEval ?m Elab.TermElabM
+  [Meta.synthInstance.apply] ✅️ apply @instMonadEvalOfMonadLift to MonadEval ?m Elab.TermElabM
     [Meta.synthInstance] new goal MonadLift _tc.1 Elab.TermElabM
       [Meta.synthInstance.instances] #[@ReaderT.instMonadLift]
-  [Meta.synthInstance] ✅️ apply @ReaderT.instMonadLift to MonadLift (StateRefT' IO.RealWorld Elab.Term.State MetaM)
-        Elab.TermElabM
+  [Meta.synthInstance.apply] ✅️ apply @ReaderT.instMonadLift to MonadLift
+        (StateRefT' IO.RealWorld Elab.Term.State MetaM) Elab.TermElabM
     [Meta.synthInstance.answer] ✅️ MonadLift (StateRefT' IO.RealWorld Elab.Term.State MetaM) Elab.TermElabM
   [Meta.synthInstance.resume] propagating MonadLift (StateRefT' IO.RealWorld Elab.Term.State MetaM)
         (ReaderT Elab.Term.Context
@@ -139,16 +139,16 @@
     [Meta.synthInstance.resume] size: 2
     [Meta.synthInstance] new goal MonadEvalT MetaM (StateRefT' IO.RealWorld Elab.Term.State MetaM)
       [Meta.synthInstance.instances] #[instMonadEvalTOfMonadEval, instMonadEvalT]
-  [Meta.synthInstance] ❌️ apply instMonadEvalT to MonadEvalT MetaM (StateRefT' IO.RealWorld Elab.Term.State MetaM)
-  [Meta.synthInstance] ✅️ apply instMonadEvalTOfMonadEval to MonadEvalT MetaM
+  [Meta.synthInstance.apply] ❌️ apply instMonadEvalT to MonadEvalT MetaM (StateRefT' IO.RealWorld Elab.Term.State MetaM)
+  [Meta.synthInstance.apply] ✅️ apply instMonadEvalTOfMonadEval to MonadEvalT MetaM
         (StateRefT' IO.RealWorld Elab.Term.State MetaM)
     [Meta.synthInstance] new goal MonadEval _tc.1 (StateRefT' IO.RealWorld Elab.Term.State MetaM)
       [Meta.synthInstance.instances] #[@instMonadEvalOfMonadLift]
-  [Meta.synthInstance] ✅️ apply @instMonadEvalOfMonadLift to MonadEval ?m
+  [Meta.synthInstance.apply] ✅️ apply @instMonadEvalOfMonadLift to MonadEval ?m
         (StateRefT' IO.RealWorld Elab.Term.State MetaM)
     [Meta.synthInstance] new goal MonadLift _tc.1 (StateRefT' IO.RealWorld Elab.Term.State MetaM)
       [Meta.synthInstance.instances] #[@StateRefT'.instMonadLift]
-  [Meta.synthInstance] ✅️ apply @StateRefT'.instMonadLift to MonadLift MetaM
+  [Meta.synthInstance.apply] ✅️ apply @StateRefT'.instMonadLift to MonadLift MetaM
         (StateRefT' IO.RealWorld Elab.Term.State MetaM)
     [Meta.synthInstance.answer] ✅️ MonadLift MetaM (StateRefT' IO.RealWorld Elab.Term.State MetaM)
   [Meta.synthInstance.resume] propagating MonadLift MetaM
@@ -166,7 +166,7 @@
     [Meta.synthInstance.resume] size: 2
     [Meta.synthInstance] new goal MonadEvalT MetaM MetaM
       [Meta.synthInstance.instances] #[instMonadEvalTOfMonadEval, instMonadEvalT]
-  [Meta.synthInstance] ✅️ apply instMonadEvalT to MonadEvalT MetaM MetaM
+  [Meta.synthInstance.apply] ✅️ apply instMonadEvalT to MonadEvalT MetaM MetaM
     [Meta.synthInstance.answer] ✅️ MonadEvalT MetaM MetaM
   [Meta.synthInstance.resume] propagating MonadEvalT MetaM
         MetaM to subgoal MonadEvalT MetaM MetaM of MonadEvalT MetaM (StateRefT' IO.RealWorld Elab.Term.State MetaM)
@@ -186,10 +186,10 @@
 [Meta.synthInstance] ✅️ Bind IO
   [Meta.synthInstance] new goal Bind IO
     [Meta.synthInstance.instances] #[@Monad.toBind]
-  [Meta.synthInstance] ✅️ apply @Monad.toBind to Bind IO
+  [Meta.synthInstance.apply] ✅️ apply @Monad.toBind to Bind IO
     [Meta.synthInstance] new goal Monad IO
       [Meta.synthInstance.instances] #[@instMonadEIO]
-  [Meta.synthInstance] ✅️ apply @instMonadEIO to Monad IO
+  [Meta.synthInstance.apply] ✅️ apply @instMonadEIO to Monad IO
     [Meta.synthInstance.answer] ✅️ Monad IO
   [Meta.synthInstance.resume] propagating Monad (EIO IO.Error) to subgoal Monad IO of Bind IO
     [Meta.synthInstance.resume] size: 1
@@ -199,11 +199,11 @@
 [Meta.synthInstance] ✅️ MonadEvalT MetaM Elab.Command.CommandElabM
   [Meta.synthInstance] new goal MonadEvalT MetaM Elab.Command.CommandElabM
     [Meta.synthInstance.instances] #[instMonadEvalTOfMonadEval, instMonadEvalT]
-  [Meta.synthInstance] ❌️ apply instMonadEvalT to MonadEvalT MetaM Elab.Command.CommandElabM
-  [Meta.synthInstance] ✅️ apply instMonadEvalTOfMonadEval to MonadEvalT MetaM Elab.Command.CommandElabM
+  [Meta.synthInstance.apply] ❌️ apply instMonadEvalT to MonadEvalT MetaM Elab.Command.CommandElabM
+  [Meta.synthInstance.apply] ✅️ apply instMonadEvalTOfMonadEval to MonadEvalT MetaM Elab.Command.CommandElabM
     [Meta.synthInstance] new goal MonadEval _tc.1 Elab.Command.CommandElabM
       [Meta.synthInstance.instances] #[@instMonadEvalOfMonadLift, Elab.Command.instMonadEvalTermElabMCommandElabM]
-  [Meta.synthInstance] ✅️ apply Elab.Command.instMonadEvalTermElabMCommandElabM to MonadEval Elab.TermElabM
+  [Meta.synthInstance.apply] ✅️ apply Elab.Command.instMonadEvalTermElabMCommandElabM to MonadEval Elab.TermElabM
         Elab.Command.CommandElabM
     [Meta.synthInstance.answer] ✅️ MonadEval Elab.TermElabM Elab.Command.CommandElabM
   [Meta.synthInstance.resume] propagating MonadEval Elab.TermElabM
@@ -212,15 +212,15 @@
     [Meta.synthInstance.resume] size: 1
     [Meta.synthInstance] new goal MonadEvalT MetaM Elab.TermElabM
       [Meta.synthInstance.instances] #[instMonadEvalTOfMonadEval, instMonadEvalT]
-  [Meta.synthInstance] ❌️ apply instMonadEvalT to MonadEvalT MetaM Elab.TermElabM
-  [Meta.synthInstance] ✅️ apply instMonadEvalTOfMonadEval to MonadEvalT MetaM Elab.TermElabM
+  [Meta.synthInstance.apply] ❌️ apply instMonadEvalT to MonadEvalT MetaM Elab.TermElabM
+  [Meta.synthInstance.apply] ✅️ apply instMonadEvalTOfMonadEval to MonadEvalT MetaM Elab.TermElabM
     [Meta.synthInstance] new goal MonadEval _tc.1 Elab.TermElabM
       [Meta.synthInstance.instances] #[@instMonadEvalOfMonadLift]
-  [Meta.synthInstance] ✅️ apply @instMonadEvalOfMonadLift to MonadEval ?m Elab.TermElabM
+  [Meta.synthInstance.apply] ✅️ apply @instMonadEvalOfMonadLift to MonadEval ?m Elab.TermElabM
     [Meta.synthInstance] new goal MonadLift _tc.1 Elab.TermElabM
       [Meta.synthInstance.instances] #[@ReaderT.instMonadLift]
-  [Meta.synthInstance] ✅️ apply @ReaderT.instMonadLift to MonadLift (StateRefT' IO.RealWorld Elab.Term.State MetaM)
-        Elab.TermElabM
+  [Meta.synthInstance.apply] ✅️ apply @ReaderT.instMonadLift to MonadLift
+        (StateRefT' IO.RealWorld Elab.Term.State MetaM) Elab.TermElabM
     [Meta.synthInstance.answer] ✅️ MonadLift (StateRefT' IO.RealWorld Elab.Term.State MetaM) Elab.TermElabM
   [Meta.synthInstance.resume] propagating MonadLift (StateRefT' IO.RealWorld Elab.Term.State MetaM)
         (ReaderT Elab.Term.Context
@@ -235,16 +235,16 @@
     [Meta.synthInstance.resume] size: 2
     [Meta.synthInstance] new goal MonadEvalT MetaM (StateRefT' IO.RealWorld Elab.Term.State MetaM)
       [Meta.synthInstance.instances] #[instMonadEvalTOfMonadEval, instMonadEvalT]
-  [Meta.synthInstance] ❌️ apply instMonadEvalT to MonadEvalT MetaM (StateRefT' IO.RealWorld Elab.Term.State MetaM)
-  [Meta.synthInstance] ✅️ apply instMonadEvalTOfMonadEval to MonadEvalT MetaM
+  [Meta.synthInstance.apply] ❌️ apply instMonadEvalT to MonadEvalT MetaM (StateRefT' IO.RealWorld Elab.Term.State MetaM)
+  [Meta.synthInstance.apply] ✅️ apply instMonadEvalTOfMonadEval to MonadEvalT MetaM
         (StateRefT' IO.RealWorld Elab.Term.State MetaM)
     [Meta.synthInstance] new goal MonadEval _tc.1 (StateRefT' IO.RealWorld Elab.Term.State MetaM)
       [Meta.synthInstance.instances] #[@instMonadEvalOfMonadLift]
-  [Meta.synthInstance] ✅️ apply @instMonadEvalOfMonadLift to MonadEval ?m
+  [Meta.synthInstance.apply] ✅️ apply @instMonadEvalOfMonadLift to MonadEval ?m
         (StateRefT' IO.RealWorld Elab.Term.State MetaM)
     [Meta.synthInstance] new goal MonadLift _tc.1 (StateRefT' IO.RealWorld Elab.Term.State MetaM)
       [Meta.synthInstance.instances] #[@StateRefT'.instMonadLift]
-  [Meta.synthInstance] ✅️ apply @StateRefT'.instMonadLift to MonadLift MetaM
+  [Meta.synthInstance.apply] ✅️ apply @StateRefT'.instMonadLift to MonadLift MetaM
         (StateRefT' IO.RealWorld Elab.Term.State MetaM)
     [Meta.synthInstance.answer] ✅️ MonadLift MetaM (StateRefT' IO.RealWorld Elab.Term.State MetaM)
   [Meta.synthInstance.resume] propagating MonadLift MetaM
@@ -262,7 +262,7 @@
     [Meta.synthInstance.resume] size: 2
     [Meta.synthInstance] new goal MonadEvalT MetaM MetaM
       [Meta.synthInstance.instances] #[instMonadEvalTOfMonadEval, instMonadEvalT]
-  [Meta.synthInstance] ✅️ apply instMonadEvalT to MonadEvalT MetaM MetaM
+  [Meta.synthInstance.apply] ✅️ apply instMonadEvalT to MonadEvalT MetaM MetaM
     [Meta.synthInstance.answer] ✅️ MonadEvalT MetaM MetaM
   [Meta.synthInstance.resume] propagating MonadEvalT MetaM
         MetaM to subgoal MonadEvalT MetaM MetaM of MonadEvalT MetaM (StateRefT' IO.RealWorld Elab.Term.State MetaM)
@@ -282,25 +282,25 @@
 [Meta.synthInstance] ✅️ BEq Nat
   [Meta.synthInstance] new goal BEq Nat
     [Meta.synthInstance.instances] #[@instBEqOfDecidableEq, @Std.PreorderPackage.toBEq]
-  [Meta.synthInstance] ✅️ apply @Std.PreorderPackage.toBEq to BEq Nat
+  [Meta.synthInstance.apply] ✅️ apply @Std.PreorderPackage.toBEq to BEq Nat
     [Meta.synthInstance] new goal Std.PreorderPackage Nat
       [Meta.synthInstance.instances] #[@Std.PartialOrderPackage.toPreorderPackage, @Std.LinearPreorderPackage.toPreorderPackage]
-  [Meta.synthInstance] ✅️ apply @Std.LinearPreorderPackage.toPreorderPackage to Std.PreorderPackage Nat
+  [Meta.synthInstance.apply] ✅️ apply @Std.LinearPreorderPackage.toPreorderPackage to Std.PreorderPackage Nat
     [Meta.synthInstance] new goal Std.LinearPreorderPackage Nat
       [Meta.synthInstance.instances] #[@Std.LinearOrderPackage.toLinearPreorderPackage]
-  [Meta.synthInstance] ✅️ apply @Std.LinearOrderPackage.toLinearPreorderPackage to Std.LinearPreorderPackage Nat
+  [Meta.synthInstance.apply] ✅️ apply @Std.LinearOrderPackage.toLinearPreorderPackage to Std.LinearPreorderPackage Nat
     [Meta.synthInstance] no instances for Std.LinearOrderPackage Nat
       [Meta.synthInstance.instances] #[]
-  [Meta.synthInstance] ✅️ apply @Std.PartialOrderPackage.toPreorderPackage to Std.PreorderPackage Nat
+  [Meta.synthInstance.apply] ✅️ apply @Std.PartialOrderPackage.toPreorderPackage to Std.PreorderPackage Nat
     [Meta.synthInstance] new goal Std.PartialOrderPackage Nat
       [Meta.synthInstance.instances] #[@Std.LinearOrderPackage.toPartialOrderPackage]
-  [Meta.synthInstance] ✅️ apply @Std.LinearOrderPackage.toPartialOrderPackage to Std.PartialOrderPackage Nat
+  [Meta.synthInstance.apply] ✅️ apply @Std.LinearOrderPackage.toPartialOrderPackage to Std.PartialOrderPackage Nat
     [Meta.synthInstance] no instances for Std.LinearOrderPackage Nat
       [Meta.synthInstance.instances] #[]
-  [Meta.synthInstance] ✅️ apply @instBEqOfDecidableEq to BEq Nat
+  [Meta.synthInstance.apply] ✅️ apply @instBEqOfDecidableEq to BEq Nat
     [Meta.synthInstance] new goal DecidableEq Nat
       [Meta.synthInstance.instances] #[instDecidableEqNat]
-  [Meta.synthInstance] ✅️ apply instDecidableEqNat to DecidableEq Nat
+  [Meta.synthInstance.apply] ✅️ apply instDecidableEqNat to DecidableEq Nat
     [Meta.synthInstance.answer] ✅️ DecidableEq Nat
   [Meta.synthInstance.resume] propagating DecidableEq Nat to subgoal DecidableEq Nat of BEq Nat
     [Meta.synthInstance.resume] size: 1
diff --git a/tests/elab/trace_synth.lean b/tests/elab/trace_synth.lean
index 04c3dfcc6bad..dabdbe35cafc 100644
--- a/tests/elab/trace_synth.lean
+++ b/tests/elab/trace_synth.lean
@@ -24,7 +24,7 @@ error: failed to synthesize instance of type class
 trace: [Meta.synthInstance] ❌️ Foo "two"
   [Meta.synthInstance] new goal Foo "two"
     [Meta.synthInstance.instances] #[@instFoo_1]
-  [Meta.synthInstance] ✅️ apply @instFoo_1 to Foo "two"
+  [Meta.synthInstance.apply] ✅️ apply @instFoo_1 to Foo "two"
     [Meta.synthInstance.tryResolve] ✅️ Foo "two" ≟ Foo "two"
     [Meta.synthInstance] no instances for Foo "three"
       [Meta.synthInstance.instances] #[]