From 4f800f7654dce22e06f8f1a9f99ea379361c8693 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott@tqft.net>
Date: Wed, 24 Jan 2024 11:48:18 +0000
Subject: [PATCH] chore: adaptations for nightly-2024-01-23 (#9960)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
---
 Mathlib/Init/Data/Int/Basic.lean  | 2 +-
 Mathlib/Init/Data/Int/Lemmas.lean | 2 +-
 lake-manifest.json                | 6 +++---
 lakefile.lean                     | 2 +-
 lean-toolchain                    | 2 +-
 5 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/Mathlib/Init/Data/Int/Basic.lean b/Mathlib/Init/Data/Int/Basic.lean
index 52d5637513cbc..64e97441b1ea8 100644
--- a/Mathlib/Init/Data/Int/Basic.lean
+++ b/Mathlib/Init/Data/Int/Basic.lean
@@ -7,7 +7,7 @@ The integers, with addition, multiplication, and subtraction.
 -/
 import Mathlib.Mathport.Rename
 import Mathlib.Init.Data.Nat.Notation
-import Std.Data.Int.Lemmas
+import Std.Data.Int.Order
 
 open Nat
 
diff --git a/Mathlib/Init/Data/Int/Lemmas.lean b/Mathlib/Init/Data/Int/Lemmas.lean
index 31803bd249387..d19ff4b4b307e 100644
--- a/Mathlib/Init/Data/Int/Lemmas.lean
+++ b/Mathlib/Init/Data/Int/Lemmas.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
 -/
 
-import Std.Data.Int.Lemmas
+import Std.Data.Int.Order
 import Mathlib.Mathport.Rename
 
 /-!
diff --git a/lake-manifest.json b/lake-manifest.json
index 8a83c2b2f9846..8ab84cb9c4e7e 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "427cf7ea160ef0c2c10fbe92102a2f470b9d74ad",
+   "rev": "c6c85991538681aa7eb8a8cca6f15038b022bbc4",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "bump/v4.6.0",
@@ -31,10 +31,10 @@
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "8dd18350791c85c0fc9adbd6254c94a81d260d35",
+   "rev": "9466e2c665dd81f8c9bdd2e27b67c1cac0145571",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.25",
+   "inputRev": "v0.0.26-pre",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
diff --git a/lakefile.lean b/lakefile.lean
index a3b04edf0a26d..e5b1fbc0526ad 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -29,7 +29,7 @@ require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"
 require std from git "https://github.com/leanprover/std4" @ "bump/v4.6.0"
 require Qq from git "https://github.com/leanprover-community/quote4" @ "master"
 require aesop from git "https://github.com/leanprover-community/aesop" @ "bump/v4.6.0"
-require proofwidgets from git "https://github.com/leanprover-community/ProofWidgets4" @ "v0.0.25"
+require proofwidgets from git "https://github.com/leanprover-community/ProofWidgets4" @ "v0.0.26-pre"
 require Cli from git "https://github.com/leanprover/lean4-cli" @ "main"
 require importGraph from git "https://github.com/leanprover-community/import-graph.git" @ "main"
 
diff --git a/lean-toolchain b/lean-toolchain
index 271fe10f7dbb4..b39e2129f7686 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2024-01-22
+leanprover/lean4:nightly-2024-01-23