diff --git a/src/Lean/Elab/GuardMsgs.lean b/src/Lean/Elab/GuardMsgs.lean
index 9a0017f23c..fc730335fa 100644
--- a/src/Lean/Elab/GuardMsgs.lean
+++ b/src/Lean/Elab/GuardMsgs.lean
@@ -163,7 +163,7 @@ def MessageOrdering.apply (mode : MessageOrdering) (msgs : List String) : List S
           let diff := Diff.diff (expected.split (· == '\n')).toArray (res.split (· == '\n')).toArray
           Diff.linesToString diff
         else res
-      logErrorAt tk m!"❌ Docstring on `#guard_msgs` does not match generated message:\n\n{feedback}"
+      logErrorAt tk m!"❌️ Docstring on `#guard_msgs` does not match generated message:\n\n{feedback}"
       pushInfoLeaf (.ofCustomInfo { stx := ← getRef, value := Dynamic.mk (GuardMsgFailure.mk res) })
   | _ => throwUnsupportedSyntax
 
diff --git a/src/Lean/Util/Trace.lean b/src/Lean/Util/Trace.lean
index 8e09295b56..3aa659337e 100644
--- a/src/Lean/Util/Trace.lean
+++ b/src/Lean/Util/Trace.lean
@@ -294,9 +294,9 @@ macro "trace[" id:ident "]" s:(interpolatedStr(term) <|> term) : doElem => do
     if (← Lean.isTracingEnabledFor cls) then
       Lean.addTrace cls $msg)
 
-def bombEmoji := "💥"
-def checkEmoji := "✅"
-def crossEmoji := "❌"
+def bombEmoji := "💥️"
+def checkEmoji := "✅️"
+def crossEmoji := "❌️"
 
 def exceptBoolEmoji : Except ε Bool → String
   | .error _ => bombEmoji
@@ -326,7 +326,7 @@ instance : ExceptToEmoji ε (Option α) where
 Similar to `withTraceNode`, but msg is constructed **before** executing `k`.
 This is important when debugging methods such as `isDefEq`, and we want to generate the message
 before `k` updates the metavariable assignment. The class `ExceptToEmoji` is used to convert
-the result produced by `k` into an emoji (e.g., `💥`, `✅`, `❌`).
+the result produced by `k` into an emoji (e.g., `💥️`, `✅️`, `❌️`).
 
 TODO: find better name for this function.
 -/
diff --git a/tests/lean/366.lean.expected.out b/tests/lean/366.lean.expected.out
index 966e0ef9b9..190dcd528a 100644
--- a/tests/lean/366.lean.expected.out
+++ b/tests/lean/366.lean.expected.out
@@ -1,7 +1,7 @@
-[Meta.synthInstance] ✅ Inhabited Nat
+[Meta.synthInstance] ✅️ Inhabited Nat
   [Meta.synthInstance] new goal Inhabited Nat
     [Meta.synthInstance.instances] #[@instInhabitedOfMonad, instInhabitedNat]
-  [Meta.synthInstance] ✅ apply instInhabitedNat to Inhabited Nat
-    [Meta.synthInstance.tryResolve] ✅ Inhabited Nat ≟ Inhabited Nat
-    [Meta.synthInstance.answer] ✅ Inhabited Nat
+  [Meta.synthInstance] ✅️ 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/lean/815b.lean.expected.out b/tests/lean/815b.lean.expected.out
index 3d5fe6616d..6642d853a3 100644
--- a/tests/lean/815b.lean.expected.out
+++ b/tests/lean/815b.lean.expected.out
@@ -5,19 +5,19 @@
 815b.lean:9:9-9:13: warning: declaration uses 'sorry'
 815b.lean:10:9-10:13: warning: declaration uses 'sorry'
 815b.lean:11:9-11:13: warning: declaration uses 'sorry'
-[Meta.synthInstance] ✅ IsSmooth fun g a => f (g a) d
+[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.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.tryResolve] ✅ IsSmooth fun g a => f (g a) d ≟ IsSmooth fun b a => f (b a) d
+  [Meta.synthInstance] ❌️ 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.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.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.tryResolve] ✅ IsSmooth fun g => f (g a) d ≟ IsSmooth fun a_1 => f (a_1 a) d
+  [Meta.synthInstance] ❌️ 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.tryResolve] ✅️ IsSmooth fun g => f (g a) d ≟ IsSmooth fun a_1 => f (a_1 a) d
     [Meta.synthInstance.unusedArgs] α → IsSmooth f
         has unused arguments, reduced type
           IsSmooth f
