diff --git a/Aesop/Builder/Cases.lean b/Aesop/Builder/Cases.lean
index 914bae91..e45a4056 100644
--- a/Aesop/Builder/Cases.lean
+++ b/Aesop/Builder/Cases.lean
@@ -22,7 +22,7 @@ def check (decl : Name) (p : CasesPattern) : MetaM Unit :=
 
 def toIndexingMode (p : CasesPattern) : MetaM IndexingMode :=
   withoutModifyingState do
-    .hyps <$> DiscrTree.mkPath (← p.toExpr) discrTreeConfig
+    .hyps <$> (withConfigWithKey discrTreeConfig <| DiscrTree.mkPath (← p.toExpr))
 
 end CasesPattern
 
diff --git a/Aesop/Builder/Forward.lean b/Aesop/Builder/Forward.lean
index def5c30b..b7e8c6d5 100644
--- a/Aesop/Builder/Forward.lean
+++ b/Aesop/Builder/Forward.lean
@@ -34,7 +34,7 @@ private def forwardIndexingModeCore (type : Expr)
       match args.get? i with
       | some arg =>
         let argT := (← arg.mvarId!.getDecl).type
-        let keys ← DiscrTree.mkPath argT discrTreeConfig
+        let keys ← withConfigWithKey discrTreeConfig <| DiscrTree.mkPath argT
         return .hyps keys
       | none => throwError
         "aesop: internal error: immediate arg for forward rule is out of range"
diff --git a/Aesop/Frontend/RuleExpr.lean b/Aesop/Frontend/RuleExpr.lean
index 1cc31699..63b837ab 100644
--- a/Aesop/Frontend/RuleExpr.lean
+++ b/Aesop/Frontend/RuleExpr.lean
@@ -173,7 +173,7 @@ def elabSingleIndexingMode (stx : Syntax) : ElabM IndexingMode :=
     elabKeys (stx : Syntax) : ElabM (Array DiscrTree.Key) :=
       show TermElabM _ from withoutModifyingState do
         let e ← elabPattern stx
-        DiscrTree.mkPath (← instantiateMVars e) discrTreeConfig
+        withConfigWithKey discrTreeConfig <| DiscrTree.mkPath (← instantiateMVars e)
 
 def IndexingMode.elab (stxs : Array Syntax) : ElabM IndexingMode :=
   .or <$> stxs.mapM elabSingleIndexingMode
diff --git a/Aesop/Index.lean b/Aesop/Index.lean
index b0256dc7..65c10dd5 100644
--- a/Aesop/Index.lean
+++ b/Aesop/Index.lean
@@ -96,7 +96,7 @@ private def applicableByTargetRules (ri : Index α) (goal : MVarId)
     (include? : Rule α → Bool) :
     MetaM (Array (Rule α × Array IndexMatchLocation)) :=
   goal.withContext do
-    let rules ← ri.byTarget.getUnify (← goal.getType) discrTreeConfig
+    let rules ← withConfigWithKey discrTreeConfig <| ri.byTarget.getUnify (← goal.getType)
     let mut rs := Array.mkEmpty rules.size
       -- Assumption: include? is true for most rules.
     for r in rules do
@@ -114,7 +114,7 @@ private def applicableByHypRules (ri : Index α) (goal : MVarId)
     for localDecl in ← getLCtx do
       if localDecl.isImplementationDetail then
         continue
