fix: patch for std4#193 (#6188)

fix: patch for std4#193

Mathlib/Init/Data/Nat/Lemmas.lean

@@ -500,15 +500,6 @@ def subInduction {P : ℕ → ℕ → Sort u} (H1 : ∀ m, P 0 m) (H2 : ∀ n, P
   | succ n, succ m => H3 _ _ (subInduction H1 H2 H3 n m)
 #align nat.sub_induction Nat.subInduction
 
-protected def strongRecOn {p : Nat → Sort u} (n : Nat) (h : ∀ n, (∀ m, m < n → p m) → p n) :
-    p n := by
-  suffices ∀ n m, m < n → p m from this (succ n) n (lt_succ_self _)
-  intro n; induction' n with n ih
-  · intro m h₁; exact absurd h₁ m.not_lt_zero
-  · intro m h₁
-    apply Or.by_cases (Decidable.lt_or_eq_of_le (le_of_lt_succ h₁))
-    · intros; apply ih; assumption
-    · intros; subst m; apply h _ ih
 #align nat.strong_rec_on Nat.strongRecOn
 
 -- porting note: added `elab_as_elim`

lake-manifest.json

@@ -28,6 +28,6 @@
   {"git":
    {"url": "https://github.com/leanprover/std4",
     "subDir?": null,
-    "rev": "dbffa8cb31b0c51b151453c4ff8f00ede2a84ed8",
+    "rev": "8b864260672b21d964d79ecb2376e01d0eab9f5b",
     "name": "std",
     "inputRev?": "main"}}]}