@@ -25,9 +25,9 @@
           fun redf a => redf
     [Meta.synthInstance] new goal IsSmooth f
       [Meta.synthInstance.instances] #[inst✝]
-  [Meta.synthInstance] ✅ apply inst✝ to IsSmooth f
-    [Meta.synthInstance.tryResolve] ✅ IsSmooth f ≟ IsSmooth f
-    [Meta.synthInstance.answer] ✅ IsSmooth f
+  [Meta.synthInstance] ✅️ 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
     [Meta.synthInstance.resume] size: 1
     [Meta.synthInstance.unusedArgs] α → IsSmooth f
@@ -45,24 +45,24 @@
           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.tryResolve] ❌ IsSmooth (f b) ≟ IsSmooth f
-  [Meta.synthInstance] ❌ 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.tryResolve] ✅ IsSmooth fun g => f (g a) d ≟ IsSmooth fun a_1 => f (a_1 a) d
+  [Meta.synthInstance] ❌️ 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.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.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.tryResolve] ❌ IsSmooth fun g => f (g a) ≟ IsSmooth f
-  [Meta.synthInstance] ✅ 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] ❌️ 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.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.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.tryResolve] ✅ IsSmooth fun g => f (g a✝) a ≟ IsSmooth fun a_1 => f (a_1 a✝) a
+  [Meta.synthInstance] ❌️ 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.tryResolve] ✅️ IsSmooth fun g => f (g a✝) a ≟ IsSmooth fun a_1 => f (a_1 a✝) a
     [Meta.synthInstance.unusedArgs] α → δ → IsSmooth f
         has unused arguments, reduced type
           IsSmooth f
@@ -76,24 +76,25 @@
           ∀ (b : β), IsSmooth (f b)
         Transformer
           fun redf a a => redf
-  [Meta.synthInstance] ❌ 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.tryResolve] ✅ IsSmooth fun g => f (g a✝) a ≟ IsSmooth fun a_1 => f (a_1 a✝) a
+  [Meta.synthInstance] ❌️ 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.tryResolve] ✅️ IsSmooth fun g => f (g a✝) a ≟ IsSmooth fun a_1 => f (a_1 a✝) a
     [Meta.synthInstance.unusedArgs] ∀ (a : α), δ → 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.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.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.tryResolve] ❌ IsSmooth fun g =>
+  [Meta.synthInstance] ❌️ 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.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.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.tryResolve] ✅ IsSmooth fun g => f (g a) ≟ IsSmooth fun a_1 => f (a_1 a)
+  [Meta.synthInstance] ✅️ 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] α → IsSmooth f
         has unused arguments, reduced type
           IsSmooth f
@@ -104,15 +105,15 @@
     [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.tryResolve] ❌ IsSmooth fun g => g a ≟ IsSmooth f
-  [Meta.synthInstance] ❌ apply @diag to ∀ (a : α), IsSmooth fun g => g a
-    [Meta.synthInstance.tryResolve] ❌ IsSmooth fun g =>
+  [Meta.synthInstance] ❌️ 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.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.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.tryResolve] ✅ IsSmooth fun g => g a ≟ IsSmooth fun a_1 => a_1 a
+  [Meta.synthInstance] ❌️ 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.tryResolve] ✅️ IsSmooth fun g => g a ≟ IsSmooth fun a_1 => a_1 a
     [Meta.synthInstance.unusedArgs] α → IsSmooth fun g => g
         has unused arguments, reduced type
           IsSmooth fun g => g
@@ -120,21 +121,21 @@
           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.tryResolve] ❌ IsSmooth fun g => g ≟ IsSmooth f
-  [Meta.synthInstance] ✅ 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.tryResolve] ❌ IsSmooth fun g => g ≟ IsSmooth fun a => ?m (?m a) (?m a)
-  [Meta.synthInstance] ❌ 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.tryResolve] ❌ IsSmooth fun g => g ≟ IsSmooth fun a => ?m a ?m
-  [Meta.synthInstance] ❌ 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.tryResolve] ✅ IsSmooth fun g => g ≟ IsSmooth fun a => a
-    [Meta.synthInstance.answer] ✅ IsSmooth fun g => g
+  [Meta.synthInstance] ❌️ 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.tryResolve] ✅️ IsSmooth fun g => g ≟ IsSmooth fun b a => b a
+  [Meta.synthInstance] ❌️ 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.tryResolve] ❌️ IsSmooth fun g => g ≟ IsSmooth fun a => ?m (?m a)
+  [Meta.synthInstance] ❌️ 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.tryResolve] ❌️ IsSmooth fun g => g ≟ IsSmooth fun a => ?m
+  [Meta.synthInstance] ✅️ 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 =>
         a to subgoal IsSmooth fun g => g of ∀ (a : α), IsSmooth fun g => g a
     [Meta.synthInstance.resume] size: 1
