feat: measureRec for strong induction use cases (#829)

* feat: `Nat.strongRecOnMeasure`

Co-Authored-By: Joachim Breitner <[email protected]>

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`
 -/