diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean
index 5ef26737ea..0fd1e185a3 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean
@@ -500,7 +500,7 @@ def checkRing : RingM Bool := do
   modifyRing fun s => { s with recheck := false }
   return true
 
-def check : GoalM Bool := do
+def check : GoalM Bool := do profileitM Exception "grind ring" (← getOptions) do
   if (← checkMaxSteps) then return false
   let mut progress := false
   checkInvariants
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Search.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Search.lean
index 3c58f0b237..79eb02be55 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Search.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Search.lean
@@ -578,7 +578,7 @@ There are two kinds of progress:
 
 The result is `false` if module already has a satisfying assignment.
 -/
-def check : GoalM Bool := do
+def check : GoalM Bool := do profileitM Exception "grind cutsat" (← getOptions) do
   if (← hasAssignment) then
     return false
   else
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Linear/Search.lean b/src/Lean/Meta/Tactic/Grind/Arith/Linear/Search.lean
index 68b0621804..f0f0373528 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Linear/Search.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Linear/Search.lean
@@ -264,7 +264,7 @@ There are two kinds of progress:
 
 The result is `false` if module for every structure already has an assignment.
 -/
-def check : GoalM Bool := do
+def check : GoalM Bool := do profileitM Exception "grind linarith" (← getOptions) do
   let mut progress := false
   for structId in *...(← get').structs.size do
     let r ← LinearM.run structId do
diff --git a/src/Lean/Meta/Tactic/Grind/EMatch.lean b/src/Lean/Meta/Tactic/Grind/EMatch.lean
index 33ffe5ab4b..fd9d7aace4 100644
--- a/src/Lean/Meta/Tactic/Grind/EMatch.lean
+++ b/src/Lean/Meta/Tactic/Grind/EMatch.lean
@@ -553,7 +553,7 @@ end EMatch
 open EMatch
 
 /-- Performs one round of E-matching, and returns new instances. -/
-private def ematchCore : GoalM Unit := do
+private def ematchCore : GoalM Unit := do profileitM Exception "grind ematch" (← getOptions) do
   let go (thms newThms : PArray EMatchTheorem) : EMatch.M Unit := do
     withReader (fun ctx => { ctx with useMT := true }) <| ematchTheorems thms
     withReader (fun ctx => { ctx with useMT := false }) <| ematchTheorems newThms