@@ -146,11 +147,11 @@
   [Meta.synthInstance.resume] propagating α →
         IsSmooth fun a => a to subgoal α → IsSmooth fun g => g of ∀ (a : α), IsSmooth fun g => g a
     [Meta.synthInstance.resume] size: 2
-    [Meta.synthInstance.answer] ✅ ∀ (a : α), IsSmooth fun g => g a
+    [Meta.synthInstance.answer] ✅️ ∀ (a : α), IsSmooth fun g => g a
   [Meta.synthInstance.resume] propagating ∀ (a : α),
         IsSmooth fun a_1 => a_1 a to subgoal ∀ (a : α), IsSmooth fun g => g a of IsSmooth fun g => g
     [Meta.synthInstance.resume] size: 3
-    [Meta.synthInstance.answer] ✅ IsSmooth fun g => g
+    [Meta.synthInstance.answer] ✅️ IsSmooth fun g => g
   [Meta.synthInstance.resume] propagating IsSmooth fun b a =>
         b a to subgoal IsSmooth fun g => g of ∀ (a : α), IsSmooth fun g => g a
     [Meta.synthInstance.resume] size: 4
@@ -162,23 +163,23 @@
   [Meta.synthInstance.resume] propagating α →
         IsSmooth fun b a => b a to subgoal α → IsSmooth fun g => g of ∀ (a : α), IsSmooth fun g => g a
     [Meta.synthInstance.resume] size: 8
-    [Meta.synthInstance.answer] ✅ ∀ (a : α), IsSmooth fun g => g a
+    [Meta.synthInstance.answer] ✅️ ∀ (a : α), IsSmooth fun g => g a
   [Meta.synthInstance.resume] propagating α →
         IsSmooth fun a => a to subgoal α → IsSmooth fun g => g of ∀ (a : α), IsSmooth fun g => g a
     [Meta.synthInstance.resume] size: 5
-    [Meta.synthInstance.answer] ✅ ∀ (a : α), IsSmooth fun g => g a
+    [Meta.synthInstance.answer] ✅️ ∀ (a : α), IsSmooth fun g => g a
   [Meta.synthInstance.resume] propagating ∀ (a : α),
         IsSmooth fun a_1 => a_1 a to subgoal ∀ (a : α), IsSmooth fun g => g a of ∀ (a : α), IsSmooth fun g => f (g a)
     [Meta.synthInstance.resume] size: 4
-    [Meta.synthInstance.answer] ✅ ∀ (a : α), IsSmooth fun g => f (g a)
+    [Meta.synthInstance.answer] ✅️ ∀ (a : α), IsSmooth fun g => f (g a)
   [Meta.synthInstance.resume] propagating ∀ (a : α),
         IsSmooth fun a_1 =>
           f (a_1 a) to subgoal ∀ (a : α), IsSmooth fun g => f (g a) of ∀ (a : α), IsSmooth fun g => f (g a) d
     [Meta.synthInstance.resume] size: 5
-    [Meta.synthInstance.answer] ✅ ∀ (a : α), IsSmooth fun g => f (g a) d
+    [Meta.synthInstance.answer] ✅️ ∀ (a : α), IsSmooth fun g => f (g a) d
   [Meta.synthInstance.resume] propagating ∀ (a : α),
         IsSmooth fun a_1 =>
           f (a_1 a) d to subgoal ∀ (a : α), IsSmooth fun g => f (g a) d of IsSmooth fun g a => f (g a) d
     [Meta.synthInstance.resume] size: 6
-    [Meta.synthInstance.answer] ✅ IsSmooth fun g a => f (g a) d
+    [Meta.synthInstance.answer] ✅️ IsSmooth fun g a => f (g a) d
   [Meta.synthInstance] result swap fun a g => f (g a) d
