diff --git a/backends/lean/Aeneas/Data/Array.lean b/backends/lean/Aeneas/Data/Array.lean
index 0930b95b8..356c45bf1 100644
--- a/backends/lean/Aeneas/Data/Array.lean
+++ b/backends/lean/Aeneas/Data/Array.lean
@@ -108,13 +108,9 @@ theorem getElem_set! {α : Type u}
   simp only [set!_eq_setIfInBounds, ← getElem_toList, toList_setIfInBounds]
   simp_lists
 
-@[simp, simp_lists_safe]
-theorem getElem!_set!_ne {α : Type u}
-  [Inhabited α] {i j : ℕ} {x : α} {xs : Array α}
-  (h : i ≠ j) :
-  (xs.set! i x)[j]! = xs[j]! := by
-  simp only [set!_eq_setIfInBounds, ← getElem!_toList, toList_setIfInBounds]
-  simp_lists
+-- `Array.getElem!_set!_ne` is now provided by the core library; just register the
+-- Aeneas simp attributes on it.
+attribute [simp, simp_lists_safe] _root_.Array.getElem!_set!_ne
 
 @[simp, simp_lists_safe]
 theorem getElem_set!_ne {α : Type u}
diff --git a/backends/lean/Aeneas/Data/Vector.lean b/backends/lean/Aeneas/Data/Vector.lean
index 42118e3bb..b62c10e2d 100644
--- a/backends/lean/Aeneas/Data/Vector.lean
+++ b/backends/lean/Aeneas/Data/Vector.lean
@@ -108,16 +108,9 @@ theorem getElem!_set! {α : Type u}
     ← Array.getElem!_toList, Array.toList_setIfInBounds]
   simp_lists
 
-@[simp, simp_lists_safe]
-theorem getElem_set! {α : Type u}
-  [Inhabited α] {n i j : ℕ} {x : α} {xs : Vector α n}
-  (hi : i < n ∧ j = i) :
-  (xs.set! i x)[j] = x := by
-  have : i < xs.toArray.size := by scalar_tac
-  simp only [getElem_eq_toArray_getElem, toArray_set!, Array.set!_eq_setIfInBounds,
-    Array.size_setIfInBounds, size_toArray, Array.Inhabited_getElem_eq_getElem!,
-    ← Array.getElem!_toList, Array.toList_setIfInBounds, hi]
-  grind
+-- `Vector.getElem_set!_self` is now provided by the core library; register the
+-- Aeneas simp attribute on it.
+attribute [simp_lists_safe] getElem_set!_self
 
 @[simp, simp_lists_safe]
 theorem getElem!_set!_ne {α : Type u}
@@ -127,13 +120,9 @@ theorem getElem!_set!_ne {α : Type u}
   simp only [getElem!_eq_toArray_getElem!, toArray_set!]
   simp_lists
 
-@[simp, simp_lists_safe]
-theorem getElem_set!_ne {α : Type u}
-  [Inhabited α] {n i j : ℕ} {x : α} {xs : Vector α n}
-  (h : i ≠ j ∧ j < n) :
-  (xs.set! i x)[j] = xs[j] := by
-  simp only [getElem_eq_toArray_getElem, toArray_set!]
-  simp_lists
+-- `Vector.getElem_set!_ne` is now provided by the core library; register the
+-- Aeneas simp attribute on it.
+attribute [simp_lists_safe] getElem_set!_ne
 
 @[simp, simp_lists_safe]
 theorem getElem!_replicate {α : Type u} [Inhabited α] {i n : ℕ} {a : α} (h : i < n) :
diff --git a/backends/lean/Aeneas/Do/Tests.lean b/backends/lean/Aeneas/Do/Tests.lean
index f34c136e8..b8c56e16f 100644
--- a/backends/lean/Aeneas/Do/Tests.lean
+++ b/backends/lean/Aeneas/Do/Tests.lean
@@ -625,13 +625,15 @@ def do_match_cross_arm_used (t : Two) : Result Nat := do
 
 /-- warning: Variable name `n` is not explicitly referenced.
 
-The binding can be removed (if unused) or named `_` (if used implicitly).
+Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
+  [apply] _n
 
 Note: This linter can be disabled with `set_option linter.unusedVariables false`
 ---
 warning: Variable name `n` is not explicitly referenced.
 
-The binding can be removed (if unused) or named `_` (if used implicitly).
+Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
+  [apply] _n
 
 Note: This linter can be disabled with `set_option linter.unusedVariables false` -/
 #guard_msgs in
@@ -647,7 +649,8 @@ def do_let_arrow_id_used : Result Nat := do
 
 /-- warning: Variable name `x` is not explicitly referenced.
 
-The binding can be removed (if unused) or named `_` (if used implicitly).
+Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
+  [apply] _x
 
 Note: This linter can be disabled with `set_option linter.unusedVariables false` -/
 #guard_msgs in
@@ -668,25 +671,29 @@ def do_let_arrow_pat_used : Result Nat := do
 /--
 warning: Variable name `a` is not explicitly referenced.
 
-The binding can be removed (if unused) or named `_` (if used implicitly).
+Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
+  [apply] _a
 
 Note: This linter can be disabled with `set_option linter.unusedVariables false`
 ---
 warning: Variable name `b` is not explicitly referenced.
 
-The binding can be removed (if unused) or named `_` (if used implicitly).
+Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
+  [apply] _b
 
 Note: This linter can be disabled with `set_option linter.unusedVariables false`
 ---
 warning: Variable name `c` is not explicitly referenced.
 
-The binding can be removed (if unused) or named `_` (if used implicitly).
+Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
+  [apply] _c
 
 Note: This linter can be disabled with `set_option linter.unusedVariables false`
 ---
 warning: Variable name `d` is not explicitly referenced.
 
-The binding can be removed (if unused) or named `_` (if used implicitly).
+Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
+  [apply] _d
 
 Note: This linter can be disabled with `set_option linter.unusedVariables false`
 -/
@@ -699,25 +706,29 @@ def do_let_arrow_pat_unused : Result Nat := do
 /--
 warning: Variable name `a` is not explicitly referenced.
 
-The binding can be removed (if unused) or named `_` (if used implicitly).
+Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
+  [apply] _a
 
 Note: This linter can be disabled with `set_option linter.unusedVariables false`
 ---
 warning: Variable name `b` is not explicitly referenced.
 
-The binding can be removed (if unused) or named `_` (if used implicitly).
+Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
+  [apply] _b
 
 Note: This linter can be disabled with `set_option linter.unusedVariables false`
 ---
 warning: Variable name `c` is not explicitly referenced.
 
-The binding can be removed (if unused) or named `_` (if used implicitly).
+Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
+  [apply] _c
 
 Note: This linter can be disabled with `set_option linter.unusedVariables false`
 ---
 warning: Variable name `d` is not explicitly referenced.
 
-The binding can be removed (if unused) or named `_` (if used implicitly).
+Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
+  [apply] _d
 
 Note: This linter can be disabled with `set_option linter.unusedVariables false`
 -/
