diff --git a/Batteries/Data/Nat/Basic.lean b/Batteries/Data/Nat/Basic.lean
index 9f7c7d8f36..a6e55a6ea2 100644
--- a/Batteries/Data/Nat/Basic.lean
+++ b/Batteries/Data/Nat/Basic.lean
@@ -28,6 +28,15 @@ protected def strongRec {motive : Nat → Sort _} (ind : ∀ n, (∀ m, m < n 
 protected def strongRecOn (t : Nat) {motive : Nat → Sort _}
   (ind : ∀ n, (∀ m, m < n → motive m) → motive n) : motive t := Nat.strongRec ind t
 
+/--
+  Strong recursor via a `Nat`-valued measure
+-/
+@[elab_as_elim]
+def strongRecMeasure (f : α → Nat) {motive : α → Sort _}
+    (ind : ∀ x, (∀ y, f y < f x → motive y) → motive x) (x : α) : motive x :=
+  ind x fun y _ => strongRecMeasure f ind y
+termination_by f x
+
 /--
   Simple diagonal recursor for `Nat`
 -/