From b24dc53e95affe6bce70ba4a1fedf90060100f88 Mon Sep 17 00:00:00 2001
From: Tobias Grosser <tobias@grosser.es>
Date: Wed, 25 Sep 2024 21:07:01 +0100
Subject: [PATCH] chore: update to nightly-2024-09-25 (#655)

---
 SSA/Projects/InstCombine/ForLean.lean | 12 ++++++------
 lake-manifest.json                    |  6 +++---
 lakefile.toml                         |  2 +-
 lean-toolchain                        |  2 +-
 4 files changed, 11 insertions(+), 11 deletions(-)

diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean
index aea45a94c..50598ffe0 100644
--- a/SSA/Projects/InstCombine/ForLean.lean
+++ b/SSA/Projects/InstCombine/ForLean.lean
@@ -493,7 +493,7 @@ theorem and_add_or {A B : BitVec w} : (B &&& A) + (B ||| A) = B + A := by
 
 @[simp] theorem msb_signExtend_of_ge {i} (h : i ≥ w) (x : BitVec w) :
     (x.signExtend i).msb = x.msb := by
-  simp [BitVec.msb_eq_getLsbD_last]
+  simp [BitVec.msb_eq_getLsbD_last, getLsbD_signExtend]
   split <;> by_cases (0 < i) <;> simp_all
   simp [show i = w by omega]
 
@@ -518,16 +518,16 @@ theorem allOnes_sshiftRight {w n : Nat} :
   (allOnes w).sshiftRight n = allOnes w := by
   ext i
   by_cases h : 0 < w
-  · simp [BitVec.msb_allOnes h]
-  · simp ; omega
+  · simp [BitVec.msb_allOnes h, getLsbD_sshiftRight]
+  · simp [getLsbD_sshiftRight]; omega
 
 @[simp]
 theorem zero_sshiftRight {w n : Nat} :
   (0#w).sshiftRight n = 0#w := by
   ext i
   by_cases h : 0 < w
-  · simp [BitVec.msb_allOnes h]
-  · simp
+  · simp [BitVec.msb_allOnes h, getLsbD_sshiftRight]
+  · simp [getLsbD_sshiftRight]
 
 @[simp]
 theorem zero_ushiftRight {w n : Nat} :
@@ -540,7 +540,7 @@ theorem zero_ushiftRight {w n : Nat} :
 theorem not_sshiftRight {b : BitVec w} :
     ~~~b.sshiftRight n = (~~~b).sshiftRight n := by
   ext i
-  simp
+  simp [getLsbD_sshiftRight]
   by_cases h : w ≤ i
   <;> by_cases h' : n + i < w
   <;> by_cases h'' : 0 < w
diff --git a/lake-manifest.json b/lake-manifest.json
index b1463a93a..a52062903 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c37494a698d68c5e3711575fcb90ebf2974900ff",
+   "rev": "cd404b26c6ea643b9fdf5fb004d83a88c0f00f3e",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",
@@ -75,10 +75,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "08a9b5c185b952bb4a0c628361f4b2f8fe7eb623",
+   "rev": "f22e9cb44e572aa5c27f2b3e5136e365e36bf1c3",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "nightly-testing-2024-09-24",
+   "inputRev": "nightly-testing-2024-09-25",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/acmepjz/md4lean",
diff --git a/lakefile.toml b/lakefile.toml
index e13cbb13e..67c14d340 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -4,7 +4,7 @@ defaultTargets = ["SSA"]
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4"
-rev = "nightly-testing-2024-09-24"
+rev = "nightly-testing-2024-09-25"
 
 [[require]]
 name = "Cli"
diff --git a/lean-toolchain b/lean-toolchain
index 98d327efe..211c2d6ba 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2024-09-24
+leanprover/lean4:nightly-2024-09-25