diff --git a/Arm/BitVec.lean b/Arm/BitVec.lean
index a7218c5b..1e3c1874 100644
--- a/Arm/BitVec.lean
+++ b/Arm/BitVec.lean
@@ -241,8 +241,8 @@ protected theorem zero_le_sub (x y : BitVec n) :
 
 @[simp]
 protected theorem zero_or (x : BitVec n) : 0#n ||| x = x := by
-  unfold HOr.hOr instHOr OrOp.or instOrOpBitVec BitVec.or
-  simp only [toNat_ofNat, Nat.or_zero]
+  unfold HOr.hOr instHOrOfOrOp OrOp.or instOrOp BitVec.or
+  simp only [toNat_ofNat, Nat.zero_mod, Nat.zero_or]
   congr
 
 theorem BitVec.toNat_or (x y : BitVec n):
diff --git a/Arm/Insts/Common.lean b/Arm/Insts/Common.lean
index f349be99..6b0db913 100644
--- a/Arm/Insts/Common.lean
+++ b/Arm/Insts/Common.lean
@@ -302,8 +302,8 @@ def rev_elems (n esize : Nat) (x : BitVec n) (h₀ : esize ∣ n) (h₁ : 0 < es
     h3 ▸ (element ++ rest_ans)
    termination_by n
 
-example : rev_elems 4 4 0xA#4 (by decide) (by decide) = 0xA#4 := rfl
-example : rev_elems 8 4 0xAB#8 (by decide) (by decide) = 0xBA#8 := rfl
+example : rev_elems 4 4 0xA#4 (by decide) (by decide) = 0xA#4 := by rfl
+example : rev_elems 8 4 0xAB#8 (by decide) (by decide) = 0xBA#8 := by rfl
 example : rev_elems 8 4 (rev_elems 8 4 0xAB#8 (by decide) (by decide))
           (by decide) (by decide) = 0xAB#8 := by native_decide
 
diff --git a/Arm/Map.lean b/Arm/Map.lean
index b6428f98..0ecd78ce 100644
--- a/Arm/Map.lean
+++ b/Arm/Map.lean
@@ -118,17 +118,8 @@ def Map.size (m : Map α β) : Nat :=
 @[simp] theorem Map.size_erase_le [DecidableEq α] (m : Map α β) (a : α) : (m.erase a).size ≤ m.size := by
   induction m <;> simp [erase, size] at *
   split
-  next =>
-    -- (FIXME) This could be discharged by omega in
-    -- leanprover/lean4:nightly-2024-02-24, but not in
-    -- leanprover/lean4:nightly-2024-03-01.
-    exact Nat.le_succ_of_le (by assumption)
-  next =>
-    simp;
-    -- (FIXME) This could be discharged by omega in
-    -- leanprover/lean4:nightly-2024-02-24, but not in
-    -- leanprover/lean4:nightly-2024-03-01.
-    exact Nat.succ_le_succ (by assumption)
+  next => omega
+  next => simp; omega
 
 @[simp] theorem Map.size_erase_eq [DecidableEq α] (m : Map α β) (a : α) : m.contains a = false → (m.erase a).size = m.size := by
   induction m <;> simp [erase, size] at *
diff --git a/Arm/SeparateProofs.lean b/Arm/SeparateProofs.lean
index 39cbb52f..174c73f2 100644
--- a/Arm/SeparateProofs.lean
+++ b/Arm/SeparateProofs.lean
@@ -29,7 +29,7 @@ open BitVec
 ---- Some helpful bitvector lemmas ----
 
 theorem n_minus_1_lt_2_64_1 (n : Nat)
-  (h1 : Nat.succ 0 ≤ n) (h2 : n + 1 ≤ 2 ^ 64) :
+  (h1 : Nat.succ 0 ≤ n) (h2 : n < 2 ^ 64) :
   (n - 1)#64 < (2 ^ 64 - 1)#64 := by
   refine BitVec.val_bitvec_lt.mp ?a
   simp [BitVec.bitvec_to_nat_of_nat]
diff --git a/lean-toolchain b/lean-toolchain
index 2f334869..1a4d2185 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2024-03-28
+leanprover/lean4:nightly-2024-05-16