From 5f5c4e1885bf283680af7bf0ca6c3eecde68f961 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20G=2E=20Dorais?= <fgdorais@gmail.com>
Date: Thu, 17 Aug 2023 10:19:52 +0000
Subject: [PATCH] fix: patch for std4#193 (#6188)

fix: patch for std4#193
---
 Mathlib/Init/Data/Nat/Lemmas.lean | 9 ---------
 lake-manifest.json                | 2 +-
 2 files changed, 1 insertion(+), 10 deletions(-)

diff --git a/Mathlib/Init/Data/Nat/Lemmas.lean b/Mathlib/Init/Data/Nat/Lemmas.lean
index c9ee09bb8d9a4..92a6b32d55518 100644
--- a/Mathlib/Init/Data/Nat/Lemmas.lean
+++ b/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`
diff --git a/lake-manifest.json b/lake-manifest.json
index c756fe0b74dc9..5f0c320319014 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -28,6 +28,6 @@
   {"git":
    {"url": "https://github.com/leanprover/std4",
     "subDir?": null,
-    "rev": "dbffa8cb31b0c51b151453c4ff8f00ede2a84ed8",
+    "rev": "8b864260672b21d964d79ecb2376e01d0eab9f5b",
     "name": "std",
     "inputRev?": "main"}}]}