fixes for leanprover/lean4#5988

Aesop/RuleSet.lean

@@ -377,7 +377,7 @@ def LocalRuleSet.erase (rs : LocalRuleSet) (f : RuleFilter) :
       if SimpTheorems.containsDecl simpTheorems decl then
         let origin := .decl decl (inv := false)
         simpTheoremsArray' :=
-          ⟨simpTheoremsArray'.fst.set ⟨i, i_valid⟩
+          ⟨simpTheoremsArray'.fst.set i
             (name, simpTheorems.eraseCore origin),
            by simp [simpTheoremsArray'.snd, Array.size_set]⟩
         anyErased := true

Aesop/Util/Basic.lean

@@ -117,7 +117,7 @@ private partial def filterTrieM [Monad m] [Inhabited σ] (f : σ → α → m σ
       if h : i < children.size then
         let (key, t) := children[i]'h
         let (t, acc) ← filterTrieM f p acc t
-        go acc (i + 1) (children.set ⟨i, h⟩ (key, t))
+        go acc (i + 1) (children.set i (key, t))
       else
         return (children, acc)
 

lake-manifest.json

@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "76e9ebe4176d29cb9cc89c669ab9f1ce32b33c3d",
+   "rev": "4fbc598626f02cae3d60708c04a09c311bb60369",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "lean-pr-testing-5988",
    "inherited": false,
    "configFile": "lakefile.toml"}],
  "name": "aesop",

lakefile.toml

@@ -6,7 +6,7 @@ precompileModules = false # We would like to turn this on, but it breaks the Mat
 [[require]]
 name = "batteries"
 git = "https://github.com/leanprover-community/batteries"
-rev = "main"
+rev = "lean-pr-testing-5988"
 
 [[lean_lib]]
 name = "Aesop"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.14.0-rc1
+leanprover/lean4-pr-releases:pr-release-5988