diff --git a/Duper/Clause.lean b/Duper/Clause.lean
index 0c74449..a587c06 100644
--- a/Duper/Clause.lean
+++ b/Duper/Clause.lean
@@ -68,7 +68,7 @@ def map (f : Expr → Expr) (l : Lit) :=
   {l with ty := f l.ty, lhs := f l.lhs, rhs := f l.rhs}
 
 def instantiateLevelParamsArray (l : Lit) (paramNames : Array Name) (levels : Array Level) :=
-  {l with lvl := l.lvl.instantiateParams paramNames.data levels.data
+  {l with lvl := l.lvl.instantiateParams paramNames.toList levels.toList
           ty := l.ty.instantiateLevelParamsArray paramNames levels
           lhs := l.lhs.instantiateLevelParamsArray paramNames levels
           rhs := l.rhs.instantiateLevelParamsArray paramNames levels}
@@ -294,7 +294,7 @@ def litsToExpr : List Lit → Expr
 | l :: ls => mkApp2 (mkConst ``Or) l.toExpr (litsToExpr ls)
 
 def toExpr (c : Clause) : Expr :=
-  litsToExpr c.lits.data
+  litsToExpr c.lits.toList
 
 def foldM {β : Type v} {m : Type v → Type w} [Monad m]
     (f : β → Expr → ClausePos → m β) (init : β) (c : Clause) : m β := do
diff --git a/Duper/Expr.lean b/Duper/Expr.lean
index b28b670..4007576 100644
--- a/Duper/Expr.lean
+++ b/Duper/Expr.lean
@@ -180,11 +180,11 @@ private partial def replaceAtPosHelper [Monad m] [MonadLiftT MetaM m] (e : Expr)
 
 /-- Attempts to put replacement at pos in e. Returns some res if successful, and returns none otherwise -/
 partial def replaceAtPos? [Monad m] [MonadLiftT MetaM m] (e : Expr) (pos : ExprPos) (replacement : Expr) : m (Option Expr) :=
-  replaceAtPosHelper e pos.data replacement
+  replaceAtPosHelper e pos.toList replacement
 
 /-- Attempts to put replacement at pos in e. Returns the result if successful and throws and error otherwise -/
 partial def replaceAtPos! [Monad m] [MonadLiftT MetaM m] [MonadError m] (e : Expr) (pos : ExprPos) (replacement : Expr) : m Expr := do
-  match ← replaceAtPosHelper e pos.data replacement with
+  match ← replaceAtPosHelper e pos.toList replacement with
   | some res => return res
   | none => throwError "replaceAtPos error: Invalid position {pos} given for expression {e}"
 
@@ -270,7 +270,7 @@ private partial def abstractAtPosHelper! [Monad m] [MonadLiftT MetaM m] [MonadEr
     the given expression to consist only of applications up to the given ExprPos. Additionally, since the exact
     ExprPos is given, we don't need to pass in Meta.kabstract's second argument p -/
 partial def abstractAtPos! [Monad m] [MonadLiftT MetaM m] [MonadError m] (e : Expr) (pos : ExprPos) : m Expr := do
-  abstractAtPosHelper! e pos.data 0
+  abstractAtPosHelper! e pos.toList 0
 
 private partial def abstractAtPosesHelper! [Monad m] [MonadLiftT MetaM m] [MonadError m] (e : Expr)
   (poses : Array (List Nat)) (numBindersUnder : Nat) : m Expr := do
@@ -322,7 +322,7 @@ private partial def abstractAtPosesHelper! [Monad m] [MonadLiftT MetaM m] [Monad
     return e
 
 partial def abstractAtPoses! [Monad m] [MonadLiftT MetaM m] [MonadError m] (e : Expr) (poses : Array ExprPos) : m Expr :=
-  abstractAtPosesHelper! e (poses.map (fun x => x.data)) 0
+  abstractAtPosesHelper! e (poses.map (fun x => x.toList)) 0
 
 /-
   Note: this function may require revision to be more similar to Zipperposition's ho_weight function once we actually
diff --git a/Duper/Interface.lean b/Duper/Interface.lean
index 51f7f52..a7555ff 100644
--- a/Duper/Interface.lean
+++ b/Duper/Interface.lean
@@ -374,7 +374,7 @@ def unfoldDefinitions (formulas : List (Expr × Expr × Array Name × Bool)) : M
 
 def printSaturation (state : ProverM.State) : MetaM Unit := do
   trace[duper.prover.saturate] "Final Active Set: {state.activeSet.toArray}"
-  trace[duper.saturate.debug] "Final active set numbers: {state.activeSet.toArray.map (fun c => (state.allClauses.find! c).number)}"
+  trace[duper.saturate.debug] "Final active set numbers: {state.activeSet.toArray.map (fun c => (state.allClauses.get! c).number)}"
   trace[duper.saturate.debug] "Final Active Set: {state.activeSet.toArray}"
   trace[duper.saturate.debug] "Verified Inhabited Types: {state.verifiedInhabitedTypes.map (fun x => x.expr)}"
   trace[duper.saturate.debug] "Verified Nonempty Types: {state.verifiedNonemptyTypes.map (fun x => x.1.expr)}"
@@ -382,7 +382,7 @@ def printSaturation (state : ProverM.State) : MetaM Unit := do
   trace[duper.saturate.debug] "Potentially Vacuous Clauses: {state.potentiallyVacuousClauses.toArray}"
 
 def formulasToMessageData : Expr × Expr × Array Name × Bool → MessageData
-| (ty, term, names, isFromGoal) => .compose (.compose m!"{names} @ " m!"{term} : ") m!"{ty}"
+| (ty, term, names, _isFromGoal) => .compose (.compose m!"{names} @ " m!"{term} : ") m!"{ty}"
 
 /-- Entry point for calling a single instance of duper using the options determined by (← getOptions).
 
@@ -455,7 +455,7 @@ def runDuperInstanceWithMonomorphization (formulas : List (Expr × Expr × Array
   let lemmas ← lemmas.mapM (m:=MetaM) (Auto.unfoldConstAndPreprocessLemma #[])
   let inhFacts ← Auto.Inhabitation.getInhFactsFromLCtx
   let prover : Array Auto.Lemma → Array Auto.Lemma → MetaM Expr :=
-    fun lemmas inhLemmas => do
+    fun lemmas _inhLemmas => do
       let monomorphizedFormulas ← autoLemmasToFormulas lemmas
       trace[duper.monomorphization.debug] "Original formulas: {formulas.map (fun f => (f.1, f.2.2.2))}"
       trace[duper.monomorphization.debug] "Auto lemmas: {lemmas.map (fun l => (l.type, l.proof, l.deriv))}"
@@ -472,7 +472,7 @@ def runDuperInstanceWithFullPreprocessing (formulas : List (Expr × Expr × Arra
   let lemmas ← lemmas.mapM (m:=MetaM) (Auto.unfoldConstAndPreprocessLemma #[])
   let inhFacts ← Auto.Inhabitation.getInhFactsFromLCtx
   let prover : Array Auto.Lemma → Array Auto.Lemma → MetaM Expr :=
-    fun lemmas inhLemmas => do
+    fun lemmas _inhLemmas => do
       let monomorphizedFormulas ← autoLemmasToFormulas lemmas
       trace[duper.monomorphization.debug] "Original formulas: {formulas.map (fun f => (f.1, f.2.2.2))}"
       trace[duper.monomorphization.debug] "Auto lemmas: {lemmas.map (fun l => (l.type, l.proof, l.deriv))}"
diff --git a/Duper/MClause.lean b/Duper/MClause.lean
index 1b6f568..bc93bd7 100644
--- a/Duper/MClause.lean
+++ b/Duper/MClause.lean
@@ -10,7 +10,7 @@ deriving Inhabited, BEq, Hashable
 namespace MClause
 
 def toExpr (c : MClause) : Expr :=
-  litsToExpr c.lits.data
+  litsToExpr c.lits.toList
 where litsToExpr : List Lit → Expr
 | [] => mkConst ``False
 | [l] => l.toExpr
diff --git a/Duper/Order.lean b/Duper/Order.lean
index 7aded06..cff44a5 100644
--- a/Duper/Order.lean
+++ b/Duper/Order.lean
@@ -29,7 +29,7 @@ def Symbol.toString : Symbol → String
 instance : ToMessageData Symbol := ⟨Symbol.format⟩
 instance : ToString Symbol := ⟨Symbol.toString⟩
 
-abbrev SymbolPrecMap := HashMap Symbol Nat -- Maps symbols to their precedence. Lower numbers indicate higher precedence
+abbrev SymbolPrecMap := Std.HashMap Symbol Nat -- Maps symbols to their precedence. Lower numbers indicate higher precedence
 
 namespace Comparison
 
@@ -67,13 +67,13 @@ def absWeight (w : Weight) : Weight := (Int.natAbs w.1, Int.natAbs w.2)
 
 local notation "ω" => ((1,0) : Weight)
 
-def VarBalance := HashMap (Expr × Bool) Weight
+def VarBalance := Std.HashMap (Expr × Bool) Weight
 
 def VarBalance.addPosVar (vb : VarBalance) (t : Expr × Bool) : VarBalance :=
-  vb.insert t $ vb.findD t 0 + 1
+  vb.insert t $ vb.getD t 0 + 1
 
 def VarBalance.addNegVar (vb : VarBalance) (t : Expr × Bool) : VarBalance :=
-  vb.insert t $ vb.findD t 0 - 1
+  vb.insert t $ vb.getD t 0 - 1
 
 -- The orderings treat lambda-expressions like a "LAM" symbol applied to the
 -- type and body of the lambda-expression
@@ -112,14 +112,14 @@ def headWeight (f : Expr) (symbolPrecMap : SymbolPrecMap) (highesetPrecSymbolHas
       if belowLam then 1 else ω
     else
       let fSymbol := Symbol.Const name
-      match symbolPrecMap.find? fSymbol with
+      match symbolPrecMap.get? fSymbol with
       | some 0 => -- The symbol with the highest precedence in symbolPrecMap is mapped to 0 (unless it has arity zero)
         if highesetPrecSymbolHasArityZero then 1
         else 0
       | _ => 1
   | Expr.fvar fVarId =>
     let fSymbol := Symbol.FVarId fVarId
-    match symbolPrecMap.find? fSymbol with
+    match symbolPrecMap.get? fSymbol with
     | some 0 => -- The symbol with the highest precedence in symbolPrecMap is mapped to 0 (unless it has arity zero)
       if highesetPrecSymbolHasArityZero then 1
       else 0
@@ -180,7 +180,7 @@ def symbolPrecCompare (e1 : Expr) (e2 : Expr) (s1 : Symbol) (s2 : Symbol) (symbo
     so that the firstmaximal0 weight generation scheme can determine if a symbol is maximal simply by checking whether it maps
     to 0 in symbolPrecMap
   -/
-  match symbolPrecMap.find? s1, symbolPrecMap.find? s2 with
+  match symbolPrecMap.get? s1, symbolPrecMap.get? s2 with
   | some n1, some n2 =>
     if n1 > n2 then return LessThan -- n1 is larger than n2 so s1 has a lower precedence
     else if n1 < n2 then return GreaterThan -- n1 is smaller than n2 so s1 has a higher precedence
@@ -407,13 +407,13 @@ mutual
   partial def kbo (t1 t2 : Expr) (alreadyReduced : Bool) (symbolPrecMap : SymbolPrecMap)
     (highesetPrecSymbolHasArityZero : Bool) : MetaM Comparison := do
     if alreadyReduced then
-      let (_, _, res) ← tckbo 0 HashMap.empty t1 t2 (belowLam := false) symbolPrecMap highesetPrecSymbolHasArityZero
+      let (_, _, res) ← tckbo 0 Std.HashMap.empty t1 t2 (belowLam := false) symbolPrecMap highesetPrecSymbolHasArityZero
       trace[duper.unaryFirst.debug] "Result of comparing {t1} with {t2} (alreadyReduced: {alreadyReduced}) is {res}"
       return res
     else
       let t1 ← betaEtaReduceInstMVars t1
       let t2 ← betaEtaReduceInstMVars t2
-      let (_, _, res) ← tckbo 0 HashMap.empty t1 t2 (belowLam := false) symbolPrecMap highesetPrecSymbolHasArityZero
+      let (_, _, res) ← tckbo 0 Std.HashMap.empty t1 t2 (belowLam := false) symbolPrecMap highesetPrecSymbolHasArityZero
       trace[duper.unaryFirst.debug] "Result of comparing {t1} with {t2} (alreadyReduced: {alreadyReduced}) is {res}"
       return res
 
@@ -555,12 +555,12 @@ end
     the two expressions' weights. -/
 def getNetWeight (t1 t2 : Expr) (alreadyReduced : Bool) (symbolPrecMap : SymbolPrecMap) (highesetPrecSymbolHasArityZero : Bool) : MetaM Weight := do
   if alreadyReduced then
-    let (netWeight, _, _) ← tckbo 0 HashMap.empty t1 t2 (belowLam := false) symbolPrecMap highesetPrecSymbolHasArityZero
+    let (netWeight, _, _) ← tckbo 0 Std.HashMap.empty t1 t2 (belowLam := false) symbolPrecMap highesetPrecSymbolHasArityZero
     return netWeight
   else
     let t1 ← betaEtaReduceInstMVars t1
     let t2 ← betaEtaReduceInstMVars t2
-    let (netWeight, _, _) ← tckbo 0 HashMap.empty t1 t2 (belowLam := false) symbolPrecMap highesetPrecSymbolHasArityZero
+    let (netWeight, _, _) ← tckbo 0 Std.HashMap.empty t1 t2 (belowLam := false) symbolPrecMap highesetPrecSymbolHasArityZero
     return netWeight
 
 end Order
diff --git a/Duper/Preprocessing.lean b/Duper/Preprocessing.lean
index 6fd5a8f..694a4db 100644
--- a/Duper/Preprocessing.lean
+++ b/Duper/Preprocessing.lean
@@ -55,12 +55,12 @@ partial def preprocessingClausification : ProverM Unit := do
     times, then updates f's result in symbolFreqMap to be n greater than it was originally). Note that as with Expr.weight,
     this function may require revision to be more similar to Zipperposition's implementation once we actually start working
     on higher order things. -/
-partial def updateSymbolFreqArityMap (f : Expr) (symbolFreqArityMap : HashMap Symbol (Nat × Nat)) :
-  ProverM (HashMap Symbol (Nat × Nat)) := do
+partial def updateSymbolFreqArityMap (f : Expr) (symbolFreqArityMap : Std.HashMap Symbol (Nat × Nat)) :
+  ProverM (Std.HashMap Symbol (Nat × Nat)) := do
   match f with
   | Expr.fvar fVarId =>
     let fSymbol := Symbol.FVarId fVarId
-    match symbolFreqArityMap.find? fSymbol with
+    match symbolFreqArityMap.get? fSymbol with
     | some (fFreq, fArity) => return symbolFreqArityMap.insert fSymbol (fFreq + 1, fArity)
     | none =>
       match (← getLCtx).fvarIdToDecl.find? fVarId with
@@ -70,7 +70,7 @@ partial def updateSymbolFreqArityMap (f : Expr) (symbolFreqArityMap : HashMap Sy
       | none => throwError s!"Unable to find {fVarId.name} in local context"
   | Expr.const name _ =>
     let fSymbol := Symbol.Const name
-    match symbolFreqArityMap.find? fSymbol with
+    match symbolFreqArityMap.get? fSymbol with
     | some (fFreq, fArity) => return symbolFreqArityMap.insert fSymbol (fFreq + 1, fArity)
     | none =>
       let fType ← inferType f
@@ -107,13 +107,13 @@ def isInductiveAndNonPropAndNotTypeClass (t : Expr) : ProverM Bool := do
     on higher order things. Additionally, updates datatypeList to make sure that all inductive datatypes that appear
     in the problem are contained in the datatypeList. The format in which inductive datatypes are recorded as elements of
     type `Expr × Array Name` is described in the comment above `buildSymbolFreqArityMapAndDatatypeList` -/
-partial def updateSymbolFreqArityMapAndDatatypeList (f : Expr) (symbolFreqArityMap : HashMap Symbol (Nat × Nat))
+partial def updateSymbolFreqArityMapAndDatatypeList (f : Expr) (symbolFreqArityMap : Std.HashMap Symbol (Nat × Nat))
   (datatypeList : List (Expr × Array Name)) (paramNames : Array Name) :
-  ProverM (HashMap Symbol (Nat × Nat) × List (Expr × Array Name)) := do
+  ProverM (Std.HashMap Symbol (Nat × Nat) × List (Expr × Array Name)) := do
   match f with
   | Expr.fvar fVarId =>
     let fSymbol := Symbol.FVarId fVarId
-    match symbolFreqArityMap.find? fSymbol with
+    match symbolFreqArityMap.get? fSymbol with
     | some (fFreq, fArity) => return (symbolFreqArityMap.insert fSymbol (fFreq + 1, fArity), datatypeList)
     | none =>
       match (← getLCtx).fvarIdToDecl.find? fVarId with
@@ -127,7 +127,7 @@ partial def updateSymbolFreqArityMapAndDatatypeList (f : Expr) (symbolFreqArityM
       | none => throwError s!"Unable to find {fVarId.name} in local context"
   | Expr.const name _ =>
     let fSymbol := Symbol.Const name
-    match symbolFreqArityMap.find? fSymbol with
+    match symbolFreqArityMap.get? fSymbol with
     | some (fFreq, fArity) => -- fSymbol has already been seen so datatypeList does not need to be updated
       return (symbolFreqArityMap.insert fSymbol (fFreq + 1, fArity), datatypeList)
     | none =>
@@ -216,8 +216,8 @@ partial def updateSymbolFreqArityMapAndDatatypeList (f : Expr) (symbolFreqArityM
 /-- Builds a HashMap that maps each symbol to a tuple containing:
     - The number of times they appear in formulas
     - Its arity -/
-partial def buildSymbolFreqArityMap (clauses : List Clause) : ProverM (HashMap Symbol (Nat × Nat)) := do
-  let mut symbolFreqArityMap := HashMap.empty
+partial def buildSymbolFreqArityMap (clauses : List Clause) : ProverM (Std.HashMap Symbol (Nat × Nat)) := do
+  let mut symbolFreqArityMap := Std.HashMap.empty
   for c in clauses do
     for l in c.lits do
       symbolFreqArityMap ← updateSymbolFreqArityMap l.lhs symbolFreqArityMap
@@ -232,8 +232,8 @@ partial def buildSymbolFreqArityMap (clauses : List Clause) : ProverM (HashMap S
     - A list containing every inductive datatype that appears in any clause. Polymorphic inductive datatypes are represented as universally
     quantified types paired with an array of parameters that can appear in the inductive datatype. For example, the polymorphic list datatype
     `List α` of where `α : Type u` is represented via `((∀ (α : Type u), List α), #[u])` -/
-partial def buildSymbolFreqArityMapAndDatatypeList (clauses : List Clause) : ProverM (HashMap Symbol (Nat × Nat) × List (Expr × Array Name)) := do
-  let mut symbolFreqArityMap := HashMap.empty
+partial def buildSymbolFreqArityMapAndDatatypeList (clauses : List Clause) : ProverM (Std.HashMap Symbol (Nat × Nat) × List (Expr × Array Name)) := do
+  let mut symbolFreqArityMap := Std.HashMap.empty
   let mut datatypeList := []
   for c in clauses do
     trace[duper.collectDatatypes.debug] "Loaded clause c: {c.lits}"
@@ -289,7 +289,7 @@ def buildSymbolPrecMap (clauses : List Clause) : ProverM (SymbolPrecMap × Bool)
     -- We use unaryFirstGt as the lt argument for binInsert so that symbols with higher precedence come first in symbolPrecArray
     symbolPrecArr := symbolPrecArr.binInsert unaryFirstGt (s, sFreq, sArity)
   trace[duper.unaryFirst.debug] "symbolPrecArr: {symbolPrecArr}"
-  let mut symbolPrecMap := HashMap.empty
+  let mut symbolPrecMap := Std.HashMap.empty
   let mut counter := 0
   let mut highesetPrecSymbolHasArityZero := false
   for (s, _, sArity) in symbolPrecArr do
@@ -343,7 +343,7 @@ def buildSymbolPrecMapAndDatatypeList (clauses : List Clause) : ProverM (SymbolP
     -- We use unaryFirstGt as the lt argument for binInsert so that symbols with higher precedence come first in symbolPrecArray
     symbolPrecArr := symbolPrecArr.binInsert unaryFirstGt (s, sFreq, sArity)
   trace[duper.unaryFirst.debug] "symbolPrecArr: {symbolPrecArr}"
-  let mut symbolPrecMap := HashMap.empty
+  let mut symbolPrecMap := Std.HashMap.empty
   let mut counter := 0
   let mut highesetPrecSymbolHasArityZero := false
   for (s, _, sArity) in symbolPrecArr do
diff --git a/Duper/ProofReconstruction.lean b/Duper/ProofReconstruction.lean
index 5a9ee0f..8ab4b17 100644
--- a/Duper/ProofReconstruction.lean
+++ b/Duper/ProofReconstruction.lean
@@ -11,7 +11,7 @@ initialize
   registerTraceClass `duper.proofReconstruction
 
 def getClauseInfo! (state : ProverM.State) (c : Clause) : CoreM ClauseInfo := do
-  let some ci := state.allClauses.find? c
+  let some ci := state.allClauses.get? c
     | throwError "clause info not found: {c}"
   return ci
 
@@ -49,25 +49,25 @@ partial def collectClauses (state : ProverM.State) (c : Clause) (acc : (Array Na
   return acc
 
 -- Map from clause `id` to Array of request of levels
-abbrev LevelRequests := HashMap Nat (HashMap (Array Level) Nat)
+abbrev LevelRequests := Std.HashMap Nat (Std.HashMap (Array Level) Nat)
 
 partial def collectLevelRequests (state : ProverM.State) (c : Clause)
   (lvls : Array Level) (acc : LevelRequests) : MetaM LevelRequests := do
   Core.checkMaxHeartbeats "collectLevelRequests"
   let info ← getClauseInfo! state c
-  if let some set := acc.find? info.number then
+  if let some set := acc.get? info.number then
     if set.contains lvls then
       return acc
   let mut acc := acc
   let lvlset :=
-    match acc.find? info.number with
+    match acc.get? info.number with
     | some set => set
-    | none     => HashMap.empty
+    | none     => Std.HashMap.empty
   trace[duper.proofReconstruction] "Request {c.paramNames} ↦ {lvls} for {c}"
   acc := acc.insert info.number (lvlset.insert lvls lvlset.size)
   for proofParent in info.proof.parents do
     let lvls' := proofParent.paramSubst.map
-      (fun lvl => lvl.instantiateParams c.paramNames.data lvls.data)
+      (fun lvl => lvl.instantiateParams c.paramNames.toList lvls.toList)
     acc ← collectLevelRequests state proofParent.clause lvls' acc
   return acc
 
@@ -79,9 +79,9 @@ structure PRState where
   -- `Nat` is the `id` of the clause
   -- `Array Level` is the requested levels for the clause
   -- `Expr` is the fvarId corresponding to the proof for the clause in the current `lctx`
-  constructedClauses : HashMap (Nat × Array Level) Expr
+  constructedClauses : Std.HashMap (Nat × Array Level) Expr
   -- Map from `id` of skolem constant to the constructed `fvar`
-  constructedSkolems : HashMap Nat FVarId
+  constructedSkolems : Std.HashMap Nat FVarId
   lctx : LocalContext
   mctx : MetavarContext
   localInstances : LocalInstances
@@ -128,10 +128,10 @@ partial def PRM.matchSkolem : Expr → PRM TransformStep
     let skTy := args[2]!
     let skmap := (← read).pmstate.skolemMap
     let consk := (← get).constructedSkolems
-    if let some isk := skmap.find? skid then
+    if let some isk := skmap.get? skid then
       let trailingArgs := args.extract 3 args.size
       let trailingArgs ← trailingArgs.mapM (fun e => Core.transform e PRM.matchSkolem)
-      if let some fvarId := consk.find? skid then
+      if let some fvarId := consk.get? skid then
         return .done (mkAppN (mkFVar fvarId) trailingArgs)
       let ⟨skProof, params⟩ := isk
       let skProof := skProof.instantiateLevelParamsArray params lvls
@@ -161,15 +161,15 @@ partial def mkClauseProof : List Clause → PRM Expr
   let reqs := (← read).reqs
   Core.checkMaxHeartbeats "mkClauseProof"
   let info ← getClauseInfo! state c
-  let lvlreqs := reqs.find! info.number
+  let lvlreqs := reqs.get! info.number
   for (req, reqid) in lvlreqs.toList do
     let mut parents : Array Expr := #[]
     let mut instantiatedProofParents := #[]
     for parent in info.proof.parents do
       let parentInfo ← getClauseInfo! state parent.clause
       let parentNumber := parentInfo.number
-      let instantiatedParentParamSubst := parent.paramSubst.map (fun lvl => lvl.instantiateParams c.paramNames.data req.data)
-      let parentPrfFvar := (← get).constructedClauses.find! (parentNumber, instantiatedParentParamSubst)
+      let instantiatedParentParamSubst := parent.paramSubst.map (fun lvl => lvl.instantiateParams c.paramNames.toList req.toList)
+      let parentPrfFvar := (← get).constructedClauses.get! (parentNumber, instantiatedParentParamSubst)
       parents := parents.push parentPrfFvar
       runMetaAsPRM <| do
         trace[duper.proofReconstruction] (
@@ -197,7 +197,7 @@ partial def mkClauseProof : List Clause → PRM Expr
     let instTr ← instTr.mapM (fun e => Core.transform e PRM.matchSkolem)
     let newProof ← (do
       let prf ← runMetaAsPRM <|
-        info.proof.mkProof parents.data instantiatedProofParents.data instTr instC
+        info.proof.mkProof parents.toList instantiatedProofParents.toList instTr instC
       if info.proof.ruleName != "assumption" then
         return prf
       else
@@ -224,10 +224,10 @@ partial def mkAllProof (state : ProverM.State) (cs : List Clause) : MetaM Expr :
   let emptyClause := cs[cslen - 1]!
   -- Other clauses
   let zeroLvlsForEmptyClause := emptyClause.paramNames.map (fun _ => Level.zero)
-  let reqs ← collectLevelRequests state emptyClause zeroLvlsForEmptyClause HashMap.empty
-  let (e, prstate) ← (do mkClauseProof cs.data).run
+  let reqs ← collectLevelRequests state emptyClause zeroLvlsForEmptyClause Std.HashMap.empty
+  let (e, prstate) ← (do mkClauseProof cs.toList).run
       {pmstate := state, reqs := reqs}
-      {constructedClauses := HashMap.empty, constructedSkolems := HashMap.empty,
+      {constructedClauses := Std.HashMap.empty, constructedSkolems := Std.HashMap.empty,
        lctx := ← getLCtx, mctx := ← getMCtx, localInstances := ← getLocalInstances, fvars := #[]}
   setMCtx prstate.mctx
   let lctx := prstate.lctx
diff --git a/Duper/ProverM.lean b/Duper/ProverM.lean
index c7a3615..9f98598 100644
--- a/Duper/ProverM.lean
+++ b/Duper/ProverM.lean
@@ -41,7 +41,7 @@ structure ClauseInfo where
 (isOrphan : Bool)
 deriving Inhabited
 
-abbrev ClauseSet := HashSet Clause
+abbrev ClauseSet := Std.HashSet Clause
 abbrev FairAgeClauseHeap := StrategyHeap Clause (β:=Nat)
 abbrev abstractedMVarList := List Meta.AbstractMVarsResult
 abbrev abstractedMVarAndClauseList := List (Meta.AbstractMVarsResult × Clause)
@@ -58,11 +58,11 @@ deriving Inhabited
 structure State where
   instanceMaxHeartbeats : Nat := 0 -- Heartbeats allocated to current instance of duper (0 treated as unlimited)
   result : Result := unknown
-  allClauses : HashMap Clause ClauseInfo := {}
+  allClauses : Std.HashMap Clause ClauseInfo := {}
   activeSet : ClauseSet := {}
   passiveSet : FairAgeClauseHeap := FairAgeHeap.empty Clause 5
   qStreamSet : ClauseStreamHeap ClauseStream := ClauseStreamHeap.empty ClauseStream
-  symbolPrecMap : SymbolPrecMap := HashMap.empty
+  symbolPrecMap : SymbolPrecMap := Std.HashMap.empty
   highesetPrecSymbolHasArityZero : Bool := false
   supMainPremiseIdx : RootCFPTrie := {}
   fluidSupMainPremiseIdx : RootCFPTrie := {} -- Stores fluid subterms and variables that appear in green positions and are also deeply occurring
@@ -70,7 +70,7 @@ structure State where
   demodMainPremiseIdx : RootCFPTrie := {}
   demodSidePremiseIdx : RootCFPTrie := {}
   subsumptionTrie : SubsumptionTrie := SubsumptionTrie.emptyNode
-  skolemMap : HashMap Nat SkolemInfo := HashMap.empty
+  skolemMap : Std.HashMap Nat SkolemInfo := Std.HashMap.empty
   skolemSorryName : Name := Name.anonymous
   verifiedInhabitedTypes : abstractedMVarList := [] -- List of (abstracted) types that we have determined are inhabited by typeclass inference
   verifiedNonemptyTypes : abstractedMVarAndClauseList := [] -- List of (abstracted) types that duper has derived are nonempty (along with the clause asserting that fact)
@@ -111,7 +111,7 @@ def getInstanceMaxHeartbeats : ProverM Nat :=
 def getResult : ProverM Result :=
   return (← get).result
 
-def getAllClauses : ProverM (HashMap Clause ClauseInfo) :=
+def getAllClauses : ProverM (Std.HashMap Clause ClauseInfo) :=
   return (← get).allClauses
 
 def getActiveSet : ProverM ClauseSet :=
@@ -145,7 +145,7 @@ def getSubsumptionTrie : ProverM SubsumptionTrie :=
   return (← get).subsumptionTrie
 
 def getClauseInfo! (c : Clause) : ProverM ClauseInfo := do
-  let some ci := (← getAllClauses).find? c
+  let some ci := (← getAllClauses).get? c
     | throwError "Clause not found: {c}"
   return ci
 
@@ -155,7 +155,7 @@ def getQStreamSet : ProverM (ClauseStreamHeap ClauseStream) :=
 def getSkolemSorryName : ProverM Name :=
   return (← get).skolemSorryName
 
-def getSkolemMap : ProverM (HashMap Nat SkolemInfo) :=
+def getSkolemMap : ProverM (Std.HashMap Nat SkolemInfo) :=
   return (← get).skolemMap
 
 def getVerifiedInhabitedTypes : ProverM abstractedMVarList :=
@@ -182,7 +182,7 @@ def setResult (result : Result) : ProverM Unit :=
 def setActiveSet (activeSet : ClauseSet) : ProverM Unit :=
   modify fun s => { s with activeSet := activeSet }
 
-def setAllClauses (allClauses : HashMap Clause ClauseInfo) : ProverM Unit :=
+def setAllClauses (allClauses : Std.HashMap Clause ClauseInfo) : ProverM Unit :=
   modify fun s => { s with allClauses := allClauses }
 
 def setPassiveSet (passiveSet : FairAgeClauseHeap) : ProverM Unit :=
@@ -215,7 +215,7 @@ def setSubsumptionTrie (subsumptionTrie : SubsumptionTrie) : ProverM Unit :=
 def setQStreamSet (Q : ClauseStreamHeap ClauseStream) : ProverM Unit :=
   modify fun s => { s with qStreamSet := Q }
 
-def setSkolemMap (skmap : HashMap Nat SkolemInfo) : ProverM Unit :=
+def setSkolemMap (skmap : Std.HashMap Nat SkolemInfo) : ProverM Unit :=
   modify fun s => {s with skolemMap := skmap}
 
 def setVerifiedInhabitedTypes (verifiedInhabitedTypes : abstractedMVarList) : ProverM Unit :=
@@ -256,7 +256,7 @@ partial def chooseGivenClause : ProverM (Option Clause) := do
 def markAsDescendantToGeneratingAncestors (c : Clause) (generatingAncestors : Array Clause) : ProverM Unit := do
   let mut allClauses ← getAllClauses
   for ancestor in generatingAncestors do
-    match allClauses.find? ancestor with
+    match allClauses.get? ancestor with
     | some ancestorInfo =>
       let descendantList := ancestorInfo.descendants
       let ancestorInfo := {ancestorInfo with descendants := c :: descendantList}
@@ -271,7 +271,7 @@ def addNewClause (c : Clause) (proof : Proof) (goalDistance : Nat) (generationNu
   trace[duper.clauseSelection.debug] "addNewClause: c: {c}, c.weight: {c.weight}, goalDistance: {goalDistance}, c.selectionPrecedence: {c.selectionPrecedence goalDistance}"
   let allClauses ← getAllClauses
   let ci ← (do
-    match allClauses.find? c with
+    match allClauses.get? c with
     | some ci =>
       if ci.isOrphan then
         -- Update c's generating ancestors and orphan status because it has been added to the passiveSet by new ancestors
@@ -302,11 +302,11 @@ def addNewClause (c : Clause) (proof : Proof) (goalDistance : Nat) (generationNu
           throwEmptyClauseException
         return ci)
   trace[duper.prover.saturate] (
-    let parentInfos := proof.parents.map (fun p => allClauses.find! p.clause)
+    let parentInfos := proof.parents.map (fun p => allClauses.get! p.clause)
     m!"New clause #{ci.number} by {proof.ruleName} on {parentInfos.map (fun i => i.number)}: {c}"
   )
   trace[duper.createdClauses] (
-    let parentInfos := proof.parents.map (fun p => allClauses.find! p.clause)
+    let parentInfos := proof.parents.map (fun p => allClauses.get! p.clause)
     m!"New clause #{ci.number} by {proof.ruleName} on {parentInfos.map (fun i => i.number)}: {c}"
   )
   return ci
@@ -315,7 +315,7 @@ def addNewClause (c : Clause) (proof : Proof) (goalDistance : Nat) (generationNu
     selection strategy's heuristics. The `generatingAncestors` argument contains the list of clauses that were used to generate `c` (or `c`'s
     ancestor which generated `c` by a modifying inference). See page 8 of "E – A Brainiac Theorem Prover" -/
 def addNewToPassive (c : Clause) (proof : Proof) (goalDistance : Nat) (generationNumber : Nat) (generatingAncestors : Array Clause) : ProverM Unit := do
-  match (← getAllClauses).find? c with
+  match (← getAllClauses).get? c with
   | some ci =>
     if (ci.wasSimplified) then pure () -- No need to add c to the passive set because it would just be simplified away later
     else if(ci.isOrphan) then -- We've seen c before, but we should readd it because it was only removed as an orphan (and wasn't simplified away)
@@ -332,7 +332,7 @@ def addNewToPassive (c : Clause) (proof : Proof) (goalDistance : Nat) (generatio
 
 /-- Takes a clause that was generated by preprocessing clausification and re-adds it to the passive set and its associated heaps -/
 def addClausifiedToPassive (c : Clause) : ProverM Unit := do
-  match (← getAllClauses).find? c with
+  match (← getAllClauses).get? c with
   | some ci =>
     setPassiveSet $ (← getPassiveSet).insert c (c.selectionPrecedence ci.goalDistance) ci.generationNumber ci.number
   | none => throwError "Unable to find information for clausified clause {c}"
@@ -496,7 +496,7 @@ partial def removeDescendants (c : Clause) (ci : ClauseInfo) (protectedClauses :
   for d in ci.descendants do
     if protectedClauses.contains d then continue
     trace[duper.simplification.debug] "Marking {d} as orphan because it is a descendant of {c} and does not appear in {protectedClauses}"
-    match allClauses.find? d with
+    match allClauses.get? d with
     | some dInfo =>
       -- Tag d as an orphan in allClauses
       let dInfo := {dInfo with generatingAncestors := #[], isOrphan := true}
@@ -524,13 +524,12 @@ partial def removeClause (c : Clause) (protectedClauses := ([] : List Clause)) :
   let mut passiveSet ← getPassiveSet
   let mut potentiallyVacuousClauses ← getPotentiallyVacuousClauses
   let mut allClauses ← getAllClauses
-  match allClauses.find? c with
+  match allClauses.get? c with
   | none => throwError "Attempted to remove {c} but was not able to find it in allClauses"
   | some ci =>
     -- Tag c as "wasSimplified" in allClauses
     let ci := {ci with wasSimplified := true}
     setAllClauses $ allClauses.insert c ci
-    allClauses ← getAllClauses
     -- Remove c from active set
     if activeSet.contains c then
       setActiveSet $ activeSet.erase c
diff --git a/Duper/RuleM.lean b/Duper/RuleM.lean
index 90be31e..bc7de4b 100644
--- a/Duper/RuleM.lean
+++ b/Duper/RuleM.lean
@@ -103,7 +103,7 @@ structure LoadedClause where
 structure State where
   loadedClauses : Array LoadedClause := #[]
   inhabitationClauses : Array LoadedClause := #[]
-  skolemMap : HashMap Nat SkolemInfo
+  skolemMap : Std.HashMap Nat SkolemInfo
 deriving Inhabited
 
 abbrev RuleM := ReaderT Context $ StateRefT State MetaM
@@ -147,7 +147,7 @@ def getLoadedClauses : RuleM (Array LoadedClause) :=
 def getInhabitationClauses : RuleM (Array LoadedClause) :=
   return (← get).inhabitationClauses
 
-def getSkolemMap : RuleM (HashMap Nat SkolemInfo) :=
+def getSkolemMap : RuleM (Std.HashMap Nat SkolemInfo) :=
   return (← get).skolemMap
 
 def setLoadedClauses (loadedClauses : Array LoadedClause) : RuleM Unit :=
@@ -159,7 +159,7 @@ def setInhabitationClauses (inhabitationClauses : Array LoadedClause) : RuleM Un
 def setState (s : State) : RuleM Unit :=
   modify fun _ => s
 
-def setSkolemMap (skmap : HashMap Nat SkolemInfo) : RuleM Unit :=
+def setSkolemMap (skmap : Std.HashMap Nat SkolemInfo) : RuleM Unit :=
   modify fun s => {s with skolemMap := skmap}
 
 def withoutModifyingMCtx (x : RuleM α) : RuleM α := do
@@ -305,7 +305,7 @@ def neutralizeMClause (c : MClause) (loadedClauses : Array LoadedClause) (transf
     let instantiatedparent := lst.lctx.mkForall lst.fvars finstantiatedparent
     -- Make sure that levels are abstracted
     let lmvars := lmvarIds.map Level.mvar
-    let lvarSubstWithExpr ← Duper.AbstractMVars.abstractExprMVars (Expr.const `_ <| lmvars.data)
+    let lvarSubstWithExpr ← Duper.AbstractMVars.abstractExprMVars (Expr.const `_ <| lmvars.toList)
     let paramSubst := Array.mk lvarSubstWithExpr.constLevels!
     proofParents := proofParents.push ⟨instantiatedparent, loadedClause, paramSubst⟩
   -- Deal with universe variables differently from metavariables :
@@ -343,7 +343,7 @@ def neutralizeMClauseInhabitedReasoningOn (c : MClause) (loadedClauses : Array L
     let finstantiatedparent ← Duper.AbstractMVars.abstractExprMVars minstantiatedparent
     -- Make sure that levels are abstracted
     let lmvars := lmvarIds.map Level.mvar
-    let lvarSubstWithExpr ← Duper.AbstractMVars.abstractExprMVars (Expr.const `_ <| lmvars.data)
+    let lvarSubstWithExpr ← Duper.AbstractMVars.abstractExprMVars (Expr.const `_ <| lmvars.toList)
     let paramSubst := Array.mk lvarSubstWithExpr.constLevels!
     proofParentsPre := proofParentsPre.push ⟨finstantiatedparent, loadedClause, paramSubst⟩
   -- Process inhabitationClauses
@@ -353,7 +353,7 @@ def neutralizeMClauseInhabitedReasoningOn (c : MClause) (loadedClauses : Array L
     let parentExpr ← Duper.AbstractMVars.abstractExprMVars inhabitationClause.toLambdaExpr
     -- Make sure that levels are abstracted
     let lmvars := lmvarIds.map Level.mvar
-    let lvarSubstWithExpr ← Duper.AbstractMVars.abstractExprMVars (Expr.const `_ <| lmvars.data)
+    let lvarSubstWithExpr ← Duper.AbstractMVars.abstractExprMVars (Expr.const `_ <| lmvars.toList)
     let paramSubst := Array.mk lvarSubstWithExpr.constLevels!
     proofParentsPre := proofParentsPre.push ⟨parentExpr, inhabitationClause, paramSubst⟩
   -- Process local context
diff --git a/Duper/Simp.lean b/Duper/Simp.lean
index 59c1c6c..18c6c4f 100644
--- a/Duper/Simp.lean
+++ b/Duper/Simp.lean
@@ -57,10 +57,10 @@ def MSimpRule.toSimpRule (rule : MSimpRule) : SimpRule := fun givenClause => do
   | some cs => do
     trace[duper.simplification.debug] "About to remove {givenClause} because it was simplified away to produce {cs.map (fun x => x.1)}"
     removeClause givenClause -- It is important that we remove givenClause and its descendants before readding the newly generated clauses
-    match cs.data with
+    match cs.toList with
     | List.nil => return Removed
     | (c, proof) :: restCs =>
-      match (← getAllClauses).find? givenClause with
+      match (← getAllClauses).get? givenClause with
       | some givenClauseInfo =>
         -- For forward simplification rules, each result clause has the same set of generating ancestors as givenClause
         let generatingAncestors := givenClauseInfo.generatingAncestors
@@ -91,7 +91,7 @@ def BackwardMSimpRule.toBackwardSimpRule (rule : BackwardMSimpRule) : BackwardSi
   for (c, _) in backwardSimpRes do
     trace[duper.simplification.debug] "About to remove {c} because it was simplified away"
     removeClause c [givenClause] -- givenClause must be protected when we remove c and its descendants because givenClause was used to eliminate c
-    match (← getAllClauses).find? c with
+    match (← getAllClauses).get? c with
     | some ci =>
       /- To match the strategy used for forward simplification, we use `ci.goalDistance` to ensure that the new clause is given the same goal distance as
          its main parent `c`. But if, in the future, we adopt Zipperposition's approach of giving the new clause the minimum goal distance of all its parents
diff --git a/Duper/SubsumptionTrie.lean b/Duper/SubsumptionTrie.lean
index f1c0d78..cfa326c 100644
--- a/Duper/SubsumptionTrie.lean
+++ b/Duper/SubsumptionTrie.lean
@@ -12,8 +12,8 @@ initialize Lean.registerTraceClass `duper.subsumptionTrie.debug
 
 inductive SubsumptionTrieFeatureValue where
   | N : Nat → SubsumptionTrieFeatureValue -- Feature is a number
-  | S : HashSet Expr → SubsumptionTrieFeatureValue -- Feature is a set
-  | M : HashMap Expr Nat → SubsumptionTrieFeatureValue -- Feature is a map
+  | S : Std.HashSet Expr → SubsumptionTrieFeatureValue -- Feature is a set
+  | M : Std.HashMap Expr Nat → SubsumptionTrieFeatureValue -- Feature is a map
 deriving Inhabited
 
 open SubsumptionTrieFeatureValue
@@ -30,7 +30,7 @@ def SubsumptionTrieFeatureValueLe (f1 : SubsumptionTrieFeatureValue) (f2 : Subsu
   | M m1, M m2 => -- Return true iff for every (e, n1) pair in m1 there is an (e, n2) pair in m2 with n1 ≤ n2
     Id.run $ do
     for (e, n1) in m1.toArray do
-      match m2.find? e with
+      match m2.get? e with
       | none => return false
       | some n2 =>
         if n1 ≤ n2 then continue
@@ -53,7 +53,7 @@ abbrev FeatureVector := List SubsumptionTrieFeatureValue
 -/
 inductive SubsumptionTrie where
   | node (children : Array (SubsumptionTrieFeatureValue × SubsumptionTrie)) : SubsumptionTrie
-  | leaf (vals : HashSet Clause) : SubsumptionTrie
+  | leaf (vals : Std.HashSet Clause) : SubsumptionTrie
 deriving Inhabited
 
 namespace SubsumptionTrie
@@ -79,7 +79,7 @@ instance : ToMessageData SubsumptionTrie := ⟨format⟩
 
 /-- Inserts every variable and constant that appears in e into acc. Note that as with Expr.weight, this function may require
     revision to be more similar to Zipperposition's implementation once we actually start working on higher order things -/
-partial def collectSymbolsInExpr (acc : HashSet Expr) (e : Expr) : HashSet Expr :=
+partial def collectSymbolsInExpr (acc : Std.HashSet Expr) (e : Expr) : Std.HashSet Expr :=
   match e.consumeMData with
   | fvar _ => acc.insert e.consumeMData
   | const _ _ => acc.insert e.consumeMData
@@ -91,22 +91,22 @@ partial def collectSymbolsInExpr (acc : HashSet Expr) (e : Expr) : HashSet Expr
   | _ => acc
 
 /-- Inserts every variable and constant that appears in l into acc. -/
-def collectSymbolsInLit (acc : HashSet Expr) (l : Lit) : HashSet Expr :=
+def collectSymbolsInLit (acc : Std.HashSet Expr) (l : Lit) : Std.HashSet Expr :=
   collectSymbolsInExpr (collectSymbolsInExpr acc l.lhs) l.rhs
 
 /-- Updates acc with maps each symbol to its maximal depth in a clause. Note that as with Expr.weight, this function may
     require revision to be more similar to Zipperposition's implementation once we actually start working on higher order things.
     See https://github.com/sneeuwballen/zipperposition/blob/master/src/core/FV_tree.ml#L182 -/
-partial def updateDepthMapWithExpr (acc : HashMap Expr Nat) (e : Expr) (curDepth := 0) : HashMap Expr Nat :=
+partial def updateDepthMapWithExpr (acc : Std.HashMap Expr Nat) (e : Expr) (curDepth := 0) : Std.HashMap Expr Nat :=
   match e.consumeMData with
   | fvar fVarId =>
-    match acc.find? (fvar fVarId) with
+    match acc.get? (fvar fVarId) with
     | none => acc.insert (fvar fVarId) curDepth
     | some maxDepth =>
       if curDepth > maxDepth then acc.insert (fvar fVarId) curDepth
       else acc
   | const declName us =>
-    match acc.find? (const declName us) with
+    match acc.get? (const declName us) with
     | none => acc.insert (const declName us) curDepth
     | some maxDepth =>
       if curDepth > maxDepth then acc.insert (const declName us) curDepth
@@ -123,19 +123,19 @@ partial def updateDepthMapWithExpr (acc : HashMap Expr Nat) (e : Expr) (curDepth
   | _ => acc
 
 /-- Updates acc which maps each symbol to its maximal depth in a clause. -/
-def updateDepthMapWithLit (acc : HashMap Expr Nat) (l : Lit) : HashMap Expr Nat :=
+def updateDepthMapWithLit (acc : Std.HashMap Expr Nat) (l : Lit) : Std.HashMap Expr Nat :=
   updateDepthMapWithExpr (updateDepthMapWithExpr acc l.lhs) l.rhs
 
 /-- Updates acc which maps each symbol to the number of times it occurs in a clause. Note that as with Expr.weight, this function may
     require revision to be more similar to Zipperposition's implementation once we actually start working on higher order things. -/
-partial def updateOccurrenceMapWithExpr (acc : HashMap Expr Nat) (e : Expr) : HashMap Expr Nat :=
+partial def updateOccurrenceMapWithExpr (acc : Std.HashMap Expr Nat) (e : Expr) : Std.HashMap Expr Nat :=
   match e.consumeMData with
   | fvar fVarId =>
-    match acc.find? (fvar fVarId) with
+    match acc.get? (fvar fVarId) with
     | none => acc.insert (fvar fVarId) 1
     | some numOccurrences => acc.insert (fvar fVarId) (numOccurrences + 1)
   | const declName us =>
-    match acc.find? (const declName us) with
+    match acc.get? (const declName us) with
     | none => acc.insert (const declName us) 1
     | some numOccurrences => acc.insert (const declName us) (numOccurrences + 1)
   | app e1 e2 => updateOccurrenceMapWithExpr (updateOccurrenceMapWithExpr acc e1) e2
@@ -146,7 +146,7 @@ partial def updateOccurrenceMapWithExpr (acc : HashMap Expr Nat) (e : Expr) : Ha
   | _ => acc
 
 /-- Updates acc which maps each symbol to the number of times it occurs in a clause. -/
-def updateOccurrenceMapWithLit (acc : HashMap Expr Nat) (l : Lit) : HashMap Expr Nat :=
+def updateOccurrenceMapWithLit (acc : Std.HashMap Expr Nat) (l : Lit) : Std.HashMap Expr Nat :=
   updateOccurrenceMapWithExpr (updateOccurrenceMapWithExpr acc l.lhs) l.rhs
 
 /-
@@ -228,7 +228,7 @@ def emptyNode : SubsumptionTrie := node #[]
 
 def singleton (c : Clause) (features : FeatureVector) : SubsumptionTrie :=
   match features with
-  | [] => leaf (HashSet.empty.insert c)
+  | [] => leaf (Std.HashSet.empty.insert c)
   | fstFeature :: restFeatures => node #[(fstFeature, singleton c restFeatures)]
 
 private def insertHelper (t : SubsumptionTrie) (c : Clause) (features : FeatureVector) : RuleM SubsumptionTrie :=
diff --git a/Duper/Util/MessageData.lean b/Duper/Util/MessageData.lean
index 1cf67c1..34e398f 100644
--- a/Duper/Util/MessageData.lean
+++ b/Duper/Util/MessageData.lean
@@ -15,4 +15,4 @@ def ListToMessageData (as : List α) (f : α → MessageData) : MessageData :=
     | .cons a as@(.cons _ _) => .compose (f a) (.compose ", " (go as))
 
 def ArrayToMessageData (as : Array α) (f : α → MessageData) : MessageData :=
-  ListToMessageData as.data f
\ No newline at end of file
+  ListToMessageData as.toList f
diff --git a/lake-manifest.json b/lake-manifest.json
index 585682b..11a2fd9 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,21 +5,21 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "0728f384d78982e6fb0f1cdf263e172d3135e0be",
+   "rev": "915802517242f70b284fbcd5eac55bdaae29535e",
    "name": "auto",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "0728f384d78982e6fb0f1cdf263e172d3135e0be",
+   "inputRev": "915802517242f70b284fbcd5eac55bdaae29535e",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "4756e0fc48acce0cc808df0ad149de5973240df6",
+   "rev": "31a10a332858d6981dbcf55d54ee51680dd75f18",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.12.0",
+   "inputRev": "v4.13.0",
    "inherited": false,
-   "configFile": "lakefile.lean"}],
+   "configFile": "lakefile.toml"}],
  "name": "Duper",
  "lakeDir": ".lake"}
diff --git a/lakefile.lean b/lakefile.lean
index 3cd8544..98d1a82 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -2,8 +2,8 @@ import Lake
 
 open Lake DSL
 
-require auto from git "https://github.com/leanprover-community/lean-auto.git"@"0728f384d78982e6fb0f1cdf263e172d3135e0be"
-require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.12.0"
+require auto from git "https://github.com/leanprover-community/lean-auto.git"@"915802517242f70b284fbcd5eac55bdaae29535e"
+require batteries from git "https://github.com/leanprover-community/batteries" @ "v4.13.0"
 
 package Duper {
   precompileModules := true
diff --git a/lean-toolchain b/lean-toolchain
index 8998520..4f86f95 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.12.0
+leanprover/lean4:v4.13.0