diff --git a/Mathlib/Util/SleepHeartbeats.lean b/Mathlib/Util/SleepHeartbeats.lean
index f6cb76c320e8dc..306b2fa284f05c 100644
--- a/Mathlib/Util/SleepHeartbeats.lean
+++ b/Mathlib/Util/SleepHeartbeats.lean
@@ -30,8 +30,10 @@ def sleepAtLeastHeartbeats (n : Nat) : IO Unit := do
 elab "sleep_heartbeats " n:num : tactic => do
   match Syntax.isNatLit? n with
   | none    => throwIllFormedSyntax
-  /- as this is a user facing command we multiply the user input by 1000 to match the maxHeartbeats
-     option -/
+  /-
+  We multiply by `1000` to convert the user-facing heartbeat count to the
+  internal heartbeat counter used by `IO.getNumHeartbeats`.
+  -/
   | some m => sleepAtLeastHeartbeats (m * 1000)
 
 example : 1 = 1 := by