-      let rules ← ri.byHyp.getUnify localDecl.type discrTreeConfig
+      let rules ← withConfigWithKey discrTreeConfig <| ri.byHyp.getUnify localDecl.type
       for r in rules do
         if include? r then
           rs := rs.push (r, #[.hyp localDecl])
diff --git a/Aesop/Index/Basic.lean b/Aesop/Index/Basic.lean
index a1a65a1d..30889103 100644
--- a/Aesop/Index/Basic.lean
+++ b/Aesop/Index/Basic.lean
@@ -14,7 +14,7 @@ namespace Aesop
 
 -- This value controls whether we use 'powerful' reductions, e.g. iota, when
 -- indexing Aesop rules. See the `DiscrTree` docs for details.
-def discrTreeConfig : WhnfCoreConfig := { iota := false }
+def discrTreeConfig : ConfigWithKey := { iota := false : Config}.toConfigWithKey
 
 inductive IndexingMode : Type
   | unindexed
diff --git a/Aesop/RuleSet.lean b/Aesop/RuleSet.lean
index ec689567..82bec298 100644
--- a/Aesop/RuleSet.lean
+++ b/Aesop/RuleSet.lean
@@ -367,7 +367,7 @@ def LocalRuleSet.erase (rs : LocalRuleSet) (f : RuleFilter) :
       Σ' a : Array (Name × SimpTheorems), a.size = rs.simpTheoremsArray.size :=
     ⟨rs.simpTheoremsArray, rfl⟩
   if let some id := f.matchesLocalNormSimpRule? then
-    if let some idx := localNormSimpRules.findIdx? (·.id == id) then
+    if let some idx := localNormSimpRules.findFinIdx? (·.id == id) then
       localNormSimpRules := localNormSimpRules.eraseIdx idx
   if let some decl := f.matchesSimpTheorem? then
     for h : i in [:rs.simpTheoremsArray.size] do
@@ -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
diff --git a/Aesop/RuleTac/ElabRuleTerm.lean b/Aesop/RuleTac/ElabRuleTerm.lean
index e4aacc99..8ea79f1e 100644
--- a/Aesop/RuleTac/ElabRuleTerm.lean
+++ b/Aesop/RuleTac/ElabRuleTerm.lean
@@ -81,7 +81,7 @@ def elabRuleTermForSimpCore (goal : MVarId) (term : Term) (ctx : Simp.Context)
     elabSimpTheorems (mkSimpArgs term) ctx simprocs isSimpAll
 
 def checkElabRuleTermForSimp (term : Term) (isSimpAll : Bool) : ElabM Unit := do
-  let ctx := { simpTheorems := #[{}] }
+  let ctx ← Simp.mkContext (simpTheorems := #[{}] )
   let simprocs := #[{}]
   discard $ elabRuleTermForSimpCore (← read).goal term ctx simprocs isSimpAll
 
diff --git a/Aesop/RuleTac/Forward.lean b/Aesop/RuleTac/Forward.lean
index 34d113fe..5c7cfc4c 100644
--- a/Aesop/RuleTac/Forward.lean
+++ b/Aesop/RuleTac/Forward.lean
@@ -50,7 +50,7 @@ partial def makeForwardHyps (e : Expr) (pat? : Option RulePattern)
         (proofTypesAcc : Std.HashSet Expr) :
         MetaM (Array (Expr × Nat) × Array FVarId × Std.HashSet Expr) := do
       if h : i < immediateMVars.size then
-        let mvarId := immediateMVars.get ⟨i, h⟩
+        let mvarId := immediateMVars[i]
         let type ← mvarId.getType
         (← getLCtx).foldlM (init := (proofsAcc, usedHypsAcc, proofTypesAcc)) λ s@(proofsAcc, usedHypsAcc, proofTypesAcc) ldecl => do
           if ldecl.isImplementationDetail then
diff --git a/Aesop/Search/Expansion/Simp.lean b/Aesop/Search/Expansion/Simp.lean
index 5c0d6582..2e56133c 100644
--- a/Aesop/Search/Expansion/Simp.lean
+++ b/Aesop/Search/Expansion/Simp.lean
@@ -44,7 +44,7 @@ def addLetDeclsToSimpTheorems (ctx : Simp.Context) : MetaM Simp.Context := do
     if ldecl.hasValue && ! ldecl.isImplementationDetail then
       simpTheoremsArray := simpTheoremsArray.modify 0 λ simpTheorems =>
         simpTheorems.addLetDeclToUnfold ldecl.fvarId
-  return { ctx with simpTheorems := simpTheoremsArray }
+  return ctx.setSimpTheorems simpTheoremsArray
 
 def addLetDeclsToSimpTheoremsUnlessZetaDelta (ctx : Simp.Context) :
     MetaM Simp.Context := do
@@ -58,7 +58,7 @@ def simpGoal (mvarId : MVarId) (ctx : Simp.Context)
     (simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[])
     (stats : Simp.Stats := {}) : MetaM SimpResult := do
   let mvarIdOld := mvarId
-  let ctx := { ctx with config.failIfUnchanged := false }
+  let ctx := ctx.setFailIfUnchanged false
   let (result, { usedTheorems := usedSimps, .. }) ←
     Meta.simpGoal mvarId ctx simprocs discharge? simplifyTarget fvarIdsToSimp
       stats
@@ -89,7 +89,7 @@ def simpAll (mvarId : MVarId) (ctx : Simp.Context)
     (simprocs : Simp.SimprocsArray) (stats : Simp.Stats := {}) :
     MetaM SimpResult :=
   mvarId.withContext do
-    let ctx := { ctx with config.failIfUnchanged := false }
+    let ctx := ctx.setFailIfUnchanged false
     let ctx ← addLetDeclsToSimpTheoremsUnlessZetaDelta ctx
     match ← Lean.Meta.simpAll mvarId ctx simprocs stats with
     | (none, stats) => return .solved stats.usedTheorems
diff --git a/Aesop/Search/SearchM.lean b/Aesop/Search/SearchM.lean
index 4c0884b8..ba803bf9 100644
--- a/Aesop/Search/SearchM.lean
+++ b/Aesop/Search/SearchM.lean
@@ -15,7 +15,8 @@ open Lean.Meta
 
 namespace Aesop
 
-structure NormSimpContext extends Simp.Context where
+structure NormSimpContext where
+  toContext : Simp.Context
   enabled : Bool
   useHyps : Bool
   configStx? : Option Term
@@ -83,10 +84,8 @@ protected def run (ruleSet : LocalRuleSet) (options : Aesop.Options')
     MetaM (α × State Q × Tree × Stats) := do
   let t ← mkInitialTree goal
   let normSimpContext := {
-    config := simpConfig
-    maxDischargeDepth := UInt32.ofNatTruncate simpConfig.maxDischargeDepth
-    simpTheorems := ruleSet.simpTheoremsArray.map (·.snd)
-    congrTheorems := ← getSimpCongrTheorems
+    toContext := ← Simp.mkContext simpConfig (simpTheorems := ruleSet.simpTheoremsArray.map (·.snd))
+      (congrTheorems := ← getSimpCongrTheorems)
     simprocs := ruleSet.simprocsArray.map (·.snd)
     configStx? := simpConfigStx?
     enabled := options.enableSimp
diff --git a/Aesop/Tree/TreeM.lean b/Aesop/Tree/TreeM.lean
index 693f8937..dbf476a2 100644
--- a/Aesop/Tree/TreeM.lean
+++ b/Aesop/Tree/TreeM.lean
@@ -92,7 +92,7 @@ def getRootGoal : TreeM GoalRef := do
   let cref ← getRootMVarCluster
   let grefs := (← cref.get).goals
   if h : grefs.size = 1 then
-    return grefs.get ⟨0, by simp [h]⟩
+    return grefs[0]
   else
     throwError "aesop: internal error: unexpected number of goals in root mvar cluster: {grefs.size}"
 
diff --git a/Aesop/Util/Basic.lean b/Aesop/Util/Basic.lean
index 233353ab..fac2c16f 100644
--- a/Aesop/Util/Basic.lean
+++ b/Aesop/Util/Basic.lean
@@ -78,11 +78,11 @@ open DiscrTree
 
 -- For `type = ∀ (x₁, ..., xₙ), T`, returns keys that match `T * ... *` (with
 -- `n` stars).
-def getConclusionDiscrTreeKeys (type : Expr) (config : WhnfCoreConfig) :
+def getConclusionDiscrTreeKeys (type : Expr) (config : ConfigWithKey) :
     MetaM (Array Key) :=
   withoutModifyingState do
     let (_, _, conclusion) ← forallMetaTelescope type
-    mkPath conclusion config
+    withConfigWithKey config <| mkPath conclusion
     -- We use a meta telescope because `DiscrTree.mkPath` ignores metas (they
     -- turn into `Key.star`) but not fvars.
 
@@ -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)
 
diff --git a/Aesop/Util/Tactic/Unfold.lean b/Aesop/Util/Tactic/Unfold.lean
index 0b1b15c1..2183355a 100644
--- a/Aesop/Util/Tactic/Unfold.lean
+++ b/Aesop/Util/Tactic/Unfold.lean
@@ -14,12 +14,7 @@ namespace Aesop
 -- Lean.Meta.unfoldLocalDecl.
 
 def mkUnfoldSimpContext : MetaM Simp.Context := do
-  return {
-    simpTheorems := #[]
-    congrTheorems := ← getSimpCongrTheorems
-    config := Simp.neutralConfig
-    dischargeDepth := 0
-  }
+  Simp.mkContext Simp.neutralConfig (simpTheorems := #[]) (congrTheorems := ← getSimpCongrTheorems)
 
 @[inline]
 def unfoldManyCore (ctx : Simp.Context) (unfold? : Name → Option (Option Name))
diff --git a/AesopTest/RulePattern.lean b/AesopTest/RulePattern.lean
index 96d22c86..2b401679 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 ≤ (m : Int)
-    guard_hyp fwd_2 : 0 ≤ (n : Int)
+    guard_hyp fwd_1 : 0 ≤ (n : Int)
+    guard_hyp fwd_2 : 0 ≤ (m : Int)
     falso
 
 @[aesop safe forward (pattern := min x y)]
diff --git a/AesopTest/SaturatePerformance.lean b/AesopTest/SaturatePerformance.lean
index 6c8011a9..b57ad042 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 ++ l2).length ≥ 0
-fwd_1 : l0.length ≥ 0
+fwd : (l0 ++ l1).length ≥ 0
+fwd_1 : (l0 ++ l1 ++ l2).length ≥ 0
 fwd_2 : l2.length ≥ 0
-fwd_3 : l1.length ≥ 0
-fwd_4 : (l0 ++ l1).length ≥ 0
+fwd_3 : l0.length ≥ 0
+fwd_4 : l1.length ≥ 0
 ⊢ (l0 ++ l1 ++ l2).length = l0.length + l1.length + l2.length
 -/
 #guard_msgs in
diff --git a/lean-toolchain b/lean-toolchain
index 3450f2d4..cf25a981 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.15.0-rc1
\ No newline at end of file
+leanprover/lean4:v4.15.0-rc1