diff --git a/tests/lean/973b.lean.expected.out b/tests/lean/973b.lean.expected.out
index f68dd13270..0cd8213d49 100644
--- a/tests/lean/973b.lean.expected.out
+++ b/tests/lean/973b.lean.expected.out
@@ -1,5 +1,5 @@
 973b.lean:5:8-5:10: warning: declaration uses 'sorry'
 973b.lean:9:8-9:11: warning: declaration uses 'sorry'
-[Meta.Tactic.simp.discharge] ex discharge ❌
+[Meta.Tactic.simp.discharge] ex discharge ❌️
       ?p x
-[Meta.Tactic.simp.discharge] ex discharge ❌ ?p (f x)
+[Meta.Tactic.simp.discharge] ex discharge ❌️ ?p (f x)
diff --git a/tests/lean/etaReducedMvarAssignments.lean.expected.out b/tests/lean/etaReducedMvarAssignments.lean.expected.out
index b85fc4033b..3b6a3a78d2 100644
--- a/tests/lean/etaReducedMvarAssignments.lean.expected.out
+++ b/tests/lean/etaReducedMvarAssignments.lean.expected.out
@@ -1,4 +1,4 @@
 Pi.hasLe : LE ((i : ι) → α i)
-[Meta.isDefEq.assign] ✅ ?m i := α i
+[Meta.isDefEq.assign] ✅️ ?m i := α i
   [Meta.isDefEq.assign.beforeMkLambda] ?m [i] := α i
-  [Meta.isDefEq.assign.checkTypes] ✅ (?m : ι → Type ?u) := (α : ι → Type v)
+  [Meta.isDefEq.assign.checkTypes] ✅️ (?m : ι → Type ?u) := (α : ι → Type v)
diff --git a/tests/lean/infoFromFailure.lean.expected.out b/tests/lean/infoFromFailure.lean.expected.out
index ca2ea71f6f..07b76cedc6 100644
--- a/tests/lean/infoFromFailure.lean.expected.out
+++ b/tests/lean/infoFromFailure.lean.expected.out
@@ -1,9 +1,9 @@
 B.foo "hello" : String × String
-[Meta.synthInstance] ❌ Add String
+[Meta.synthInstance] ❌️ Add String
   [Meta.synthInstance] no instances for Add String
     [Meta.synthInstance.instances] #[]
   [Meta.synthInstance] result <not-available>
-[Meta.synthInstance] ❌ Add Bool
+[Meta.synthInstance] ❌️ Add Bool
   [Meta.synthInstance] no instances for Add Bool
     [Meta.synthInstance.instances] #[]
   [Meta.synthInstance] result <not-available>
diff --git a/tests/lean/run/1234.lean b/tests/lean/run/1234.lean
index e026411a36..825378b8cd 100644
--- a/tests/lean/run/1234.lean
+++ b/tests/lean/run/1234.lean
@@ -10,7 +10,7 @@ set_option trace.Meta.Tactic.simp true
 warning: declaration uses 'sorry'
 ---
 info: [Meta.Tactic.simp.rewrite] h₁:1000, k ≤ v - 1 ==> True
-[Meta.Tactic.simp.discharge] succ_pred_eq_of_pos discharge ✅
+[Meta.Tactic.simp.discharge] succ_pred_eq_of_pos discharge ✅️
       0 < v
   [Meta.Tactic.simp.rewrite] h₂:1000, 0 < v ==> True
 [Meta.Tactic.simp.rewrite] succ_pred_eq_of_pos:1000, v - 1 + 1 ==> v
@@ -35,7 +35,7 @@ example (h₁: k ≤ v - 1) (h₂: 0 < v):
 warning: declaration uses 'sorry'
 ---
 info: [Meta.Tactic.simp.rewrite] h₁:1000, k ≤ v - 1 ==> True
-[Meta.Tactic.simp.discharge] succ_pred_eq_of_pos discharge ✅
+[Meta.Tactic.simp.discharge] succ_pred_eq_of_pos discharge ✅️
       0 < v
   [Meta.Tactic.simp.rewrite] h₂:1000, 0 < v ==> True
 [Meta.Tactic.simp.rewrite] succ_pred_eq_of_pos:1000, v - 1 + 1 ==> v
@@ -58,7 +58,7 @@ example (h₁: k ≤ v - 1) (h₂: 0 < v):
 warning: declaration uses 'sorry'
 ---
 info: [Meta.Tactic.simp.rewrite] h₁:1000, k ≤ v - 1 ==> True
