diff --git a/Mathlib/Data/Int/Basic.lean b/Mathlib/Data/Int/Basic.lean
index 698e503bec8d3..be0dd2169bc10 100644
--- a/Mathlib/Data/Int/Basic.lean
+++ b/Mathlib/Data/Int/Basic.lean
@@ -140,9 +140,6 @@ theorem sign_coe_add_one (n : ℕ) : Int.sign (n + 1) = 1 :=
   rfl
 #align int.sign_coe_add_one Int.sign_coe_add_one
 
-@[simp]
-theorem sign_negSucc (n : ℕ) : Int.sign -[n+1] = -1 :=
-  rfl
 #align int.sign_neg_succ_of_nat Int.sign_negSucc
 
 /-! ### succ and pred -/
diff --git a/lake-manifest.json b/lake-manifest.json
index 3c77bd579f439..cd84b28dab14e 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "b197bd218dbab248ad8899404334d41da04f5d13",
+   "rev": "604b4078d46104d4144a87ebf4c2dae581cb704a",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",