diff --git a/backends/lean/Aeneas/Std/Array/Array.lean b/backends/lean/Aeneas/Std/Array/Array.lean
index 7571a44c5..8983fcac6 100644
--- a/backends/lean/Aeneas/Std/Array/Array.lean
+++ b/backends/lean/Aeneas/Std/Array/Array.lean
@@ -225,6 +225,7 @@ theorem Array.update_spec {α : Type u} {n : Usize} (v: Array α n) (i: Usize) (
   := by
   simp only [partialSpec, update, set]
   cases hopt : v[i]? <;> simp_all
+  rfl
 
 def Array.index_mut_usize {α : Type u} {n : Usize} (v: Array α n) (i: Usize) :
   Result (α × (α -> Array α n)) := do
@@ -244,8 +245,8 @@ theorem Array.index_mut_usize_spec {α : Type u} {n : Usize} (v: Array α n) (i:
 @[simp]
 theorem Array.set_getElem!_eq {α} {n : Usize} [Inhabited α] (x : Array α n) (i : Usize) :
   x.set i (x.val[i.val]!) = x := by
-  have := @List.set_getElem_self _ x.val i.val
-  simp only [Array, Subtype.ext_iff, set_val_eq, List.set_getElem!]
+  apply Subtype.ext
+  simp only [set_val_eq, List.set_getElem!]
 
 @[simp]
 theorem Array.set_getElem_eq {α} {n : Usize} (x : Array α n) (i : Usize) (h : i.val < x.length) :
@@ -254,15 +255,14 @@ theorem Array.set_getElem_eq {α} {n : Usize} (x : Array α n) (i : Usize) (h :
     simpa using h
   have hself : x.val.set i.val x.val[i.val] = x.val :=
     List.set_getElem_self (as := x.val) (i := i.val) (h := h')
-  simp only [Array, Subtype.ext_iff, set_val_eq] at hself ⊢
+  apply Subtype.ext
+  simp only [set_val_eq]
   exact hself
 
 @[simp↓, simp_lists_safe↓]
 theorem Array.getElem_set_eq {α} {n : Usize} (v : Array α n) (i : Usize) (x : α) (h : i.val < (v.set i x).length) :
   (v.set i x)[i]'h = x := by
-  cases v
-  unfold set getElem instGetElemArrayUsizeLtNatValLengthValListEq
-  simp only [List.getElem_set_self]
+  simp only [Array.getElem_Usize_eq, Array.set_val_eq, List.getElem_set_self]
 
 @[simp↓, simp_lists_safe↓]
 theorem Array.getElem_set_eq' {α} {n : Usize} (v : Array α n) (i j : Usize) (x : α) (h : j.val < (v.set i x).length)
@@ -274,9 +274,8 @@ theorem Array.getElem_set_eq' {α} {n : Usize} (v : Array α n) (i j : Usize) (x
 theorem Array.getElem_set_neq {α} {n : Usize} (v : Array α n) (i j : Usize) (x : α)
   (h : j.val < (v.set i x).length) (h' : i ≠ j) :
   (v.set i x)[j]'h = v[j] := by
-  cases v
-  unfold set getElem instGetElemArrayUsizeLtNatValLengthValListEq
-  simp only [ne_eq, UScalar.neq_to_neq_val] at *
+  simp only [ne_eq, UScalar.neq_to_neq_val] at h'
+  simp only [Array.getElem_Usize_eq, Array.set_val_eq]
   simp_lists [List.getElem_set_ne]
 
 /-- Small helper (this function doesn't model a specific Rust function) -/
@@ -289,13 +288,19 @@ theorem Array.clone_length {α : Type u} {n : Usize} (clone : α → Result α)
   simp [Array.clone] at h
   simp [List.clone] at h
   split at h <;> simp_all
+  rename_i heq
+  have := List.mapM_Result_length heq
+  cases s'; simp_all
+  cases h; simp_all
 
 @[step]
 theorem Array.clone_spec {α : Type u} {n : Usize} {clone : α → Result α} {s : Array α n} (h : ∀ x ∈ s.val, clone x = ok x) :
   Array.clone clone s ⦃ s' => s' = s ⦄ := by
   simp only [Array.clone]
   have ⟨ l', h ⟩ := spec_imp_exists (List.clone_spec h)
-  simp [h]
+  simp only [h.1, bind_tc_ok]
+  apply (spec_ok _).mpr
+  exact Subtype.ext h.2.1
 
 @[rust_fun "core::array::{core::clone::Clone<[@T; @N]>}::clone"]
 def core.array.CloneArray.clone
@@ -307,8 +312,9 @@ theorem core.array.CloneArray.clone_spec {T : Type} {N : Usize} (cloneInst : cor
   (h : ∀ x ∈ a.val, cloneInst.clone x = ok x) :
   core.array.CloneArray.clone cloneInst a ⦃ a' => a = a' ⦄:= by
   unfold clone
-  have := spec_imp_exists (Array.clone_spec h)
-  grind
+  have ⟨a', h'⟩ := spec_imp_exists (Array.clone_spec h)
+  rw [h'.1]
+  exact (spec_ok _).mpr h'.2.symm
 
 @[rust_fun "core::array::{core::clone::Clone<[@T; @N]>}::clone_from"]
 def core.array.CloneArray.clone_from {T : Type} {N : Usize} (cloneInst : core.clone.Clone T)
@@ -320,8 +326,9 @@ theorem core.array.CloneArray.clone_from_spec {T : Type} {N : Usize} (cloneInst
   (self source : Array T N) (h : ∀ x ∈ source.val, cloneInst.clone x = ok x) :
   core.array.CloneArray.clone_from cloneInst self source ⦃ source' => source = source' ⦄ := by
   unfold clone_from
-  have := spec_imp_exists (Array.clone_spec h)
-  grind
+  have ⟨source', h'⟩ := spec_imp_exists (Array.clone_spec h)
+  rw [h'.1]
+  exact (spec_ok _).mpr h'.2.symm
 
 @[reducible, rust_trait_impl "core::clone::Clone<[@T; @N]>"]
 def core.clone.CloneArray {T : Type} (N : Usize)
@@ -337,7 +344,8 @@ def Array.setSlice! {α : Type u} {n} (s : Array α n) (i : ℕ) (s' : List α)
 theorem Array.setSlice!_getElem!_prefix {α} {n} [Inhabited α]
   (s : Array α n) (s' : List α) (i j : ℕ) (h : j < i) :
   (s.setSlice! i s')[j]! = s[j]! := by
-  simp only [Array.setSlice!, Array.getElem!_Nat_eq]
+  simp only [Array.getElem!_Nat_eq]
+  simp only [Array.setSlice!]
   simp_lists
 
 @[simp_lists_safe]
@@ -346,7 +354,8 @@ theorem Array.setSlice!_getElem_prefix {α} {n}
   (s.setSlice! i s')[j] = s[j] := by
   have hj' : j < (s.setSlice! i s').length := by scalar_tac
   have h1 : (s.setSlice! i s')[j]? = s[j]? := by
-    simp only [Array.getElem?_Nat_eq, Array.setSlice!]
+    simp only [Array.getElem?_Nat_eq]
+    simp only [Array.setSlice!]
     simp_lists [List.setSlice!_getElem?_prefix]
   simp only [Array.getElem?_Nat_eq, List.getElem?_eq_getElem hj', List.getElem?_eq_getElem h.2,
     Option.some.injEq] at h1
@@ -356,7 +365,8 @@ theorem Array.setSlice!_getElem_prefix {α} {n}
 theorem Array.setSlice!_getElem!_middle {α} {n} [Inhabited α]
   (s : Array α n) (s' : List α) (i j : ℕ) (h : i ≤ j ∧ j - i < s'.length ∧ j < s.length) :
   (s.setSlice! i s')[j]! = s'[j - i]! := by
-  simp only [Array.setSlice!, Array.getElem!_Nat_eq]
+  simp only [Array.getElem!_Nat_eq]
+  simp only [Array.setSlice!]
   simp_lists
 
 @[simp_lists_safe]
@@ -367,7 +377,8 @@ theorem Array.setSlice!_getElem_middle {α} {n}
     scalar_tac
   have hji : j - i < s'.length := h.2.1
   have h1 : (s.setSlice! i s')[j]? = s'[j - i]? := by
-    simp only [Array.getElem?_Nat_eq, Array.setSlice!]
+    simp only [Array.getElem?_Nat_eq]
+    simp only [Array.setSlice!]
     simp_lists [List.setSlice!_getElem?_middle]
   simp only [Array.getElem?_Nat_eq, List.getElem?_eq_getElem hj', List.getElem?_eq_getElem hji,
     Option.some.injEq] at h1
@@ -376,7 +387,8 @@ theorem Array.setSlice!_getElem_middle {α} {n}
 theorem Array.setSlice!_getElem!_suffix {α} {n} [Inhabited α]
   (s : Array α n) (s' : List α) (i j : ℕ) (h : i + s'.length ≤ j) :
   (s.setSlice! i s')[j]! = s[j]! := by
-  simp only [Array.setSlice!, Array.getElem!_Nat_eq]
+  simp only [Array.getElem!_Nat_eq]
+  simp only [Array.setSlice!]
   simp_lists
 
 theorem Array.setSlice!_getElem_suffix {α} {n}
@@ -384,7 +396,8 @@ theorem Array.setSlice!_getElem_suffix {α} {n}
   (s.setSlice! i s')[j] = s[j] := by
   have hj' : j < (s.setSlice! i s').length := by scalar_tac
   have h1 : (s.setSlice! i s')[j]? = s[j]? := by
-    simp only [Array.getElem?_Nat_eq, Array.setSlice!]
+    simp only [Array.getElem?_Nat_eq]
+    simp only [Array.setSlice!]
     simp_lists [List.setSlice!_getElem?_suffix]
   simp only [Array.getElem?_Nat_eq, List.getElem?_eq_getElem hj', List.getElem?_eq_getElem h.2,
     Option.some.injEq] at h1
diff --git a/backends/lean/Aeneas/Std/Array/ArraySlice.lean b/backends/lean/Aeneas/Std/Array/ArraySlice.lean
index 3e190fdbb..d5d709259 100644
--- a/backends/lean/Aeneas/Std/Array/ArraySlice.lean
+++ b/backends/lean/Aeneas/Std/Array/ArraySlice.lean
@@ -41,7 +41,9 @@ theorem Array.to_slice_mut_spec {α : Type u} {n : Usize} (a : Array α n) :
   (lift (Array.to_slice_mut a))
   ⦃ (s : Slice α) (back : Slice α → Array α n) =>
     s.val = a.val ∧ back = Array.from_slice a ⦄ := by
-  simp [lift, to_slice_mut, to_slice, WP.spec_ok]
+  simp only [lift, to_slice_mut, to_slice]
+  apply (spec_ok _).mpr
+  simp [Std.WP.uncurry']
 
 def Array.subslice {α : Type u} {n : Usize} (a : Array α n) (r : Range Usize) : Result (Slice α) :=
   if r.start.val ≤ r.end.val ∧ r.end.val ≤ a.val.length then
@@ -92,9 +94,14 @@ theorem Array.update_subslice_spec {α : Type u} {n : Usize} [Inhabited α] (a :
            | _ => False)
       False := by
   unfold update_subslice
-  split <;> rename_i h <;> simp [partialSpec]
-  · simp_lists
-  · scalar_tac
+  split
+  · rename_i h
+    simp only [partialSpec]
+    refine ⟨fun i hi => ?_, fun i hi hj => ?_, fun i hi hj => ?_⟩ <;>
+      (simp only [getElem!]; simp_lists)
+  · rename_i h
+    simp [partialSpec]
+    scalar_tac
 
 @[rust_fun "core::array::{core::ops::index::Index<[@T; @N], @I, @O>}::index"]
 def core.array.Array.index
@@ -135,7 +142,8 @@ theorem Array.val_to_slice {α} {n} (a : Array α n) : a.to_slice.val = a.val :=
 @[simp, simp_lists_safe, simp_scalar_safe, scalar_tac a.to_slice, grind =, agrind =]
 theorem Array.length_to_slice (a : Array α n) :
   a.to_slice.length = n := by
-  simp only [Slice.length, Array.to_slice, List.Vector.length_val]
+  simp only [Slice.length, Array.to_slice]
+  exact a.property
 
 @[rust_fun "core::array::equality::{core::cmp::PartialEq<[@T; @N], [@U; @N]>}::eq"]
 def core.array.equality.PartialEqArray.eq
@@ -313,7 +321,11 @@ theorem core.array.TryFromArrayCopySlice.try_from.step
         a.val = s.val ∧ a.length = N
       | .Err () => s.length ≠ N ⦄ := by
   simp only [core.array.TryFromArrayCopySlice.try_from]
-  grind only [usr Usize.cMax_bound, usr Usize.cMax_bound', = spec_ok]
+  split
+  · apply (spec_ok _).mpr
+    exact ⟨rfl, by scalar_tac⟩
+  · apply (spec_ok _).mpr
+    simpa using ‹¬ s.length = N›
 
 @[rust_fun "core::array::{core::convert::TryFrom<&'a [@T; @N], &'a [@T], core::array::TryFromSliceError>}::try_from"]
 def core.array.TryFromSharedArraySlice.try_from
@@ -381,7 +393,9 @@ theorem Array.Insts.CoreConvertAsRefSlice.as_ref.spec
     {T : Type} {N : Usize} (a : Array T N) :
     Array.Insts.CoreConvertAsRefSlice.as_ref a
     ⦃ (s : Slice T) => s.val = a.val ⦄ := by
-  simp [Array.Insts.CoreConvertAsRefSlice.as_ref, WP.spec_ok]
+  simp only [Array.Insts.CoreConvertAsRefSlice.as_ref]
+  apply (spec_ok _).mpr
+  rfl
 
 @[step]
 theorem Array.Insts.CoreConvertAsMutSlice.as_mut.spec
@@ -391,9 +405,13 @@ theorem Array.Insts.CoreConvertAsMutSlice.as_mut.spec
       s.val = a.val ∧
       s.length = N.val ∧
       ∀ s' : Slice T, s'.length = N.val → (back s').val = s'.val ⦄ := by
-  simp [Array.Insts.CoreConvertAsMutSlice.as_mut, WP.spec_ok, Slice.length]
-  intro s' hs'
-  simp [hs']
+  simp only [Array.Insts.CoreConvertAsMutSlice.as_mut]
+  apply (spec_ok _).mpr
+  simp only [Std.WP.uncurry', Slice.length]
+  refine ⟨?_, ?_, fun s' hs' => ?_⟩
+  · trivial
+  · scalar_tac
+  · simp [hs']
 
 @[simp, step_simps]
 theorem Array.index_SliceIndexRangeUsizeSlice {T : Type} {N : Usize}
@@ -414,7 +432,7 @@ theorem Array.index_SliceIndexRangeUsizeSlice.step {T : Type} {N : Usize} [Inhab
       (fun | .panic => ¬ (r.start ≤ r.end ∧ r.end ≤ N) | _ => False)
       False := by
   simp only [Array.index_SliceIndexRangeUsizeSlice]
-  have hts : a.to_slice.length = N := by simp [Array.to_slice, Slice.length]
+  have hts : a.to_slice.length = N := by simp [Array.to_slice, Slice.length, Array.length_eq]
   unfold core.slice.index.SliceIndexRangeUsizeSlice.index
   split <;> rename_i h <;> simp [partialSpec, Array.to_slice, Slice.length]
   · scalar_tac
@@ -434,10 +452,11 @@ theorem Array.index_mut_SliceIndexRangeUsizeSlice.step {T : Type} {N : Usize} [I
       False := by
   simp only [core.array.Array.index_mut, core.ops.index.IndexMutSlice,
     core.slice.index.Slice.index_mut]
-  have hts : a.to_slice.length = N := by simp [Array.to_slice, Slice.length]
+  have hts : a.to_slice.length = N := by simp [Array.to_slice, Slice.length, Array.length_eq]
   unfold core.slice.index.SliceIndexRangeUsizeSlice.index_mut
   split <;> rename_i h <;>
-    simp [partialSpec, Array.from_slice, Array.to_slice, uncurry', Slice.length]
+    simp [partialSpec, Array.from_slice, Array.to_slice, uncurry', Slice.length,
+      List.length_setSlice!, Array.length_eq]
   · simp_lists; scalar_tac
   · scalar_tac
 
@@ -464,10 +483,11 @@ theorem Array.index_mut_SliceIndexRangeToUsizeSlice {T : Type} {N : Usize}
       False := by
   simp only [core.array.Array.index_mut, core.ops.index.IndexMutSlice,
     core.slice.index.Slice.index_mut]
-  have hts : a.to_slice.length = N := by simp [Array.to_slice, Slice.length]
+  have hts : a.to_slice.length = N := by simp [Array.to_slice, Slice.length, Array.length_eq]
   unfold core.slice.index.SliceIndexRangeToUsizeSlice.index_mut
   split <;> rename_i h <;>
-    simp [partialSpec, Array.from_slice, Array.to_slice, uncurry', Slice.length] <;>
+    simp [partialSpec, Array.from_slice, Array.to_slice, uncurry', Slice.length,
+      List.length_setSlice!, Array.length_eq] <;>
     scalar_tac
 
 -- Array index/index_mut with RangeFrom
@@ -493,11 +513,12 @@ theorem Array.index_mut_SliceIndexRangeFromUsizeSlice {T : Type} {N : Usize}
       False := by
   simp only [core.array.Array.index_mut, core.ops.index.IndexMutSlice,
     core.slice.index.Slice.index_mut]
-  have hts : a.to_slice.length = N := by simp [Array.to_slice, Slice.length]
+  have hts : a.to_slice.length = N := by simp [Array.to_slice, Slice.length, Array.length_eq]
   unfold core.slice.index.SliceIndexRangeFromUsizeSlice.index_mut
   split <;> rename_i h <;>
     simp [partialSpec, Array.from_slice, Array.to_slice, uncurry',
-          Slice.length, Slice.drop, List.length_drop];
+          Slice.length, Slice.drop, List.length_drop,
+          List.length_setSlice!, Array.length_eq];
     scalar_tac
 
 @[reducible, rust_trait_impl "core::convert::AsRef<[@T; @N], [@T]>"]
diff --git a/backends/lean/Aeneas/Std/Core/Convert.lean b/backends/lean/Aeneas/Std/Core/Convert.lean
index bdcdca1ac..12b9126e4 100644
--- a/backends/lean/Aeneas/Std/Core/Convert.lean
+++ b/backends/lean/Aeneas/Std/Core/Convert.lean
@@ -129,8 +129,8 @@ theorem core.result.Result.is_ok.step_spec {T E : Type}
     core.result.Result.is_ok r
     ⦃ (b : Bool) => b = r.ok? ⦄ := by
   match r with
-  | .Ok v => grind [is_ok]
-  | .Err e => grind [is_ok]
+  | .Ok v => simp only [is_ok]; exact (WP.spec_ok _).mpr (by simp)
+  | .Err e => simp only [is_ok]; exact (WP.spec_ok _).mpr (by simp)
 
 /-- Step spec for `Result::branch` on an `Ok`: yields `Continue v`. -/
 theorem core.result.Result.Insts.CoreOpsTry.branch_Ok.spec
diff --git a/backends/lean/Aeneas/Std/Core/Core.lean b/backends/lean/Aeneas/Std/Core/Core.lean
index 8e17a5bd8..1ce724be8 100644
--- a/backends/lean/Aeneas/Std/Core/Core.lean
+++ b/backends/lean/Aeneas/Std/Core/Core.lean
@@ -97,7 +97,7 @@ def core.option.Option.unwrap {T : Type} (x : Option T) : Result T :=
 @[step]
 theorem core.option.Option.unwrap.spec {T : Type} (x : Option T) (h : x.isSome) :
   unwrap x ⦃ v => x = some v ⦄ := by
-  simp only [unwrap, ofOption]; grind
+  simp only [unwrap, ofOption]; cases x <;> simp_all
 
 @[step_pure_def, rust_fun "core::option::{core::option::Option<@T>}::unwrap_or" -canFail]
 def core.option.Option.unwrap_or (self : Option T) (default : T) : T :=
diff --git a/backends/lean/Aeneas/Std/Core/CoreOption.lean b/backends/lean/Aeneas/Std/Core/CoreOption.lean
index 5a22429d7..5ecbdb204 100644
--- a/backends/lean/Aeneas/Std/Core/CoreOption.lean
+++ b/backends/lean/Aeneas/Std/Core/CoreOption.lean
@@ -13,6 +13,6 @@ attribute [agrind =] Option.isSome_none Option.isSome_some
 
 theorem core.option.Option.expect.spec {T : Type} (x : Option T) (msg: Str) (h : x.isSome) :
   expect x msg ⦃ v => x = some v ⦄ := by
-  simp only [expect, Result.ofOption]; grind
+  simp only [expect, Result.ofOption]; cases x <;> simp_all
 
 end Aeneas.Std
diff --git a/backends/lean/Aeneas/Std/Scalar/CoreConvertNum.lean b/backends/lean/Aeneas/Std/Scalar/CoreConvertNum.lean
index fac90e77e..5a829fd2a 100644
--- a/backends/lean/Aeneas/Std/Scalar/CoreConvertNum.lean
+++ b/backends/lean/Aeneas/Std/Scalar/CoreConvertNum.lean
@@ -594,19 +594,19 @@ iscalar_no_isize def core.num.«%S».to_be_bytes (x : «%S») : Array I8 (%Size)
 # From Little-Endian
 -/
 uscalar_no_usize def core.num.«%S».from_le_bytes (a : Array U8 (%Size)#usize) : «%S» :=
-  ⟨ (BitVec.fromLEBytes (List.map U8.bv a.val)).cast (by simp) ⟩
+  ⟨ (BitVec.fromLEBytes (List.map U8.bv a.val)).cast (by scalar_tac) ⟩
 
 iscalar_no_isize def core.num.«%S».from_le_bytes (a : Array I8 (%Size)#usize) : «%S» :=
-  ⟨ (BitVec.fromLEBytes (List.map I8.bv a.val)).cast (by simp) ⟩
+  ⟨ (BitVec.fromLEBytes (List.map I8.bv a.val)).cast (by scalar_tac) ⟩
 
 /-!
 # From Big-Endian
 -/
 uscalar_no_usize def core.num.«%S».from_be_bytes (a : Array U8 (%Size)#usize) : «%S» :=
-  ⟨ (BitVec.fromBEBytes (List.map U8.bv a.val)).cast (by simp) ⟩
+  ⟨ (BitVec.fromBEBytes (List.map U8.bv a.val)).cast (by scalar_tac) ⟩
 
 iscalar_no_isize def core.num.«%S».from_be_bytes (a : Array I8 (%Size)#usize) : «%S» :=
-  ⟨ (BitVec.fromBEBytes (List.map I8.bv a.val)).cast (by simp) ⟩
+  ⟨ (BitVec.fromBEBytes (List.map I8.bv a.val)).cast (by scalar_tac) ⟩
 
 /-!
 # Progress theorems: To Little-Endian
@@ -614,25 +614,29 @@ iscalar_no_isize def core.num.«%S».from_be_bytes (a : Array I8 (%Size)#usize)
 uscalar_no_usize @[step]
 theorem core.num.«%S».to_le_bytes.step_spec (x : «%S») :
   lift (core.num.«%S».to_le_bytes x) ⦃ y => y.val = x.bv.toLEBytes.map (@UScalar.mk UScalarTy.U8) ⦄ := by
-  simp only [spec_ok, lift, to_le_bytes, UScalarTy.U8_numBits_eq]
+  simp only [lift, to_le_bytes, UScalarTy.U8_numBits_eq]
+  exact (spec_ok _).mpr rfl
 
 iscalar_no_isize @[step]
 theorem core.num.«%S».to_le_bytes.step_spec (x : «%S») :
   lift (core.num.«%S».to_le_bytes x) ⦃ y => y.val = x.bv.toLEBytes.map (@IScalar.mk IScalarTy.I8) ⦄ := by
-  simp only [spec_ok, lift, to_le_bytes, IScalarTy.I8_numBits_eq]
+  simp only [lift, to_le_bytes, IScalarTy.I8_numBits_eq]
+  exact (spec_ok _).mpr rfl
 
 /-!
 # Progress theorems: From Little-Endian
 -/
 uscalar_no_usize @[step]
 theorem core.num.«%S».from_le_bytes.step_spec (x : Array U8 (%Size)#usize) :
-  lift (core.num.«%S».from_le_bytes x) ⦃ y => y.bv = (BitVec.fromLEBytes (x.val.map U8.bv)).cast (by simp) ⦄ := by
-  simp only [spec_ok, lift, from_le_bytes]
+  lift (core.num.«%S».from_le_bytes x) ⦃ y => y.bv = (BitVec.fromLEBytes (x.val.map U8.bv)).cast (by scalar_tac) ⦄ := by
+  simp only [lift, from_le_bytes]
+  exact (spec_ok _).mpr rfl
 
 iscalar_no_isize @[step]
 theorem core.num.«%S».from_le_bytes.step_spec (x : Array I8 (%Size)#usize) :
-  lift (core.num.«%S».from_le_bytes x) ⦃ y => y.bv = (BitVec.fromLEBytes (x.val.map I8.bv)).cast (by simp) ⦄  := by
-  simp only [spec_ok, lift, from_le_bytes]
+  lift (core.num.«%S».from_le_bytes x) ⦃ y => y.bv = (BitVec.fromLEBytes (x.val.map I8.bv)).cast (by scalar_tac) ⦄  := by
+  simp only [lift, from_le_bytes]
+  exact (spec_ok _).mpr rfl
 
 /-!
 # Progress theorems: To Big-Endian
@@ -640,25 +644,29 @@ theorem core.num.«%S».from_le_bytes.step_spec (x : Array I8 (%Size)#usize) :
 uscalar_no_usize @[step]
 theorem core.num.«%S».to_be_bytes.step_spec (x : «%S») :
   lift (core.num.«%S».to_be_bytes x) ⦃ y => y.val = x.bv.toBEBytes.map (@UScalar.mk UScalarTy.U8) ⦄ := by
-  simp only [spec_ok, lift, to_be_bytes, UScalarTy.U8_numBits_eq]
+  simp only [lift, to_be_bytes, UScalarTy.U8_numBits_eq]
+  exact (spec_ok _).mpr rfl
 
 iscalar_no_isize @[step]
 theorem core.num.«%S».to_be_bytes.step_spec (x : «%S») :
   lift (core.num.«%S».to_be_bytes x) ⦃ y => y.val = x.bv.toBEBytes.map (@IScalar.mk IScalarTy.I8) ⦄ := by
-  simp only [spec_ok, lift, to_be_bytes, IScalarTy.I8_numBits_eq]
+  simp only [lift, to_be_bytes, IScalarTy.I8_numBits_eq]
+  exact (spec_ok _).mpr rfl
 
 /-!
 # Progress theorems: From Big-Endian
 -/
 uscalar_no_usize @[step]
 theorem core.num.«%S».from_be_bytes.step_spec (x : Array U8 (%Size)#usize) :
-  lift (core.num.«%S».from_be_bytes x) ⦃ y => y.bv = (BitVec.fromBEBytes (x.val.map U8.bv)).cast (by simp) ⦄ := by
-  simp only [spec_ok, lift, from_be_bytes]
+  lift (core.num.«%S».from_be_bytes x) ⦃ y => y.bv = (BitVec.fromBEBytes (x.val.map U8.bv)).cast (by scalar_tac) ⦄ := by
+  simp only [lift, from_be_bytes]
+  exact (spec_ok _).mpr rfl
 
 iscalar_no_isize @[step]
 theorem core.num.«%S».from_be_bytes.step_spec (x : Array I8 (%Size)#usize) :
-  lift (core.num.«%S».from_be_bytes x) ⦃ y => y.bv = (BitVec.fromBEBytes (x.val.map I8.bv)).cast (by simp) ⦄  := by
-  simp only [spec_ok, lift, from_be_bytes]
+  lift (core.num.«%S».from_be_bytes x) ⦃ y => y.bv = (BitVec.fromBEBytes (x.val.map I8.bv)).cast (by scalar_tac) ⦄  := by
+  simp only [lift, from_be_bytes]
+  exact (spec_ok _).mpr rfl
 
 /-!
 # `cast_signed` / `cast_unsigned`
diff --git a/backends/lean/Aeneas/Std/Slice.lean b/backends/lean/Aeneas/Std/Slice.lean
index d8c770289..b1134d82f 100644
--- a/backends/lean/Aeneas/Std/Slice.lean
+++ b/backends/lean/Aeneas/Std/Slice.lean
@@ -118,7 +118,7 @@ def Slice.index_usize {α : Type u} (v: Slice α) (i: Usize) : Result α :=
   | some x => ok x
 
 theorem Slice.eq_iff {α} (s0 s1 : Slice α) : s0 = s1 ↔ s0.val = s1.val := by
-  simp only [Slice, Subtype.ext_iff]
+  exact Subtype.ext_iff
 
 @[rust_fun "core::slice::{[@T]}::is_empty", simp]
 def core.slice.Slice.is_empty {T : Type} (s : Slice T) : Result Bool := ok (s.length = 0)
@@ -133,7 +133,7 @@ theorem core.slice.Slice.is_empty_spec {T : Type} (s : Slice T) :
 theorem Slice.index_usize_spec {α : Type u} (v: Slice α) (i: Usize)
   (hbound : i.val < v.length) :
   v.index_usize i ⦃ x => x = v.val[i.val] ⦄ := by
-  grind [index_usize]
+  simp only [index_usize, Slice.getElem?_Usize_eq, List.getElem?_eq_getElem hbound, spec_ok]
 
 @[simp, scalar_tac_simps, simp_lists_hyps_simps, grind =]
 theorem Slice.set_val_eq {α : Type u} (v: Slice α) (i: Usize) (x: α) :
@@ -268,9 +268,9 @@ def Slice.update {α : Type u} (v: Slice α) (i: Usize) (x: α) : Result (Slice
 theorem Slice.update_spec {α : Type u} (v: Slice α) (i: Usize) (x : α)
   (hbound : i.val < v.length) :
   v.update i x ⦃ nv => nv = v.set i x ⦄ := by
-  simp only [update, set, setAtNat]
-  simp at *
-  simp [*]
+  simp only [update, List.getElem?_eq_getElem hbound]
+  apply (spec_ok _).mpr
+  rfl
 
 def Slice.index_mut_usize {α : Type u} (v: Slice α) (i: Usize) :
   Result (α × (α → Slice α)) := do
@@ -288,7 +288,8 @@ theorem Slice.index_mut_usize_spec {α : Type u} (v: Slice α) (i: Usize)
 @[simp, simp_lists_safe]
 theorem Slice.update_index_eq α [Inhabited α] (x : Slice α) (i : Usize) (h : i.val < x.val.length) :
   x.set i (x.val[i.val]'h) = x := by
-  simp only [Slice, Subtype.ext_iff, set_val_eq, List.set_getElem_self]
+  apply Subtype.ext
+  simp only [set_val_eq, List.set_getElem_self]
 
 def Slice.subslice {α : Type u} (s : Slice α) (r : Range Usize) : Result (Slice α) :=
   if r.start.val ≤ r.end.val ∧ r.end.val ≤ s.length then
@@ -305,7 +306,10 @@ theorem Slice.subslice_spec {α : Type u} [Inhabited α] (s : Slice α) (r : Ran
   subslice s r ⦃ ns => ns.val = s.slice r.start.val r.end.val ∧
   (∀ i, i + r.start.val < r.end.val → ns[i]! = s[r.start.val + i]!) ⦄
   := by
-  simp_all only [subslice, length, and_self, ite_true, slice, spec_ok, true_and]
+  unfold subslice
+  rw [if_pos ⟨h0, h1⟩]
+  apply (spec_ok _).mpr
+  refine ⟨rfl, ?_⟩
   intro i _
   have := List.getElem!_slice r.start.val r.end.val i s.val (by scalar_tac)
   simp only [List.getElem!_eq_getElem?_getD, getElem!_Nat_eq] at *
@@ -324,9 +328,10 @@ theorem Slice.update_subslice_spec {α : Type u} [Inhabited α] (a : Slice α) (
     (∀ i, i < r.start.val → na[i]! = a[i]!) ∧
     (∀ i, r.start.val ≤ i → i < r.end.val → na[i]! = ss[i - r.start.val]!) ∧
     (∀ i, r.end.val ≤ i → i < a.length → na[i]! = a[i]!) ⦄ := by
-  simp only [update_subslice, length, and_self, ↓reduceDIte, getElem!_Nat_eq,
-    spec_ok, *]
-  simp_lists
+  simp only [update_subslice, length, and_self, ↓reduceDIte, *]
+  apply (spec_ok _).mpr
+  refine ⟨fun i hi => ?_, fun i hi hj => ?_, fun i hi hj => ?_⟩ <;>
+    (simp only [getElem!]; simp_lists)
 
 @[rust_fun "core::slice::{[@T]}::reverse" -canFail]
 def core.slice.Slice.reverse {T : Type} (s : Slice T) : Slice T :=
@@ -649,7 +654,9 @@ theorem _SliceIndexRangeFromUsizeSlice.index_mut.test {T} (s : Slice T) (r : cor
     back s1 = s
   | _ => False := by
   unfold core.slice.index.SliceIndexRangeFromUsizeSlice.index_mut
-  simp [h]
+  simp only [h, ↓reduceIte, Slice.drop]
+  apply Subtype.ext
+  simp
 
 @[reducible, rust_trait_impl "core::slice::index::private_slice_index::Sealed<core::ops::range::RangeFrom<usize>>"]
 def core.slice.index.private_slice_index.SealedRangeFromUsize :
@@ -692,7 +699,9 @@ theorem Slice.clone_spec {T : Type} {clone : T → Result T} {s : Slice T} (h :
   Slice.clone clone s ⦃ s' => s = s' ⦄ := by
   simp only [Slice.clone]
   have ⟨ _, h ⟩ := spec_imp_exists (List.clone_spec h)
-  simp [h]
+  simp only [h.1, bind_tc_ok]
+  apply (spec_ok _).mpr
+  exact (Subtype.ext h.2.1).symm
 
 @[rust_fun "core::slice::{[@T]}::split_at"]
 def core.slice.Slice.split_at {T : Type} (s : Slice T) (n : Usize) :
@@ -732,7 +741,7 @@ theorem core.slice.Slice.split_at.spec {T : Type} (s : Slice T) (n : Usize)
         s0.length = n.val ∧ s1.length = s.length - n.val ∧
         s0.val = s.val.take n.val ∧ s1.val = s.val.drop n.val ⦄ := by
   unfold core.slice.Slice.split_at
-  simp only [h, ↓reduceDIte, WP.spec_ok, uncurry'_pair]
+  simp only [h, ↓reduceDIte, WP.spec_ok]
   refine ⟨?_, ?_, ?_, ?_⟩ <;>
   simp only [Slice.length, List.splitAt_eq, List.length_take, inf_eq_left, List.length_drop, *]
 
@@ -759,11 +768,13 @@ theorem core.slice.Slice.split_at_mut.spec {T : Type} (s : Slice T) (n : Usize)
   · simp [Slice.length, List.splitAt_eq]
   · simp [List.splitAt_eq]
   · simp [List.splitAt_eq]
-  · split_ifs with hcond
-    · exact ⟨rfl, by simp [Slice.length, List.length_append]; scalar_tac⟩
-    · exfalso; apply hcond
-      simp [Slice.length, List.splitAt_eq] at *
-      exact ⟨by scalar_tac, by scalar_tac⟩
+  · have hc : s0'.length = (s.val.splitAt n.val).1.length ∧ s1'.length = (s.val.splitAt n.val).2.length := by
+      simp only [List.splitAt_eq, List.length_take, List.length_drop, Slice.length]
+      constructor <;> scalar_tac
+    refine ⟨?_, ?_⟩
+    · simp only [hc.1, hc.2, and_self, ↓reduceDIte]
+    · simp only [hc.1, hc.2, and_self, ↓reduceDIte, Slice.length, List.length_append]
+      scalar_tac
 
 @[rust_fun "core::slice::{[@T]}::swap"]
 def core.slice.Slice.swap {T : Type} (s : Slice T) (a b : Usize) : Result (Slice T) := do
@@ -824,7 +835,8 @@ theorem Slice.setSlice!_length {α : Type u} (s : Slice α) (i : ℕ) (s' : List
 theorem Slice.setSlice!_getElem!_prefix {α} [Inhabited α]
   (s : Slice α) (s' : List α) (i j : ℕ) (h : j < i) :
   (s.setSlice! i s')[j]! = s[j]! := by
-  simp only [Slice.setSlice!, Slice.getElem!_Nat_eq]
+  simp only [Slice.getElem!_Nat_eq]
+  simp only [Slice.setSlice!]
   simp_lists
 
 @[simp_lists_safe]
@@ -834,7 +846,8 @@ theorem Slice.setSlice!_getElem_prefix {α}
   have hj' : j < (s.setSlice! i s').length := by
     simpa [Slice.setSlice!_length] using h.2
   have h1 : (s.setSlice! i s')[j]? = s[j]? := by
-    simp only [Slice.getElem?_Nat_eq, Slice.setSlice!]
+    simp only [Slice.getElem?_Nat_eq]
+    simp only [Slice.setSlice!]
     simp_lists [List.setSlice!_getElem?_prefix]
   simp only [Slice.getElem?_Nat_eq, List.getElem?_eq_getElem hj', List.getElem?_eq_getElem h.2,
     Option.some.injEq] at h1
@@ -844,7 +857,8 @@ theorem Slice.setSlice!_getElem_prefix {α}
 theorem Slice.setSlice!_getElem!_middle {α} [Inhabited α]
   (s : Slice α) (s' : List α) (i j : ℕ) (h : i ≤ j ∧ j - i < s'.length ∧ j < s.length) :
   (s.setSlice! i s')[j]! = s'[j - i]! := by
-  simp only [Slice.setSlice!, Slice.getElem!_Nat_eq]
+  simp only [Slice.getElem!_Nat_eq]
+  simp only [Slice.setSlice!]
   simp_lists
 
 @[simp_lists_safe]
@@ -855,7 +869,8 @@ theorem Slice.setSlice!_getElem_middle {α}
     simpa [Slice.setSlice!_length] using h.2.2
   have hji : j - i < s'.length := h.2.1
   have h1 : (s.setSlice! i s')[j]? = s'[j - i]? := by
-    simp only [Slice.getElem?_Nat_eq, Slice.setSlice!]
+    simp only [Slice.getElem?_Nat_eq]
+    simp only [Slice.setSlice!]
     simp_lists [List.setSlice!_getElem?_middle]
   simp only [Slice.getElem?_Nat_eq, List.getElem?_eq_getElem hj', List.getElem?_eq_getElem hji,
     Option.some.injEq] at h1
@@ -864,7 +879,8 @@ theorem Slice.setSlice!_getElem_middle {α}
 theorem Slice.setSlice!_getElem!_suffix {α} [Inhabited α]
   (s : Slice α) (s' : List α) (i j : ℕ) (h : i + s'.length ≤ j) :
   (s.setSlice! i s')[j]! = s[j]! := by
-  simp only [Slice.setSlice!, Slice.getElem!_Nat_eq]
+  simp only [Slice.getElem!_Nat_eq]
+  simp only [Slice.setSlice!]
   simp_lists
 
 theorem Slice.setSlice!_getElem_suffix {α}
@@ -873,7 +889,8 @@ theorem Slice.setSlice!_getElem_suffix {α}
   have hj' : j < (s.setSlice! i s').length := by
     simpa [Slice.setSlice!_length] using h.2
   have h1 : (s.setSlice! i s')[j]? = s[j]? := by
-    simp only [Slice.getElem?_Nat_eq, Slice.setSlice!]
+    simp only [Slice.getElem?_Nat_eq]
+    simp only [Slice.setSlice!]
     simp_lists [List.setSlice!_getElem?_suffix]
   simp only [Slice.getElem?_Nat_eq, List.getElem?_eq_getElem hj', List.getElem?_eq_getElem h.2,
     Option.some.injEq] at h1
@@ -894,9 +911,9 @@ theorem core.slice.index.SliceIndexRangeUsizeSlice.index_mut.step_spec (r : core
   simp only [index_mut, UScalar.le_equiv, Slice.length]
   split
   . simp only [spec_ok, Std.WP.uncurry', true_and]
+    refine ⟨?_, fun s2 => rfl⟩
     simp_lists
     simp_scalar
-    simp_lists [Slice.eq_iff]
   . scalar_tac
 
 @[step]
@@ -907,9 +924,10 @@ theorem core.slice.index.SliceIndexRangeUsizeSlice.index.step_spec {α : Type}
       s1.length = r.end - r.start ⦄ := by
   simp only [core.slice.index.SliceIndexRangeUsizeSlice.index, UScalar.le_equiv, Slice.length]
   split
-  · simp only [spec_ok, true_and]
+  · apply (spec_ok _).mpr
+    refine ⟨rfl, ?_⟩
     simp_lists
-    omega
+    simp_scalar
   · simp only [spec_fail]
     scalar_tac
 
@@ -950,8 +968,11 @@ theorem core.slice.index.SliceIndexRangeToUsizeSlice.index.step_spec
       s1.length = r.end ⦄ := by
   simp only [index]
   split
-  · simp only [spec_ok, Slice.length, true_and]
-    simp; scalar_tac
+  · apply (spec_ok _).mpr
+    refine ⟨rfl, ?_⟩
+    simp only [Slice.length]
+    simp_lists
+    simp_scalar
   · scalar_tac
 
 -- RangeFrom step specs
@@ -991,8 +1012,11 @@ theorem core.slice.index.SliceIndexRangeFromUsizeSlice.index.step_spec
       s1.length = s.length - r.start.val ⦄ := by
   simp only [index]
   split
-  · simp only [spec_ok, Slice.drop, true_and]
-    simp [Slice.length, List.length_drop]
+  · apply (spec_ok _).mpr
+    refine ⟨rfl, ?_⟩
+    simp only [Slice.length]
+    simp_lists
+    simp_scalar
   · scalar_tac
 
 @[step]
@@ -1033,7 +1057,8 @@ theorem Slice.mapM_spec {α β} {f : α → Result β} {s : Slice α} {post : Na
   obtain ⟨l', hl'⟩ := hmapM_ok
   split
   case h_1 xs heq =>
-    simp only [UScalar.lt_equiv, Usize.ofNatCore_val_eq, spec_ok]
+    simp only [UScalar.lt_equiv, Usize.ofNatCore_val_eq]
+    apply (spec_ok _).mpr
     refine ⟨by grind [List.mapM_Result_length], fun i hi => ?_⟩
     have hlen : i < s.len := by have := List.mapM_Result_length heq; simp [Slice.len] at *; omega
     have hthis := List.mapM_Result_ok heq (↑i) (by scalar_tac)
@@ -1086,7 +1111,10 @@ theorem core.slice.Slice.fill.spec {T : Type} (cloneInst : core.clone.Clone T)
     | .div => exfalso; have := hclone; rw [hc] at this; simp at this
   have hmapM := List.mapM_const_ok s.val hcl
   split
-  · rename_i val heq; rw [hmapM] at heq; cases heq; simp [spec_ok, Slice.length, List.length_replicate]
+  · rename_i val heq; rw [hmapM] at heq; cases heq
+    apply (spec_ok _).mpr
+    refine ⟨?_, rfl⟩
+    simp [Slice.length, List.length_replicate]
   · exfalso; simp_all
   · exfalso; simp_all
 
diff --git a/backends/lean/Aeneas/Std/Vec.lean b/backends/lean/Aeneas/Std/Vec.lean
index c58199c4b..c5a081239 100644
--- a/backends/lean/Aeneas/Std/Vec.lean
+++ b/backends/lean/Aeneas/Std/Vec.lean
@@ -130,7 +130,15 @@ def Vec.push {α : Type u} (v : Vec α) (x : α) : Result (Vec α)
 theorem Vec.push_spec {α : Type u} (v : Vec α) (x : α) (h : v.val.length < Usize.max) :
   v.push x ⦃ v1 =>
   v1.val = v.val ++ [x] ⦄ := by
-  unfold push; grind
+  unfold push
+  simp only []
+  split
+  · apply (spec_ok _).mpr
+    simp [List.concat_eq_append]
+  · exfalso
+    rename_i hc
+    simp only [Bool.or_eq_true, decide_eq_true_eq, not_or] at hc
+    scalar_tac
 
 @[rust_fun "alloc::vec::{alloc::vec::Vec<@T>}::insert" (keepParams := [true, false])]
 def Vec.insert {α : Type u} (v: Vec α) (i: Usize) (x: α) : Result (Vec α) :=
@@ -143,7 +151,9 @@ def Vec.insert {α : Type u} (v: Vec α) (i: Usize) (x: α) : Result (Vec α) :=
 theorem Vec.insert_spec {α : Type u} (v: Vec α) (i: Usize) (x: α)
   (hbound : i.val < v.length) :
   v.insert i x ⦃ nv => nv.val = v.val.set i x ⦄ := by
-  simp [insert, *]
+  simp only [insert, hbound, ↓reduceIte]
+  apply (spec_ok _).mpr
+  rfl
 
 def Vec.index_usize {α : Type u} (v: Vec α) (i: Usize) : Result α :=
   match v[i.val]? with
@@ -170,7 +180,9 @@ theorem Vec.update_spec {α : Type u} (v: Vec α) (i: Usize) (x : α)
   v.update i x ⦃ nv => nv = v.set i x ⦄ := by
   simp only [update, set]
   simp at *
-  split <;> simp_all
+  split
+  · simp_all
+  · apply (spec_ok _).mpr; rfl
 
 @[scalar_tac_simps, grind =, agrind =]
 theorem Vec.set_length {α : Type u} (v: Vec α) (i: Usize) (x: α) :
@@ -345,6 +357,8 @@ theorem alloc.vec.from_elem_spec {T : Type} (cloneInst : core.clone.Clone T)
   unfold from_elem
   have ⟨ l, h ⟩ := spec_imp_exists (@List.clone_spec _ cloneInst.clone (List.replicate n.val x) (by intros; simp_all))
   simp [h]
+  apply (spec_ok _).mpr
+  exact ⟨rfl, by simp⟩
 
 @[rust_fun "alloc::vec::{alloc::vec::Vec<@T>}::with_capacity" -canFail -lift]
 def alloc.vec.Vec.with_capacity (T : Type) (_ : Usize) : alloc.vec.Vec T := Vec.new T
@@ -400,24 +414,24 @@ theorem alloc.vec.Vec.resize_spec {T} (cloneInst : core.clone.Clone T)
     nv.val = v.val.resize new_len value ⦄ := by
   rw [resize]
   split
-  . simp
-  . simp [*]
+  · apply (spec_ok _).mpr; rfl
+  · simp only [hClone]
+    apply (spec_ok _).mpr; rfl
 
 @[simp↓, scalar_tac_simps↓, grind =, agrind =]
 theorem alloc.vec.Vec.set_getElem!_eq α [Inhabited α] (x : alloc.vec.Vec α) (i : Usize) :
   x.set i x[i]! = x := by
-  simp only [getElem!_Usize_eq]
-  simp only [Vec, set_val_eq, Subtype.ext_iff, List.set_getElem!]
+  apply Subtype.ext
+  simp only [getElem!_Usize_eq, set_val_eq, List.set_getElem!]
 
 @[simp↓, scalar_tac_simps, simp_lists_safe, grind =, agrind =]
 theorem alloc.vec.Vec.set_getElem_eq α (x : alloc.vec.Vec α) (i : Usize) (h : i.val < x.length) :
   x.set i x[i] = x := by
   have h' : i.val < x.val.length := by
     simpa using h
-  have hself : x.val.set i.val x.val[i.val] = x.val :=
-    List.set_getElem_self (as := x.val) (i := i.val) (h := h')
-  simp only [alloc.vec.Vec, Subtype.ext_iff, set_val_eq] at hself ⊢
-  exact hself
+  apply Subtype.ext
+  simp only [set_val_eq, getElem_Usize_eq]
+  exact List.set_getElem_self (as := x.val) (i := i.val) (h := h')
 
 @[simp_lists_safe↓]
 theorem alloc.vec.Vec.set_getElem_eq' α (x : alloc.vec.Vec α) (i j : Usize) (h : j.val < x.length) (hEq : i = j) :
@@ -462,7 +476,9 @@ def alloc.vec.FromBoxSliceVec.from {T : Type} (v : alloc.vec.Vec T) : Result (Sl
 @[step]
 theorem alloc.vec.FromBoxSliceVec.from_spec {T : Type} (v : alloc.vec.Vec T) :
   alloc.vec.FromBoxSliceVec.from v ⦃ s => s.length = v.length ∧ s.val = v.val⦄ := by
-  simp [alloc.vec.FromBoxSliceVec.from]
+  simp only [alloc.vec.FromBoxSliceVec.from]
+  apply (spec_ok _).mpr
+  exact ⟨rfl, rfl⟩
 
 @[reducible, rust_trait_impl "core::convert::From<Box<[@T]>, alloc::vec::Vec<@T>>" (keepParams := [true, false])]
 def core.convert.FromBoxSliceVec (T : Type) :
@@ -482,7 +498,8 @@ theorem alloc.vec.Vec.setSlice!_length {α : Type u} (s : alloc.vec.Vec α) (i :
 theorem alloc.vec.Vec.setSlice!_getElem!_prefix {α} [Inhabited α]
   (s : alloc.vec.Vec α) (s' : List α) (i j : ℕ) (h : j < i) :
   (s.setSlice! i s')[j]! = s[j]! := by
-  simp only [Vec.setSlice!, Vec.getElem!_Nat_eq]
+  rw [Vec.getElem!_Nat_eq]
+  simp only [Vec.setSlice!]
   simp_lists
 
 @[simp_lists_safe, grind =, agrind =]
@@ -492,7 +509,8 @@ theorem alloc.vec.Vec.setSlice!_getElem_prefix {α}
   have hj' : j < (s.setSlice! i s').length := by
     simpa [Vec.setSlice!_length] using h.2
   have h1 : (s.setSlice! i s')[j]? = s[j]? := by
-    simp only [Vec.getElem?_Nat_eq, Vec.setSlice!]
+    rw [Vec.getElem?_Nat_eq]
+    simp only [Vec.setSlice!]
     simp_lists [List.setSlice!_getElem?_prefix]
   simpa [Vec.getElem?_Nat_eq, Vec.getElem_Nat_eq,
     List.getElem?_eq_getElem hj', List.getElem?_eq_getElem h.2] using h1
@@ -501,7 +519,8 @@ theorem alloc.vec.Vec.setSlice!_getElem_prefix {α}
 theorem alloc.vec.Vec.setSlice!_getElem!_middle {α} [Inhabited α]
   (s : alloc.vec.Vec α) (s' : List α) (i j : ℕ) (h : i ≤ j ∧ j - i < s'.length ∧ j < s.length) :
   (s.setSlice! i s')[j]! = s'[j - i]! := by
-  simp only [Vec.setSlice!, Vec.getElem!_Nat_eq]
+  rw [Vec.getElem!_Nat_eq]
+  simp only [Vec.setSlice!]
   simp_lists
 
 @[simp_lists_safe, grind =, agrind =]
@@ -512,7 +531,8 @@ theorem alloc.vec.Vec.setSlice!_getElem_middle {α}
     simpa [Vec.setSlice!_length] using h.2.2
   have hji : j - i < s'.length := h.2.1
   have h1 : (s.setSlice! i s')[j]? = s'[j - i]? := by
-    simp only [Vec.getElem?_Nat_eq, Vec.setSlice!]
+    rw [Vec.getElem?_Nat_eq]
+    simp only [Vec.setSlice!]
     simp_lists [List.setSlice!_getElem?_middle]
   simpa [Vec.getElem?_Nat_eq, Vec.getElem_Nat_eq,
     List.getElem?_eq_getElem hj', List.getElem?_eq_getElem hji] using h1
@@ -520,7 +540,8 @@ theorem alloc.vec.Vec.setSlice!_getElem_middle {α}
 theorem alloc.vec.Vec.setSlice!_getElem!_suffix {α} [Inhabited α]
   (s : alloc.vec.Vec α) (s' : List α) (i j : ℕ) (h : i + s'.length ≤ j) :
   (s.setSlice! i s')[j]! = s[j]! := by
-  simp only [Vec.setSlice!, Vec.getElem!_Nat_eq]
+  rw [Vec.getElem!_Nat_eq]
+  simp only [Vec.setSlice!]
   simp_lists
 
 theorem alloc.vec.Vec.setSlice!_getElem_suffix {α}
@@ -529,7 +550,8 @@ theorem alloc.vec.Vec.setSlice!_getElem_suffix {α}
   have hj' : j < (s.setSlice! i s').length := by
     simpa [Vec.setSlice!_length] using h.2
   have h1 : (s.setSlice! i s')[j]? = s[j]? := by
-    simp only [Vec.getElem?_Nat_eq, Vec.setSlice!]
+    rw [Vec.getElem?_Nat_eq]
+    simp only [Vec.setSlice!]
     simp_lists [List.setSlice!_getElem?_suffix]
   simpa [Vec.getElem?_Nat_eq, Vec.getElem_Nat_eq,
     List.getElem?_eq_getElem hj', List.getElem?_eq_getElem h.2] using h1
diff --git a/backends/lean/Aeneas/Std/WP.lean b/backends/lean/Aeneas/Std/WP.lean
index 4acf11c26..0139ac434 100644
--- a/backends/lean/Aeneas/Std/WP.lean
+++ b/backends/lean/Aeneas/Std/WP.lean
@@ -8,8 +8,8 @@ namespace Aeneas.Std.WP
 
 open Std Result
 
-def Post α := (α -> Prop)
-def Pre := Prop
+@[reducible] def Post α := (α -> Prop)
+@[reducible] def Pre := Prop
 
 def Wp α := Post α → Pre
 
@@ -37,7 +37,7 @@ theorem spec_dspec (α) (x : Result α) (p: Post α) : spec x p → dspec x p :=
 theorem dspec_admissible {α} (p : Post α )
   : Lean.Order.admissible (fun x => dspec x p) := by
   apply Lean.Order.admissible_flatOrder
-  simp [dspec]
+  simp [dspec, Lean.Order.FlatOrder.mk]
 
 /-- Variant of `uncurry` used to decompose tuples in post-conditions.
 
@@ -764,7 +764,7 @@ example (x : Nat) :
 
 private theorem massert_spec' (b : Prop) [Decidable b] (h : b) :
   massert b ⦃ _ => True ⦄ := by
-  grind [massert]
+  simp only [massert, if_pos h, spec_ok]
 
 @[simp]
 theorem qimp_spec_unit {α} (P : Unit → Prop) (k : Unit → Result α) (Q : α → Prop) :
@@ -791,11 +791,9 @@ example :
   --
   apply spec_bind'
   · apply massert_spec'; omega
-  simp -failIfUnchanged only [qimp_spec_unit, forall_const]
-  --
-  apply spec_mono'
-  · apply massert_spec'; omega
-  simp -failIfUnchanged only [qimp_unit, forall_const]
+  -- eliminate the quantifier over the `()` output and the trivial precondition
+  intro _ _
+  apply massert_spec'; omega
 
 /- Example with a post-condition manipulating an ∃ -/
 example (zero : List Nat → Result (List Nat))
@@ -809,9 +807,9 @@ example (zero : List Nat → Result (List Nat))
   apply spec_bind'
   · apply zero_spec
   simp -failIfUnchanged only [qimp_spec_iff, imp_exists_iff]
-  rintro s' h0 h1
+  rintro s' h0
   --
-  simp only [pure, spec_ok]
+  simp only [pure, spec_ok, imp, implies_true]
 
 
 end Aeneas.Std.WP
@@ -944,7 +942,16 @@ theorem loop.spec {α : Type u} {β : Type v} {γ : Type w}
   apply @wf.wf.fix γ (fun x' =>
     ∀ x, measure x = x' →
     inv x → loop body x ⦃ post ⦄)
-  grind [loop]
+  intro x1 IH x2 hmeas hinv2
+  -- `body x2` succeeds and its result satisfies the loop invariant post-condition
+  obtain ⟨r, hbr, hr⟩ := WP.spec_imp_exists (hBody x2 hinv2)
+  rw [loop.eq_def, hbr]
+  cases r with
+  | done y => simpa using hr
+  | cont x' =>
+    obtain ⟨hinv', hrel⟩ := hr
+    -- the measure strictly decreases, so we can conclude by well-founded recursion
+    exact IH (measure x') (hmeas ▸ hrel) x' rfl hinv'
 
 theorem loop.spec_decr_nat {α : Type u} {β : Type v}
   (measure : α → Nat)
diff --git a/backends/lean/Aeneas/Tactic/Simproc/ReduceZMod/ReduceZMod.lean b/backends/lean/Aeneas/Tactic/Simproc/ReduceZMod/ReduceZMod.lean
index 4e63f80b2..e19f8564c 100644
--- a/backends/lean/Aeneas/Tactic/Simproc/ReduceZMod/ReduceZMod.lean
+++ b/backends/lean/Aeneas/Tactic/Simproc/ReduceZMod/ReduceZMod.lean
@@ -80,10 +80,11 @@ simproc reduceZModInv (@Inv.inv _ (ZMod.instInv _) _) := fun e => do
 simproc reduceZModPow
   (@HPow.hPow _ Nat _
       (@instHPow _ Nat
-        (@Monoid.toPow _
-          (@MonoidWithZero.toMonoid _
-            (@Semiring.toMonoidWithZero _
-              (@CommSemiring.toSemiring _ (@CommRing.toCommSemiring _ (ZMod.commRing _)))))))
+        (@NPow.toPow _
+          (@Monoid.toNPow _
+            (@MonoidWithZero.toMonoid _
+              (@Semiring.toMonoidWithZero _
+                (@CommSemiring.toSemiring _ (@CommRing.toCommSemiring _ (ZMod.commRing _))))))))
       _ _) := fun e => do
   trace[ReduceZMod] "Visiting: {e}"
   match e.consumeMData.getAppFnArgs with
diff --git a/backends/lean/Aeneas/Tactic/Solver/BvTac/BvTac.lean b/backends/lean/Aeneas/Tactic/Solver/BvTac/BvTac.lean
index 65d1fca39..b9719b36c 100644
--- a/backends/lean/Aeneas/Tactic/Solver/BvTac/BvTac.lean
+++ b/backends/lean/Aeneas/Tactic/Solver/BvTac/BvTac.lean
@@ -7,7 +7,7 @@ namespace Aeneas.BvTac
 open Lean Lean.Meta Lean.Parser.Tactic Lean.Elab.Tactic
 open Bvify Utils
 
-structure Config extends Lean.Elab.Tactic.BVDecide.Frontend.BVDecideConfig, Bvify.Config where
+structure Config extends Lean.Elab.Tactic.BVDecide.BVDecideConfig, Bvify.Config where
 
 declare_config_elab elabConfig Config
 
@@ -79,7 +79,7 @@ partial def bvTacPreprocess (config : Config) (n : Option Expr): TacticM Unit :=
 elab "bv_tac_preprocess" config:Parser.Tactic.optConfig n:(colGt term)? : tactic => do
   bvTacPreprocess (← elabConfig config) (← optElabTerm n)
 
-open Lean.Elab.Tactic.BVDecide.Frontend Lean.Elab in
+open Lean.Meta.Tactic.BVDecide Lean.Elab in
 /-- `bv_tac n` solves goals about bit-vectors.
 
 **Usage**: `bv_tac n` where `n` is the bitwidth to use for the bit-vectors.
@@ -118,9 +118,9 @@ elab "bv_tac" config:Parser.Tactic.optConfig n:(colGt term)? : tactic =>
   -- Call bv_decide
   IO.FS.withTempFile fun _ lratFile => do
     let config := config.toBVDecideConfig
-    let cfg ← BVDecide.Frontend.TacticContext.new lratFile config
+    let cfg ← Lean.Meta.Tactic.BVDecide.TacticContext.new lratFile config
     liftMetaFinishingTactic fun g => do
-      discard <| bvDecide g cfg
+      discard <| Lean.Meta.Tactic.BVDecide.bvDecide g cfg
 
 /-!
 # Tests
diff --git a/backends/lean/Aeneas/Tactic/Step/DspecInduction.lean b/backends/lean/Aeneas/Tactic/Step/DspecInduction.lean
index 25ee63dd1..f91d2d1a3 100644
--- a/backends/lean/Aeneas/Tactic/Step/DspecInduction.lean
+++ b/backends/lean/Aeneas/Tactic/Step/DspecInduction.lean
@@ -94,7 +94,7 @@ theorem WP_func_admissible (α β : Type) (arg) (post)
   : Order.admissible fun (f : α → Result β) => WP.dspec (f arg) post := by
   apply Lean.Order.admissible_apply (fun _ fx => WP.dspec fx _)
   apply Lean.Order.admissible_flatOrder
-  simp only [WP.dspec]
+  simp only [WP.dspec, Lean.Order.FlatOrder.mk]
 
 def getParamNames (ty : Expr) : MetaM (Array Name) := do
   forallTelescope ty fun xs _ => do
diff --git a/backends/lean/Aeneas/Tactic/Step/Init.lean b/backends/lean/Aeneas/Tactic/Step/Init.lean
index 5b0fd16fe..d2d14c064 100644
--- a/backends/lean/Aeneas/Tactic/Step/Init.lean
+++ b/backends/lean/Aeneas/Tactic/Step/Init.lean
@@ -741,7 +741,8 @@ theorem intro_uncurry' (p : α × β → Prop) : p = uncurry' (fun x y => p (x,
   simp only
 
 theorem lift_to_spec x (p0 p1 : α → Prop) (h0 : p0 x) (h1 : p0 = p1) : spec (Std.lift x) p1 := by
-  grind [spec, Std.lift]
+  simp only [Std.lift, spec_ok, ← h1]
+  exact h0
 
 namespace Test
 
diff --git a/backends/lean/Aeneas/Tactic/Step/Step.lean b/backends/lean/Aeneas/Tactic/Step/Step.lean
index 3abf08fd6..48afa17b9 100644
--- a/backends/lean/Aeneas/Tactic/Step/Step.lean
+++ b/backends/lean/Aeneas/Tactic/Step/Step.lean
@@ -1022,11 +1022,10 @@ def tryApply (info : SpecInfo) (lifting : Option LiftingInfo) (args : Args) (isL
     | some th => do
       trace[Step] "Lookuped up {kind}: {th}"
       -- Apply the theorem
-      let res ← do
-        try
-          let res ← stepWith info lifting args isLet fExpr th
-          pure (some res)
-        catch _ => pure none
+      try
+        let res ← stepWith info lifting args isLet fExpr th
+        pure (some res)
+      catch _ => pure none
   match res with
   | some res => pure (some res)
   | none => pure none
@@ -2069,7 +2068,7 @@ h1 : ∀ (i : ℕ) (x : i < s.length), s'[i] = 0#u32
 
   -- `Inhabited α` is not necessary: we add it for the purpose of testing
   theorem get_spec {α} [Inhabited α] (x : Option α) (h : x.isSome) : get x ⦃ _ => True ⦄ := by
-    cases x <;> grind [get]
+    cases x <;> simp_all [get]
 
   example {α} [Inhabited α] (x : Option α) (h : x.isSome) : get x ⦃ _ => True ⦄ := by
     step with get_spec
@@ -2173,7 +2172,7 @@ h1 : ∀ (i : ℕ) (x : i < s.length), s'[i] = 0#u32
         intros y
         apply Lean.Order.admissible_apply (fun _ fx => WP.dspec fx _)
         apply Lean.Order.admissible_flatOrder
-        simp only [WP.dspec]
+        simp only [WP.dspec, Lean.Order.FlatOrder.mk]
       · intros
         simp only
         split
diff --git a/backends/lean/Aeneas/Tactic/Step/StepArraySpec.lean b/backends/lean/Aeneas/Tactic/Step/StepArraySpec.lean
index 715196f73..e653d60e3 100644
--- a/backends/lean/Aeneas/Tactic/Step/StepArraySpec.lean
+++ b/backends/lean/Aeneas/Tactic/Step/StepArraySpec.lean
@@ -107,7 +107,7 @@ def parseStepArraySpec
   match stx with
   | `($[$vis]? step_array_spec (name := $thm_name:ident) $array:ident [ $i:ident ]! { $x:ident => $pred:term } by $tac:tacticSeq) => do
     -- Compute the visibility of the `step` theorem
-    let vis : TSyntax `declModifiers ← do
+    let vis : TSyntax `Lean.Parser.Command.declModifiers ← do
       match vis with
       | none => `(declModifiers|@[step])
       | some vis =>
diff --git a/backends/lean/Aeneas/Tactic/Step/StepStar.lean b/backends/lean/Aeneas/Tactic/Step/StepStar.lean
index bfbfd9312..c7eb4afd7 100644
--- a/backends/lean/Aeneas/Tactic/Step/StepStar.lean
+++ b/backends/lean/Aeneas/Tactic/Step/StepStar.lean
@@ -463,7 +463,7 @@ where
       {simpThms := #[← Step.stepSimpExt.getTheorems]}
       (.targets #[] true)
     /- We may have proven the goal already -/
-    let tac : Array Syntax.Tactic ← do
+    let tac : Array (TaskOrDone (Option Syntax.Tactic)) ← do
       let genSimp : Bool ← do
         if r.isNone then pure true
         else do
diff --git a/backends/lean/Aeneas/Tactic/Step/Tests/TupleDestruct.lean b/backends/lean/Aeneas/Tactic/Step/Tests/TupleDestruct.lean
index c2fe9364b..f483a0a20 100644
--- a/backends/lean/Aeneas/Tactic/Step/Tests/TupleDestruct.lean
+++ b/backends/lean/Aeneas/Tactic/Step/Tests/TupleDestruct.lean
@@ -35,49 +35,57 @@ private theorem sixNats_spec : sixNats ⦃ ((a, b), c) ((d, e), f) => a = 3 ∧
 /--
 warning: Variable name `a` is not explicitly referenced.
 
-The binding can be removed (if unused) or named `_` (if used implicitly).
+Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
+  [apply] _a
 
 Note: This linter can be disabled with `set_option linter.unusedVariables false`
 ---
 warning: Variable name `b` is not explicitly referenced.
 
-The binding can be removed (if unused) or named `_` (if used implicitly).
+Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
+  [apply] _b
 
 Note: This linter can be disabled with `set_option linter.unusedVariables false`
 ---
 warning: Variable name `c` is not explicitly referenced.
 
-The binding can be removed (if unused) or named `_` (if used implicitly).
+Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
+  [apply] _c
 
 Note: This linter can be disabled with `set_option linter.unusedVariables false`
 ---
 warning: Variable name `d` is not explicitly referenced.
 
-The binding can be removed (if unused) or named `_` (if used implicitly).
+Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
+  [apply] _d
 
 Note: This linter can be disabled with `set_option linter.unusedVariables false`
 ---
 warning: Variable name `b` is not explicitly referenced.
 
-The binding can be removed (if unused) or named `_` (if used implicitly).
+Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
+  [apply] _b
 
 Note: This linter can be disabled with `set_option linter.unusedVariables false`
 ---
 warning: Variable name `c` is not explicitly referenced.
 
-The binding can be removed (if unused) or named `_` (if used implicitly).
+Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
+  [apply] _c
 
 Note: This linter can be disabled with `set_option linter.unusedVariables false`
 ---
 warning: Variable name `e` is not explicitly referenced.
 
-The binding can be removed (if unused) or named `_` (if used implicitly).
+Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
+  [apply] _e
 
 Note: This linter can be disabled with `set_option linter.unusedVariables false`
 ---
 warning: Variable name `h` is not explicitly referenced.
 
-The binding can be removed (if unused) or named `_` (if used implicitly).
+Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
+  [apply] _h
 
 Note: This linter can be disabled with `set_option linter.unusedVariables false`
 -/
diff --git a/backends/lean/AeneasMeta/BvEnumToBitVec.lean b/backends/lean/AeneasMeta/BvEnumToBitVec.lean
index 2fadf4bc0..54f9d66ef 100644
--- a/backends/lean/AeneasMeta/BvEnumToBitVec.lean
+++ b/backends/lean/AeneasMeta/BvEnumToBitVec.lean
@@ -3,7 +3,7 @@ Copyright (c) 2025. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 -/
 import Lean
-import Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Enums
+import Lean.Meta.Tactic.BVDecide.Normalize.Enums
 
 /-!
 # Eagerly realizing `bv_decide`'s enum conversion constants
@@ -44,7 +44,7 @@ module, turning the lazy per-use realisation into a single deterministic one.
 namespace Aeneas
 
 open Lean Meta Elab
-open Lean.Elab.Tactic.BVDecide.Frontend.Normalize
+open Lean.Meta.Tactic.BVDecide.Normalize
 
 /-- Marker class enabling `deriving BvEnumToBitVec` on an enum inductive.
 
@@ -69,11 +69,14 @@ def realizeBvEnumToBitVec (declName : Name) : CoreM Unit := do
       (parameter-free with only nullary constructors); \
       `bv_decide` only synthesises `enumToBitVec` for such types."
   enableRealizationsForConst declName
-  let act : MetaM Unit := do
-    discard <| getEnumToBitVecFor declName
-    discard <| getEnumToBitVecLeFor declName
-    discard <| getEqIffEnumToBitVecEqFor declName
-  discard <| act.run' {} {}
+  -- `bv_decide` registers these three constants as *reserved names* and realises
+  -- them lazily through a reserved-name action (see
+  -- `Lean.Meta.Tactic.BVDecide.Normalize`). The realiser functions themselves are
+  -- private to that module, so we trigger realisation by name instead. Only
+  -- `enumToBitVecSuffix` is exported; the other two suffixes are inlined here.
+  executeReservedNameAction (.str declName enumToBitVecSuffix)
+  executeReservedNameAction (.str declName "enumToBitVec_le")
+  executeReservedNameAction (.str declName "eq_iff_enumToBitVec_eq")
 
 /-- `#define_bv_decide_toBitVec T` eagerly realises `bv_decide`'s enum
 conversion constants for the enum inductive `T` in the current module.
diff --git a/backends/lean/AeneasMeta/Simp/Simp.lean b/backends/lean/AeneasMeta/Simp/Simp.lean
index 322ea73a5..455376f48 100644
--- a/backends/lean/AeneasMeta/Simp/Simp.lean
+++ b/backends/lean/AeneasMeta/Simp/Simp.lean
@@ -116,7 +116,7 @@ where
     let freshFVarIds ←
       match result? with
       | none => replaceMainGoal []; pure none
-      | some (fvars, mvarId) => replaceMainGoal [mvarId]; pure fvars
+      | some (fvars, mvarId) => replaceMainGoal [mvarId]; pure (some fvars)
     /- We need to filter the `fvarIdsToSimp` to remove those which have been replaced with fresh fvars -/
     let fvars ← do
       match freshFVarIds with
diff --git a/backends/lean/lake-manifest.json b/backends/lean/lake-manifest.json
index 276c521fe..033e1f3d4 100644
--- a/backends/lean/lake-manifest.json
+++ b/backends/lean/lake-manifest.json
@@ -5,17 +5,17 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "fabf563a7c95a166b8d7b6efca11c8b4dc9d911f",
+   "rev": "51e6992efd06126df61a496bebf8f49482a4e129",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.31.0",
+   "inputRev": "v4.33.0-rc2",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "63045536fe95024e6c18fc7b48e03f506701c5bc",
+   "rev": "123d15766ba49356c02ebad2a4462dfe12d79899",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843",
+   "rev": "f5c090429dff3cf66cb65562526c9ea6e8edfbcb",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "5c7542ed018c78194f1e2b903eaf6a792b74c03d",
+   "rev": "bb3469a87774349fe01898d8bf2fc6a1ce6411ca",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "24b0d9dc081c5423f8eec7e866c441e5184f29d9",
+   "rev": "222c58dad7706a6e7cae46c0edd65ea881d3ee27",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e3cb2f741431ce31bf73549fb52316a57368b06f",
+   "rev": "7db8190085343afde2f5d2cdcc9bac719b6ec02c",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "f46324995fca5f0483b742e4eb4daec7f4ee50d2",
+   "rev": "ef42f8944eaf5b6cbfbe75d1917d824c7dd6cf33",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "fa08db58b30eb033edcdab331bba000827f9f785",
+   "rev": "76e1c118b0700b4ceafe99532e887d6431625e1a",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,10 +85,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "92564e5770e4d09f2d86dfbf8ada1e9c715b384c",
+   "rev": "1319485273bf87833fa472afbcefdedecb16b45f",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.31.0",
+   "inputRev": "v4.33.0-rc2",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "aeneas",
diff --git a/backends/lean/lakefile.lean b/backends/lean/lakefile.lean
index bc2d29015..d8b44fb33 100644
--- a/backends/lean/lakefile.lean
+++ b/backends/lean/lakefile.lean
@@ -3,11 +3,22 @@ open Lake DSL
 
 -- Important: mathlib imports std4 and quote4: we mustn't add a `require std4` line
 require mathlib from git
-  "https://github.com/leanprover-community/mathlib4.git" @ "v4.31.0"
+  "https://github.com/leanprover-community/mathlib4.git" @ "v4.33.0-rc2"
 
 package «aeneas» where
   preferReleaseBuild := true
   buildArchive := s!"lean-build-aeneas-{System.Platform.target}.tar.gz"
+  -- Lean v4.33 newly enables/strengthens these linters. They fire on generated
+  -- Rust-path declaration names (`dupNamespace`, e.g. `core.clone…​.clone`),
+  -- intentional `Prop`-valued definitions (`defProp`), and `open Std` now that
+  -- `Lean.Std` also exists (`ambiguousOpen`). None are cleanly fixable in the
+  -- generated / spec code, so we disable them to keep `lake build --iofail`
+  -- (used in CI) green after the toolchain bump.
+  leanOptions := #[
+    ⟨`weak.linter.dupNamespace, false⟩,
+    ⟨`weak.linter.defProp, false⟩,
+    ⟨`weak.linter.ambiguousOpen, false⟩
+  ]
 
 @[default_target] lean_lib «Aeneas» {}
 
diff --git a/backends/lean/lean-toolchain b/backends/lean/lean-toolchain
index 18640c8b0..c084c7fbe 100644
--- a/backends/lean/lean-toolchain
+++ b/backends/lean/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.31.0
+leanprover/lean4:v4.33.0-rc2
diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean
index c63c42845..31b9e8591 100644
--- a/tests/lean/Hashmap/Properties.lean
+++ b/tests/lean/Hashmap/Properties.lean
@@ -1000,7 +1000,7 @@ theorem get_mut_spec {α} (hm : HashMap α) (key : Usize) (hInv : hm.inv) :
     -- TODO: tactic to automate this
     have hSlotsEq :
       hm.slots.set hash_mod ((hm.slots.val)[(key.val % (hm.slots.val).length)]) = hm.slots := by
-      simp_all [alloc.vec.Vec.set]
+      apply Subtype.ext; simp_all [alloc.vec.Vec.set]
     simp_all
   · grind
 
diff --git a/tests/lean/Tutorial/Exercises.lean b/tests/lean/Tutorial/Exercises.lean
index 492a8dc47..42b1f3316 100644
--- a/tests/lean/Tutorial/Exercises.lean
+++ b/tests/lean/Tutorial/Exercises.lean
@@ -1,8 +1,12 @@
 import Aeneas
 open Aeneas Std Result
 
+-- Workaround for leanprover/lean4#14521: the default `get_elem_tactic` (`grind`)
+-- emits kernel-invalid proofs when an index bound depends on `_ ≠ 0#uN` (the
+-- BitVec width `numBits U32` is defeq but not syntactically `32`). `scalar_tac`
+-- discharges these bounds correctly; `grind` stays as a fallback.
 local macro_rules
-| `(tactic| get_elem_tactic) => `(tactic| grind)
+| `(tactic| get_elem_tactic) => `(tactic| first | scalar_tac | grind)
 
 set_option maxHeartbeats 1000000
 
diff --git a/tests/lean/Tutorial/Solutions.lean b/tests/lean/Tutorial/Solutions.lean
index 14571b756..dead789f7 100644
--- a/tests/lean/Tutorial/Solutions.lean
+++ b/tests/lean/Tutorial/Solutions.lean
@@ -2,8 +2,12 @@ import Aeneas
 import Tutorial.Tutorial
 open Aeneas Std Result
 
+-- Workaround for leanprover/lean4#14521: the default `get_elem_tactic` (`grind`)
+-- emits kernel-invalid proofs when an index bound depends on `_ ≠ 0#uN` (the
+-- BitVec width `numBits U32` is defeq but not syntactically `32`). `scalar_tac`
+-- discharges these bounds correctly; `grind` stays as a fallback.
 local macro_rules
-| `(tactic| get_elem_tactic) => `(tactic| grind)
+| `(tactic| get_elem_tactic) => `(tactic| first | scalar_tac | grind)
 
 set_option maxHeartbeats 1000000
 
@@ -135,10 +139,30 @@ theorem list_nth_mut1_spec'' {T: Type} [Inhabited T] (l : CList T) (i : U32)
   unfold list_nth_mut1 list_nth_mut1_loop
   /- `step*` repeatedly applies `step`, while doing a case disjunction whenever it
       encounters a branching. Note that one can automatically generate the corresponding
-      proof script by using `step*?`. -/
-  step*
-  simp
-  simp_lists [*]
+      proof script by using `step*?`.
+
+      Workaround for leanprover/lean4#14521: `step*` closes leaf goals with `agrind`,
+      which on the `i ≠ 0#u32` branch here emits a kernel-invalid proof (the BitVec
+      width `numBits U32` is defeq but not syntactically `32`). Until that upstream
+      `grind` bug is fixed, we spell out the case analysis explicitly (as `step*?`
+      would generate it), closing the branches with `scalar_tac`/`simp` instead. -/
+  split
+  · rename_i hd tl
+    split
+    · simp
+      split_conjs
+      · simp_all
+      · intro x
+        simp_all
+    · simp at *
+      step as ⟨ i1, _, hi ⟩
+      step as ⟨ tl1, back ⟩
+      simp
+      split_conjs
+      · simp_lists [*]
+      · intro x'
+        simp [*]
+  · simp at h
 
 /-- Theorem about `list_tail_loop`: verbose version -/
 @[step]
diff --git a/tests/lean/lake-manifest.json b/tests/lean/lake-manifest.json
index 316a46c9a..4788db62e 100644
--- a/tests/lean/lake-manifest.json
+++ b/tests/lean/lake-manifest.json
@@ -12,17 +12,17 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "fabf563a7c95a166b8d7b6efca11c8b4dc9d911f",
+   "rev": "51e6992efd06126df61a496bebf8f49482a4e129",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.31.0",
+   "inputRev": "v4.33.0-rc2",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "63045536fe95024e6c18fc7b48e03f506701c5bc",
+   "rev": "123d15766ba49356c02ebad2a4462dfe12d79899",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -32,7 +32,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843",
+   "rev": "f5c090429dff3cf66cb65562526c9ea6e8edfbcb",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -42,7 +42,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "5c7542ed018c78194f1e2b903eaf6a792b74c03d",
+   "rev": "bb3469a87774349fe01898d8bf2fc6a1ce6411ca",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -52,7 +52,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "24b0d9dc081c5423f8eec7e866c441e5184f29d9",
+   "rev": "222c58dad7706a6e7cae46c0edd65ea881d3ee27",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -62,7 +62,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e3cb2f741431ce31bf73549fb52316a57368b06f",
+   "rev": "7db8190085343afde2f5d2cdcc9bac719b6ec02c",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -72,7 +72,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "f46324995fca5f0483b742e4eb4daec7f4ee50d2",
+   "rev": "ef42f8944eaf5b6cbfbe75d1917d824c7dd6cf33",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -82,7 +82,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "fa08db58b30eb033edcdab331bba000827f9f785",
+   "rev": "76e1c118b0700b4ceafe99532e887d6431625e1a",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -92,10 +92,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "92564e5770e4d09f2d86dfbf8ada1e9c715b384c",
+   "rev": "1319485273bf87833fa472afbcefdedecb16b45f",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.31.0",
+   "inputRev": "v4.33.0-rc2",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "tests",
diff --git a/tests/lean/lean-toolchain b/tests/lean/lean-toolchain
index 18640c8b0..c084c7fbe 100644
--- a/tests/lean/lean-toolchain
+++ b/tests/lean/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.31.0
+leanprover/lean4:v4.33.0-rc2