-[Meta.Tactic.simp.discharge] succ_pred_eq_of_pos discharge ✅
+[Meta.Tactic.simp.discharge] succ_pred_eq_of_pos discharge ✅️
       0 < v
   [Meta.Tactic.simp.rewrite] h₂:1000, 0 < v ==> True
 [Meta.Tactic.simp.rewrite] succ_pred_eq_of_pos:1000, v - 1 + 1 ==> v
diff --git a/tests/lean/run/1380.lean b/tests/lean/run/1380.lean
index 23fea60c85..61516a9fe3 100644
--- a/tests/lean/run/1380.lean
+++ b/tests/lean/run/1380.lean
@@ -12,7 +12,7 @@ info: [Meta.Tactic.simp.unify] eq_self:1000, failed to unify
       ?a = ?a
     with
       v₂ = v₁
-[Meta.Tactic.simp.discharge] Nat.ne_of_gt discharge ✅
+[Meta.Tactic.simp.discharge] Nat.ne_of_gt discharge ✅️
       v₁ < v₂
   [Meta.Tactic.simp.rewrite] hv:1000, v₁ < v₂ ==> True
 [Meta.Tactic.simp.rewrite] Nat.ne_of_gt:1000, v₂ = v₁ ==> False
diff --git a/tests/lean/run/3257.lean b/tests/lean/run/3257.lean
index e56a7dc79a..d7ef79a43d 100644
--- a/tests/lean/run/3257.lean
+++ b/tests/lean/run/3257.lean
@@ -14,7 +14,7 @@ example : U := by
   simp [foo, T.mk]
 
 /--
-info: [Meta.Tactic.simp.discharge] bar discharge ✅
+info: [Meta.Tactic.simp.discharge] bar discharge ✅️
       autoParam T _auto✝
   [Meta.Tactic.simp.rewrite] T.mk:1000, T ==> True
 [Meta.Tactic.simp.rewrite] bar:1000, U ==> True
diff --git a/tests/lean/run/guard_msgs.lean b/tests/lean/run/guard_msgs.lean
index 4d8d5cc255..c2039186e5 100644
--- a/tests/lean/run/guard_msgs.lean
+++ b/tests/lean/run/guard_msgs.lean
@@ -8,7 +8,7 @@ example : α := x
 /--
 error: unknown identifier 'x'
 ---
-error: ❌ Docstring on `#guard_msgs` does not match generated message:
+error: ❌️ Docstring on `#guard_msgs` does not match generated message:
 
 error: unknown identifier 'x'
 -/
@@ -62,7 +62,7 @@ example : α := 22
 info: foo ⏎
 bar
 ---
-error: ❌ Docstring on `#guard_msgs` does not match generated message:
+error: ❌️ Docstring on `#guard_msgs` does not match generated message:
 
 info: foo ⏎
 bar
@@ -83,7 +83,7 @@ run_meta Lean.logInfo "foo \nbar"
 info: foo ⏎⏎
 bar
 ---
-error: ❌ Docstring on `#guard_msgs` does not match generated message:
+error: ❌️ Docstring on `#guard_msgs` does not match generated message:
 
 info: foo ⏎⏎
 bar
@@ -170,7 +170,7 @@ info: ABCDEFG
 HIJKLMNOP
 QRSTUVWXYZ
 ---
-error: ❌ Docstring on `#guard_msgs` does not match generated message:
+error: ❌️ Docstring on `#guard_msgs` does not match generated message:
 
 -
 + info: ABCDEFG
@@ -187,7 +187,7 @@ info: ABCDEFG
 HIJKLMNOP
 QRSTUVWXYZ
 ---
-error: ❌ Docstring on `#guard_msgs` does not match generated message:
+error: ❌️ Docstring on `#guard_msgs` does not match generated message:
 
   info: ABCDEFG
 + HIJKLMNOP
@@ -237,7 +237,7 @@ info: Tree.branch
     4
     (Tree.branch (Tree.branch (Tree.leaf 0) 1 (Tree.leaf 0)) 2 (Tree.branch (Tree.leaf 0) 1 (Tree.leaf 0))))
 ---
-error: ❌ Docstring on `#guard_msgs` does not match generated message:
+error: ❌️ Docstring on `#guard_msgs` does not match generated message:
 
   info: Tree.branch
     (Tree.branch