diff --git a/Aesop/RuleSet.lean b/Aesop/RuleSet.lean
index 82bec29..c2cc052 100644
--- a/Aesop/RuleSet.lean
+++ b/Aesop/RuleSet.lean
@@ -372,7 +372,7 @@ def LocalRuleSet.erase (rs : LocalRuleSet) (f : RuleFilter) :
   if let some decl := f.matchesSimpTheorem? then
     for h : i in [:rs.simpTheoremsArray.size] do
       have i_valid : i < simpTheoremsArray'.fst.size := by
-        simp_all [Membership.mem, simpTheoremsArray'.snd]
+        simp_all +zetaDelta [Membership.mem, simpTheoremsArray'.snd]
       let (name, simpTheorems) := simpTheoremsArray'.fst[i]
       if SimpTheorems.containsDecl simpTheorems decl then
         let origin := .decl decl (inv := false)
@@ -383,7 +383,7 @@ def LocalRuleSet.erase (rs : LocalRuleSet) (f : RuleFilter) :
         anyErased := true
   let simpTheoremsArray := simpTheoremsArray'.fst
   let simpTheoremsArrayNonempty : 0 < simpTheoremsArray.size := by
-    simp [simpTheoremsArray'.snd, rs.simpTheoremsArrayNonempty]
+    simp [simpTheoremsArray, simpTheoremsArray'.snd, rs.simpTheoremsArrayNonempty]
   let rs := { rs with
     localNormSimpRules, simpTheoremsArray, simpTheoremsArrayNonempty
   }
diff --git a/AesopTest/RulePattern.lean b/AesopTest/RulePattern.lean
index 2b40167..0faf31f 100644
--- a/AesopTest/RulePattern.lean
+++ b/AesopTest/RulePattern.lean
@@ -23,8 +23,8 @@ example (m n : Nat) : (↑m : Int) < 0 ∧ (↑n : Int) > 0 := by
   set_option aesop.check.script false in
   aesop!
   all_goals
-    guard_hyp fwd_1 : 0 ≤ (n : Int)
-    guard_hyp fwd_2 : 0 ≤ (m : Int)
+    guard_hyp fwd_2 : 0 ≤ (n : Int)
+    guard_hyp fwd_1 : 0 ≤ (m : Int)
     falso
 
 @[aesop safe forward (pattern := min x y)]
@@ -44,8 +44,8 @@ axiom triangle (a b : Int) : |a + b| ≤ |a| + |b|
 
 example : |a + b| ≤ |c + d| := by
   aesop!
-  guard_hyp fwd   : |c + d| ≤ |c| + |d|
-  guard_hyp fwd_1 : |a + b| ≤ |a| + |b|
+  guard_hyp fwd_1 : |c + d| ≤ |c| + |d|
+  guard_hyp fwd   : |a + b| ≤ |a| + |b|
   falso
 
 @[aesop safe apply (pattern := (0 : Nat))]
diff --git a/AesopTest/SaturatePerformance.lean b/AesopTest/SaturatePerformance.lean
index b57ad04..d4dfa8c 100644
--- a/AesopTest/SaturatePerformance.lean
+++ b/AesopTest/SaturatePerformance.lean
@@ -41,11 +41,11 @@ import Aesop
 error: unsolved goals
 α : Type u_1
 l0 l1 l2 : List α
-fwd : (l0 ++ l1).length ≥ 0
-fwd_1 : (l0 ++ l1 ++ l2).length ≥ 0
-fwd_2 : l2.length ≥ 0
-fwd_3 : l0.length ≥ 0
-fwd_4 : l1.length ≥ 0
+fwd : l1.length ≥ 0
+fwd_1 : (l0 ++ l1).length ≥ 0
+fwd_2 : (l0 ++ l1 ++ l2).length ≥ 0
+fwd_3 : l2.length ≥ 0
+fwd_4 : l0.length ≥ 0
 ⊢ (l0 ++ l1 ++ l2).length = l0.length + l1.length + l2.length
 -/
 #guard_msgs in
diff --git a/lake-manifest.json b/lake-manifest.json
index 4cd8e6d..0cc6366 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "9b9f4d0406d00baaae62d1a717b5aa854a2ae51d",
+   "rev": "13c202289cae0db69d997904de3c4d43c9222ea8",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",
diff --git a/lean-toolchain b/lean-toolchain
index 118d9e5..a8e9a39 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2024-11-20
+leanprover/lean4:nightly-2024-12-14