diff --git a/src/Init/Grind/Util.lean b/src/Init/Grind/Util.lean
index 3175e74a06..fb17f67a6a 100644
--- a/src/Init/Grind/Util.lean
+++ b/src/Init/Grind/Util.lean
@@ -78,6 +78,19 @@ def offsetUnexpander : PrettyPrinter.Unexpander := fun stx => do
   | `($_ $lhs:term $rhs:term) => `($lhs + $rhs)
   | _ => throw ()
 
+/-
+Remark: `↑a` is notation for `Nat.cast a`. `Nat.cast` is an abbreviation
+for `NatCast.natCast`. We added it because users wanted to use dot-notation (e.g., `a.cast`).
+`grind` expands all reducible definitions. Thus, a `grind` failure state contains
+many `NatCast.natCast` applications which is too verbose. We add the following
+unexpander to cope with this issue.
+-/
+@[app_unexpander NatCast.natCast]
+def natCastUnexpander : PrettyPrinter.Unexpander := fun stx => do
+  match stx with
+  | `($_ $a:term) => `(↑$a)
+  | _ => throw ()
+
 /--
 A marker to indicate that a proposition has already been normalized and should not
 be processed again.
diff --git a/tests/lean/run/grind_canon_insts.lean b/tests/lean/run/grind_canon_insts.lean
index 8f31c8e0d6..080f02c7dd 100644
--- a/tests/lean/run/grind_canon_insts.lean
+++ b/tests/lean/run/grind_canon_insts.lean
@@ -59,11 +59,11 @@ def fallback : Fallback := do
 set_option trace.Meta.debug true
 
 /--
-info: [Meta.debug] [NatCast.natCast a * (NatCast.natCast b * NatCast.natCast c),
-     NatCast.natCast b * NatCast.natCast c,
-     NatCast.natCast d * (NatCast.natCast b * NatCast.natCast c),
-     -1 * (NatCast.natCast a * (NatCast.natCast b * NatCast.natCast c)),
-     -1 * (NatCast.natCast d * (NatCast.natCast b * NatCast.natCast c)),
+info: [Meta.debug] [↑a * (↑b * ↑c),
+     ↑b * ↑c,
+     ↑d * (↑b * ↑c),
+     -1 * (↑a * (↑b * ↑c)),
+     -1 * (↑d * (↑b * ↑c)),
      a * (b * c),
      b * c,
      d * (b * c)]
diff --git a/tests/lean/run/grind_eq.lean b/tests/lean/run/grind_eq.lean
index bb785be30b..c3d74f7a79 100644
--- a/tests/lean/run/grind_eq.lean
+++ b/tests/lean/run/grind_eq.lean
@@ -72,7 +72,7 @@ info: [grind.assert] x1 = appV a_2 b
 [grind.assert] ¬HEq x2 x4
 [grind.ematch.instance] appV_assoc: HEq (appV a_2 (appV b c)) (appV (appV a_2 b) c)
 [grind.assert] HEq (appV a_2 (appV b c)) (appV (appV a_2 b) c)
-[grind.assert] -1 * NatCast.natCast a ≤ 0
+[grind.assert] -1 * ↑a ≤ 0
 -/
 #guard_msgs (info) in
 example : x1 = appV a b → x2 = appV x1 c → x3 = appV b c → x4 = appV a x3 → HEq x2 x4 := by
diff --git a/tests/lean/run/grind_offset.lean b/tests/lean/run/grind_offset.lean
index 29335f370b..2b3f1ec6a1 100644
--- a/tests/lean/run/grind_offset.lean
+++ b/tests/lean/run/grind_offset.lean
@@ -51,7 +51,7 @@ info: [grind.assert] f (c + 2) = a
 [grind.assert] ¬a = g (g (f c))
 [grind.ematch.instance] f.eq_2: f (c + 1).succ = g (f (c + 1))
 [grind.assert] f (c + 2) = g (f (c + 1))
-[grind.assert] -1 * NatCast.natCast c ≤ 0
+[grind.assert] -1 * ↑c ≤ 0
 [grind.ematch.instance] f.eq_2: f c.succ = g (f c)
 [grind.assert] f (c + 1) = g (f c)
 -/
@@ -77,8 +77,8 @@ info: [grind.assert] foo (c + 1) = a
 [grind.assert] ¬a = g (foo b)
 [grind.ematch.instance] foo.eq_3: foo b.succ.succ = g (foo b)
 [grind.assert] foo (b + 2) = g (foo b)
-[grind.assert] -1 * NatCast.natCast b ≤ 0
-[grind.assert] -1 * NatCast.natCast c ≤ 0
+[grind.assert] -1 * ↑b ≤ 0
+[grind.assert] -1 * ↑c ≤ 0
 -/
 #guard_msgs (info) in
 example : foo (c + 1) = a → c = b + 1 → a = g (foo b) := by