diff --git a/Auto/Embedding/LamBitVec.lean b/Auto/Embedding/LamBitVec.lean
index ac3e991..0b2e9d5 100644
--- a/Auto/Embedding/LamBitVec.lean
+++ b/Auto/Embedding/LamBitVec.lean
@@ -55,16 +55,18 @@ namespace BVLems
     unfold BitVec.ushiftRight BitVec.toNat
     dsimp; rw [Nat.shiftRight_eq_div_pow]
 
-  theorem toNat_zeroExtend' {a : BitVec n} (le : n ≤ m) : (a.zeroExtend' le).toNat = a.toNat := rfl
+  theorem toNat_setWidth {a : BitVec n} (le : n ≤ m) : (a.setWidth m).toNat = a.toNat := by
+    unfold setWidth
+    simp only [le, ↓reduceDIte, toNat_setWidth']
 
   theorem toNat_zeroExtend {a : BitVec n} (i : Nat) : (a.zeroExtend i).toNat = a.toNat % (2 ^ i) := by
-    unfold BitVec.zeroExtend; cases hdec : decide (n ≤ i)
+    unfold BitVec.zeroExtend setWidth; cases hdec : decide (n ≤ i)
     case false =>
       have hnle := of_decide_eq_false hdec
       rw [Bool.dite_eq_false (proof:=hnle)]; rfl
     case true =>
       have hle := of_decide_eq_true hdec
-      rw [Bool.dite_eq_true (proof:=hle), toNat_zeroExtend']
+      rw [Bool.dite_eq_true (proof:=hle), toNat_setWidth']
       rw [Nat.mod_eq_of_lt]; rcases a with ⟨⟨a, isLt⟩⟩;
       apply Nat.le_trans isLt; apply Nat.pow_le_pow_of_le_right (Nat.le_step .refl) hle
 
@@ -103,7 +105,7 @@ namespace BVLems
   theorem msb_equiv_lt (a : BitVec n) : !a.msb ↔ a.toNat < 2 ^ (n - 1) := by
     dsimp [BitVec.msb, getMsbD, getLsbD]
     cases n
-    case zero => simp
+    case zero => simp [BitVec.toNat]
     case succ n =>
       have dtrue : decide (0 < n + 1) = true := by simp
       rw [dtrue, Bool.not_eq_true', Bool.true_and, Nat.succ_sub_one, Nat.testBit_false_iff]
@@ -112,7 +114,7 @@ namespace BVLems
   theorem msb_equiv_lt' (a : BitVec n) : !a.msb ↔ 2 * a.toNat < 2 ^ n := by
     rw [msb_equiv_lt]
     cases n
-    case zero => simp
+    case zero => simp [BitVec.toNat]
     case succ n =>
       rw [Nat.succ_sub_one, Nat.pow_succ, Nat.mul_comm (m:=2)]
       apply Iff.symm; apply Nat.mul_lt_mul_left
diff --git a/Auto/Embedding/LamChecker.lean b/Auto/Embedding/LamChecker.lean
index 0fdbd66..bf12dce 100644
--- a/Auto/Embedding/LamChecker.lean
+++ b/Auto/Embedding/LamChecker.lean
@@ -2460,9 +2460,9 @@ theorem Checker.getValidExport_indirectReduce_reflection
 structure RTableStatus where
   rTable        : Array REntry := #[]
   rTableTree    : BinTree REntry := BinTree.leaf
-  nonemptyMap   : HashMap LamSort Nat := {}
-  wfMap         : HashMap (List LamSort × LamSort × LamTerm) Nat := {}
-  validMap      : HashMap (List LamSort × LamTerm) Nat := {}
+  nonemptyMap   : Std.HashMap LamSort Nat := {}
+  wfMap         : Std.HashMap (List LamSort × LamSort × LamTerm) Nat := {}
+  validMap      : Std.HashMap (List LamSort × LamTerm) Nat := {}
   -- maxEVarSucc
   maxEVarSucc   : Nat := 0
   -- lamEVarTy
@@ -2470,7 +2470,7 @@ structure RTableStatus where
   -- This works as a cache for `BinTree.ofListGet lamEVarTy.data`
   lamEVarTyTree : BinTree LamSort := BinTree.leaf
   -- `chkMap.find?[re]` returns the checkstep which proves `re`
-  chkMap        : HashMap REntry ChkStep := {}
+  chkMap        : Std.HashMap REntry ChkStep := {}
   deriving Inhabited
 
 def RTableStatus.push (rs : RTableStatus) (re : REntry) :=
@@ -2494,8 +2494,8 @@ def RTableStatus.newEtomWithValid (rs : RTableStatus) (c : ChkStep) (re : REntry
 
 def RTableStatus.findPos? (rs : RTableStatus) (re : REntry) :=
   match re with
-  | .nonempty s => rs.nonemptyMap.find? s
-  | .wf lctx s t => rs.wfMap.find? (lctx, s, t)
-  | .valid lctx t => rs.validMap.find? (lctx, t)
+  | .nonempty s => rs.nonemptyMap.get? s
+  | .wf lctx s t => rs.wfMap.get? (lctx, s, t)
+  | .valid lctx t => rs.validMap.get? (lctx, t)
 
 end Auto.Embedding.Lam
diff --git a/Auto/Embedding/LamConv.lean b/Auto/Embedding/LamConv.lean
index 2c78aa2..950a022 100644
--- a/Auto/Embedding/LamConv.lean
+++ b/Auto/Embedding/LamConv.lean
@@ -1957,8 +1957,8 @@ section UnsafeOps
   /-- Turn `ts[i]` into `.bvar i` -/
   def LamTerm.abstractsImp (t : LamTerm) (ts : Array LamTerm) :=
     let ts := ts.mapIdx (fun i x => (x, LamTerm.bvar i.val))
-    let tmap := @Lean.HashMap.ofList _ _ inferInstance inferInstance ts.data
-    t.replace (fun x => tmap.find? x) 0
+    let tmap := @Std.HashMap.ofList _ _ inferInstance inferInstance ts.toList
+    t.replace (fun x => tmap.get? x) 0
 
   def LamTerm.abstractsRevImp (t : LamTerm) (ts : Array LamTerm) := t.abstractsImp ts.reverse
 
diff --git a/Auto/IR/SMT.lean b/Auto/IR/SMT.lean
index 9f3742a..94d070e 100644
--- a/Auto/IR/SMT.lean
+++ b/Auto/IR/SMT.lean
@@ -33,7 +33,7 @@ deriving BEq, Hashable, Inhabited
 def SIdent.toString : SIdent → String
 | .symb s => if isSimpleSymbol s then s else "|" ++ s ++ "|"
 | .indexed s idx =>
-  s!"(_ {s} " ++ String.intercalate " " (idx.data.map (fun idx =>
+  s!"(_ {s} " ++ String.intercalate " " (idx.toList.map (fun idx =>
     match idx with
     | .inl idx => s!"{idx}"
     | .inr idx => s!"{idx}")) ++ ")"
@@ -63,7 +63,7 @@ where go : List SSort → List SIdent →  List String
 | a :: as, binders => SSort.toStringAux a binders :: go as binders
 
 def SSort.toString (s : SSort) (binders : Array SIdent) : String :=
-  SSort.toStringAux s binders.data
+  SSort.toStringAux s binders.toList
 
 /-- Caution : Do not use this in define-sort, because sort there might contain bvars -/
 instance : ToString SSort where
@@ -181,7 +181,7 @@ private partial def STerm.toStringAux : STerm → List SIdent → String
     intro ++ body
   | .attr t attrs, binders =>
     let intro := "(! " ++ STerm.toStringAux t binders ++ " "
-    let sattrs := String.intercalate " " (attrs.data.map (attrToStringAux · binders))
+    let sattrs := String.intercalate " " (attrs.toList.map (attrToStringAux · binders))
     intro ++ sattrs ++ ")"
 where
   goQIdApp : List STerm → List SIdent → List String
@@ -194,9 +194,9 @@ where
         let pattern := "(" ++ (ToString.toString (SIdent.symb constr))
         pattern ++ body
       else
-        let binders := args.data.map .symb ++ binders
+        let binders := args.toList.map .symb ++ binders
         let body := " " ++ STerm.toStringAux body binders ++ ")"
-        let args := args.data.map (fun x => ToString.toString (SIdent.symb x))
+        let args := args.toList.map (fun x => ToString.toString (SIdent.symb x))
         let pattern := "((" ++ String.intercalate " " (ToString.toString (SIdent.symb constr) :: args) ++ ")"
         pattern ++ body
   goMatchBody : List (MatchCase STerm) → List SIdent → List String
@@ -206,16 +206,16 @@ where
     | .none s,     _ => ":" ++ s
     | .spec s sc,  _ => s!":{s} {sc.toString}"
     | .symb s s',  _ => s!":{s} {s'}"
-    | .sexpr s ts, binders => s!":{s} (" ++ String.intercalate " " (ts.data.map (STerm.toStringAux · binders)) ++ ")"
+    | .sexpr s ts, binders => s!":{s} (" ++ String.intercalate " " (ts.toList.map (STerm.toStringAux · binders)) ++ ")"
 
 def STerm.toString (t : STerm) (binders : Array SIdent) : String :=
-  STerm.toStringAux t binders.data
+  STerm.toStringAux t binders.toList
 
 instance : ToString STerm where
   toString t := STerm.toString t #[]
 
 def Attribute.toString (attr : Attribute) (binders : Array SIdent) : String :=
-  SMT.STerm.toStringAux.attrToStringAux attr binders.data
+  SMT.STerm.toStringAux.attrToStringAux attr binders.toList
 
 instance : ToString Attribute where
   toString attr := Attribute.toString attr #[]
@@ -232,7 +232,7 @@ private def ConstrDecl.toString : ConstrDecl → Array SIdent → String
 | ⟨name, selDecls⟩, binders =>
   let pre := s!"({SIdent.symb name}"
   let selDecls := selDecls.map (fun (name, sort) => s!"({SIdent.symb name} " ++ SSort.toString sort binders ++ ")")
-  String.intercalate " " (pre :: selDecls.data) ++ ")"
+  String.intercalate " " (pre :: selDecls.toList) ++ ")"
 
 /--
  〈datatype_dec〉 ::= ( 〈constructor_dec〉+ ) | ( par ( 〈symbol 〉+ ) ( 〈constructor_dec〉+ ) )
@@ -243,11 +243,11 @@ structure DatatypeDecl where
 
 private def DatatypeDecl.toString : DatatypeDecl → String := fun ⟨params, cstrDecls⟩ =>
   let scstrDecls := cstrDecls.map (fun d => ConstrDecl.toString d (params.map SIdent.symb))
-  let scstrDecls := "(" ++ String.intercalate " " scstrDecls.data ++ ")"
+  let scstrDecls := "(" ++ String.intercalate " " scstrDecls.toList ++ ")"
   if params.size == 0 then
     scstrDecls
   else
-    "(par ("  ++ String.intercalate " " params.data ++ ") " ++ scstrDecls ++ ")"
+    "(par ("  ++ String.intercalate " " params.toList ++ ") " ++ scstrDecls ++ ")"
 
 inductive SMTOption where
   | diagnosticOC            : String → SMTOption
@@ -345,26 +345,26 @@ def Command.toString : Command → String
 | .checkSat                            => "(check-sat)"
 | .declFun name argSorts resSort       =>
   let pre := s!"(declare-fun {SIdent.symb name} ("
-  let argSorts := String.intercalate " " (argSorts.map ToString.toString).data ++ ") "
+  let argSorts := String.intercalate " " (argSorts.map ToString.toString).toList ++ ") "
   let trail := s!"{resSort})"
   pre ++ argSorts ++ trail
 | .declSort name arity                 => s!"(declare-sort {SIdent.symb name} {arity})"
 | .defFun isRec name args resTy body =>
   let pre := if isRec then "(define-fun-rec " else "(define-fun "
   let pre := pre ++ ToString.toString (SIdent.symb name) ++ " "
-  let binders := "(" ++ String.intercalate " " (args.map (fun (name, sort) => s!"({SIdent.symb name} {sort})")).data ++ ") "
+  let binders := "(" ++ String.intercalate " " (args.map (fun (name, sort) => s!"({SIdent.symb name} {sort})")).toList ++ ") "
   let trail := s!"{resTy} " ++ STerm.toString body (args.map (fun (name, _) => SIdent.symb name)) ++ ")"
   pre ++ binders ++ trail
 | .defSort name args body              =>
   let pre := s!"(define-sort {SIdent.symb name} ("
-  let sargs := String.intercalate " " args.data ++ ") "
+  let sargs := String.intercalate " " args.toList ++ ") "
   let trail := SSort.toString body (args.map SIdent.symb) ++ ")"
   pre ++ sargs ++ trail
 | .declDtype name ddecl                =>
   s!"(declare-datatype {SIdent.symb name} {ddecl.toString})"
 | .declDtypes infos               =>
-  let sort_decs := String.intercalate " " (infos.data.map (fun (name, args, _) => s!"({SIdent.symb name} {args})"))
-  let datatype_decs := String.intercalate " " (infos.data.map (fun (_, _, ddecl) => ddecl.toString))
+  let sort_decs := String.intercalate " " (infos.toList.map (fun (name, args, _) => s!"({SIdent.symb name} {args})"))
+  let datatype_decs := String.intercalate " " (infos.toList.map (fun (_, _, ddecl) => ddecl.toString))
   s!"(declare-datatypes ({sort_decs}) ({datatype_decs}))"
 | .echo s                              => s!"(echo \"{s}\")"
 | .exit                                => "(exit)"
@@ -385,10 +385,10 @@ section
   -/
   structure State where
     -- Map from high-level construct to symbol
-    h2lMap    : HashMap ω String   := {}
+    h2lMap    : Std.HashMap ω String   := {}
     -- Inverse of `h2lMap`
     -- Map from symbol to high-level construct
-    l2hMap    : HashMap String ω   := {}
+    l2hMap    : Std.HashMap String ω   := {}
     -- We allow two types of names
     -- · `"_" ++ s`,
     -- · `"_" ++ s ++ "_" ++ <num>`
@@ -402,7 +402,7 @@ section
     --   been used, we return `n'` as the final name. If `n'` has
     --   been used for `k` times (`k > 0`), return `n' ++ s!"_{k - 1}"`.
     -- `usedNames` records the `k - 1` for each `n'`
-    usedNames : HashMap String Nat := {}
+    usedNames : Std.HashMap String Nat := {}
     -- List of commands
     commands  : Array Command      := #[]
 
@@ -443,7 +443,7 @@ section
       preName := "pl_" ++ preName
     if preName.back.isDigit then
       preName := preName ++ "_"
-    if let .some idx := (← getUsedNames).find? preName then
+    if let .some idx := (← getUsedNames).get? preName then
       -- Used
       setUsedNames ((← getUsedNames).insert preName (idx + 1))
       return "_" ++ preName ++ s!"_{idx}"
@@ -457,7 +457,7 @@ section
         "~!@$%^&*_-+=<>.?/" ++
         "ΑαΒβΓγΔδΕεΖζΗηΘθΙιΚκΛλΜμΝνΞξΟοΠπΡρΣσςΤτΥυΦφΧχΨψΩω" ++
         "₀₁₂₃₄₅₆₇₈₉"
-      let allowedSet : HashSet UInt32 := HashSet.insertMany HashSet.empty (List.map Char.val allowedStr.toList)
+      let allowedSet : Std.HashSet UInt32 := Std.HashSet.insertMany Std.HashSet.empty (List.map Char.val allowedStr.toList)
       c.isAlphanum || allowedSet.contains c.val
 
 
@@ -471,7 +471,7 @@ section
   partial def h2Symb (cstr : ω) (nameSuggestion : Option String) : TransM ω String := do
     let l2hMap ← getL2hMap
     let h2lMap ← getH2lMap
-    if let .some name := h2lMap.find? cstr then
+    if let .some name := h2lMap.get? cstr then
       return name
     let .some nameSuggestion := nameSuggestion
       | throwError "IR.SMT.h2Symb :: Fresh high-level constraint {cstr} without name suggestion"
diff --git a/Auto/Lib/Containers.lean b/Auto/Lib/Containers.lean
index 2f22643..ee5d660 100644
--- a/Auto/Lib/Containers.lean
+++ b/Auto/Lib/Containers.lean
@@ -3,7 +3,7 @@ open Lean
 
 namespace Auto
 
-def mergeHashSet {α : Type u} [BEq α] [Hashable α] (a1 a2 : HashSet α) :=
+def mergeHashSet {α : Type u} [BEq α] [Hashable α] (a1 a2 : Std.HashSet α) :=
   if a1.size < a2.size then
     a2.insertMany a1.toArray
   else
@@ -22,4 +22,4 @@ class Container {α : Type u} (C : Type v → Type w) where
   insertCorrect₁ : ∀ (c : C β) (k : α) (v : β), get? (insert c k v) k = .some val
   insertCorrect₂ : ∀ (c : C β) (k₁ k₂ : α) (v : β), k₁ ≠ k₂ → get? (insert c k₁ v) k₂ = get? c k₂
 
-end Auto
\ No newline at end of file
+end Auto
diff --git a/Auto/Lib/DeCompile.lean b/Auto/Lib/DeCompile.lean
index b89acea..4d79c70 100644
--- a/Auto/Lib/DeCompile.lean
+++ b/Auto/Lib/DeCompile.lean
@@ -13,7 +13,7 @@ namespace ExprDeCompile
 --   as explicit
 
 structure Context where
-  usedNames : HashSet String
+  usedNames : Std.HashSet String
 
 structure State where
   binderNames : Array String := #[]
@@ -69,7 +69,7 @@ private partial def exprDeCompileAux (final : Bool) (e : Expr) : ExprDeCompM Str
       return ret
     let fs ← exprDeCompileAux final f
     let argss ← args.mapM (exprDeCompileAux final)
-    let argssC := String.intercalate " " argss.data
+    let argssC := String.intercalate " " argss.toList
     return s!"({fs} {argssC})"
   | Expr.proj _ idx b =>
     let bs ← exprDeCompileAux final b
@@ -94,7 +94,7 @@ private partial def exprDeCompileAux (final : Bool) (e : Expr) : ExprDeCompM Str
   | Expr.bvar n =>
     let bn := (← get).binderNames
     return bn[bn.size - n - 1]!
-where 
+where
   constFinalDeComp (name : Name) (us : List Level) :=
     if List.length us == 0 then
       "@" ++ name.toString
@@ -118,7 +118,7 @@ where
       e := .lam `_ (ty.instantiateLevelParams lparams cst.constLevels!) e .default
     return e
 
-def levelCollectNames (l : Level) : StateT (HashSet String) MetaM Unit := do
+def levelCollectNames (l : Level) : StateT (Std.HashSet String) MetaM Unit := do
   match l with
   | .zero => return
   | .succ l => levelCollectNames l
@@ -127,7 +127,7 @@ def levelCollectNames (l : Level) : StateT (HashSet String) MetaM Unit := do
   | .max l1 l2 => levelCollectNames l1; levelCollectNames l2
   | .imax l1 l2 => levelCollectNames l1; levelCollectNames l2
 
-def exprCollectNames (e : Expr) : StateT (HashSet String) MetaM Unit := do
+def exprCollectNames (e : Expr) : StateT (Std.HashSet String) MetaM Unit := do
   match e with
   | Expr.forallE _ d b _ => exprCollectNames d; exprCollectNames b
   | Expr.lam _ d b _ => exprCollectNames d; exprCollectNames b
@@ -143,7 +143,7 @@ def exprCollectNames (e : Expr) : StateT (HashSet String) MetaM Unit := do
   | Expr.lit _ => return
   | Expr.sort l => levelCollectNames l
   | Expr.mvar .. => return
-  | Expr.fvar f => 
+  | Expr.fvar f =>
     let some decl := (← getLCtx).find? f
       | throwError "Unknown free variable {e}"
     let name := decl.userName.toString
@@ -212,4 +212,4 @@ universe u
 
 --/
 
-end Auto
\ No newline at end of file
+end Auto
diff --git a/Auto/Lib/ExprExtra.lean b/Auto/Lib/ExprExtra.lean
index adf6730..a83f10b 100644
--- a/Auto/Lib/ExprExtra.lean
+++ b/Auto/Lib/ExprExtra.lean
@@ -46,7 +46,7 @@ def Expr.forallBinders (e : Expr) : Array (Name × Expr × BinderInfo) :=
     | _ => []
   Array.mk (aux e)
 
-def Expr.collectRawM [Monad m] (p : Expr → m Bool) : Expr → m (HashSet Expr)
+def Expr.collectRawM [Monad m] (p : Expr → m Bool) : Expr → m (Std.HashSet Expr)
 | e@(.forallE _ d b _) => do
   let hd ← collectRawM p d
   let hb ← collectRawM p b
@@ -70,7 +70,7 @@ def Expr.collectRawM [Monad m] (p : Expr → m Bool) : Expr → m (HashSet Expr)
 | e@(.proj _ _ b) => do
   let hb ← collectRawM p b
   addp? p e hb
-| e => addp? p e HashSet.empty
+| e => addp? p e Std.HashSet.empty
 where addp? p e hs := do
   if ← p e then
     return hs.insert e
diff --git a/Auto/Lib/LevelExtra.lean b/Auto/Lib/LevelExtra.lean
index 58a8d0d..3be8e09 100644
--- a/Auto/Lib/LevelExtra.lean
+++ b/Auto/Lib/LevelExtra.lean
@@ -17,13 +17,13 @@ def Level.collectLevelMVars (l : Level) : MetaM (Array LMVarId) := do
   let hset := go l
   return hset.toArray
 where
-  go : Level → HashSet LMVarId
+  go : Level → Std.HashSet LMVarId
   | .zero => {}
   | .succ l => go l
   | .max l₁ l₂ => mergeHashSet (go l₁) (go l₂)
   | .imax l₁ l₂ => mergeHashSet (go l₁) (go l₂)
   | .param _ => {}
-  | .mvar id => HashSet.empty.insert id
+  | .mvar id => Std.HashSet.empty.insert id
 
 def Level.findParam? (p : Name → Bool) : Level → Option Name
 | .zero => .none
@@ -36,4 +36,4 @@ def Level.findParam? (p : Name → Bool) : Level → Option Name
   | false => .none
 | .mvar _ => .none
 
-end Auto
\ No newline at end of file
+end Auto
diff --git a/Auto/Lib/MessageData.lean b/Auto/Lib/MessageData.lean
index a0d9324..f9b9fec 100644
--- a/Auto/Lib/MessageData.lean
+++ b/Auto/Lib/MessageData.lean
@@ -17,6 +17,6 @@ def MessageData.list (as : List α) (f : α → MessageData) : MessageData :=
   .compose m!"[" (.compose (MessageData.intercalate m!", " (as.map f)) m!"]")
 
 def MessageData.array (as : Array α) (f : α → MessageData) : MessageData :=
-  MessageData.list as.data f
+  MessageData.list as.toList f
 
-end Auto
\ No newline at end of file
+end Auto
diff --git a/Auto/Lib/MonadUtils.lean b/Auto/Lib/MonadUtils.lean
index 2f22fe2..ba33e99 100644
--- a/Auto/Lib/MonadUtils.lean
+++ b/Auto/Lib/MonadUtils.lean
@@ -62,9 +62,9 @@ def structureProjs (structTy : Expr) : CoreM (Name × Expr × Array (Name × Exp
     | throwError s!"structureProjs :: {structName} is not a structure"
   let structMkExpr := mkAppN (Expr.const structDotMk lvls) structTy.getAppArgs
   let tyArgs := structTy.getAppArgs
-  let nameMap : HashMap Name StructureFieldInfo := HashMap.ofList
-    (structInfo.fieldInfo.map (fun sfi => (sfi.fieldName, sfi))).data
-  let sorted := structInfo.fieldNames.map (fun name => nameMap.find! name)
+  let nameMap : Std.HashMap Name StructureFieldInfo := Std.HashMap.ofList
+    (structInfo.fieldInfo.map (fun sfi => (sfi.fieldName, sfi))).toList
+  let sorted := structInfo.fieldNames.map (fun name => nameMap.get! name)
   let fieldInfos := sorted.map (fun i =>
       -- Field name, Projection function
       (i.fieldName, mkAppN (Expr.const i.projFn lvls) tyArgs))
diff --git a/Auto/Lib/Pos.lean b/Auto/Lib/Pos.lean
index 91ba509..d909934 100644
--- a/Auto/Lib/Pos.lean
+++ b/Auto/Lib/Pos.lean
@@ -105,7 +105,7 @@ theorem ofNat'WF.doubleSucc_xI (n : Nat) :
 
 theorem ofNat'WF_toNat' (p : Pos) : ofNat'WF (toNat' p) = p := by
   induction p
-  case xH => rfl
+  case xH => rw [toNat', ofNat'WF]
   case xO p' IH =>
     dsimp [toNat'];
     rw [ofNat'WF.double_xO];
@@ -118,7 +118,7 @@ theorem ofNat'WF_toNat' (p : Pos) : ofNat'WF (toNat' p) = p := by
 theorem toNat'_ofNat'WF (n : Nat) : n ≠ 0 → toNat' (ofNat'WF n) = n := by
   revert n; apply ofNat'WF.induction
   case base₀ => intro H; contradiction
-  case base₁ => intro _; rfl
+  case base₁ => intro _; rw [ofNat'WF, toNat']
   case ind =>
     intro x IH _
     have hne : (x + 2) / 2 ≠ 0 := by
@@ -163,7 +163,7 @@ theorem ofNat'.equivAux (rd n : Nat) : rd ≥ n → ofNat'WF n = ofNat'RD rd n :
   induction rd generalizing n  <;> intro H
   case zero =>
     have hzero : n = 0 := Nat.eq_zero_of_le_zero H
-    rw [hzero]; rfl
+    rw [hzero, ofNat'WF]; rfl
   case succ rd' IH =>
     dsimp [ofNat'RD]
     match n with
diff --git a/Auto/Parser/LeanLex.lean b/Auto/Parser/LeanLex.lean
index 59ec179..087d4b9 100644
--- a/Auto/Parser/LeanLex.lean
+++ b/Auto/Parser/LeanLex.lean
@@ -8,7 +8,7 @@ namespace Auto
 -- **TODO**: Parser for POSIX ERE
 namespace Regex
 
-private def sort : List Nat → List Nat := 
+private def sort : List Nat → List Nat :=
   have : DecidableRel Nat.le := fun (x y : Nat) => inferInstanceAs (Decidable (x <= y))
   List.mergeSort Nat.le
 
@@ -82,17 +82,17 @@ deriving BEq, Hashable, Inhabited
 def EREBracket.neg (b : EREBracket) : EREBracket := .minus b (.cc .all)
 
 -- **TODO**: Why does this need `partial`?
-partial def EREBracket.toHashSet : EREBracket → HashSet Char
-  | .cc cty       => HashSet.empty.insertMany (toString cty).toList
-  | .inStr s      => HashSet.empty.insertMany s.toList
+partial def EREBracket.toHashSet : EREBracket → Std.HashSet Char
+  | .cc cty       => Std.HashSet.empty.insertMany (toString cty).toList
+  | .inStr s      => Std.HashSet.empty.insertMany s.toList
   | .plus ⟨bl⟩     => go bl
   | .minus b1 b2  =>
     let hb := b2.toHashSet
     let b1s := b1.toHashSet.toList
-    HashSet.empty.insertMany (b1s.filter (fun x => !hb.contains x))
+    Std.HashSet.empty.insertMany (b1s.filter (fun x => !hb.contains x))
 where
-  go : List EREBracket → HashSet Char
-    | [] => HashSet.empty
+  go : List EREBracket → Std.HashSet Char
+    | [] => Std.HashSet.empty
     | b :: bl => (go bl).insertMany (toHashSet b)
 
 def EREBracket.toString (e : EREBracket) := String.mk e.toHashSet.toList
@@ -184,9 +184,9 @@ section
   structure CharGrouping where
     ngroup  : Nat
     -- All relevant characters
-    all     : HashSet σ
+    all     : Std.HashSet σ
     -- Map from character to its corresponding group
-    charMap : HashMap σ Nat
+    charMap : Std.HashMap σ Nat
     -- A character is in `all` iff it's in `charMap`.
     -- Group number takes value in `0, 1, ..., ngroups - 1`
     -- For the intermediate `NFA` generated in `ERE.toADFA`,
@@ -213,21 +213,21 @@ section
     --   Refer to `ERE.toADFA`, `ERE.ADFALex` and `DFA.run`
     cg  : CharGrouping σ
   deriving Inhabited
-  
+
   variable {σ : Type} [Hashable σ] [BEq σ] [ToString σ]
-  
+
   def CharGrouping.wf : CharGrouping σ → Bool :=
     fun ⟨ngroup, all, charMap⟩ =>
-      let img := charMap.fold (fun hs _ n => hs.insert n) HashSet.empty
+      let img := charMap.fold (fun hs _ n => hs.insert n) Std.HashSet.empty
       let surj := (sort img.toList) == List.range ngroup
       let allInCharMap := all.toList.all (fun c => charMap.contains c)
       let sizeEq := all.size == charMap.size
       surj && allInCharMap && sizeEq
-  
-  def CharGrouping.groups : CharGrouping σ → Array (HashSet σ) :=
+
+  def CharGrouping.groups : CharGrouping σ → Array (Std.HashSet σ) :=
     fun ⟨ngroup, _, charMap⟩ => Id.run <| do
-      let mut arr : Array (HashSet σ) := 
-        Array.mk ((List.range ngroup).map (fun _ => HashSet.empty))
+      let mut arr : Array (Std.HashSet σ) :=
+        Array.mk ((List.range ngroup).map (fun _ => Std.HashSet.empty))
       for (c, idx) in charMap.toList do
         arr := arr.modify idx (fun hs => hs.insert c)
       return arr
@@ -244,7 +244,7 @@ section
                s!"Group representing beginning of string := {ngroup}" ::
                s!"Group representing end of string := {ngroup + 1}" ::
                s!"Group representing other utf-8 characters := {ngroup + 2}" ::
-               groups.data
+               groups.toList
     String.intercalate "\n  " all ++ "\n⦘⦘"
 
   def CharGrouping.toString (cg : CharGrouping σ) : String :=
@@ -254,7 +254,7 @@ section
     toString := CharGrouping.toString
 
   def CharGrouping.getGroup (cg : CharGrouping σ) (c : σ) : Nat :=
-    match cg.charMap.find? c with
+    match cg.charMap.get? c with
     | .some g => g
     -- Invalid character
     | .none   => cg.ngroup + 2
@@ -278,14 +278,14 @@ section
                  s!"Group representing beginning of string := {cg.ngroup}" ::
                  s!"Group representing end of string := {cg.ngroup + 1}" ::
                  s!"Group representing other utf-8 characters := {cg.ngroup + 2}" ::
-                 "(GroupIdx, Group members):" :: cggroups.data ++
-                 s!"(State, GroupIdx → State'):" :: dtr.data ++
-                 s!"(State, Attributes)" :: attrs.data
+                 "(GroupIdx, Group members):" :: cggroups.toList ++
+                 s!"(State, GroupIdx → State'):" :: dtr.toList ++
+                 s!"(State, Attributes)" :: attrs.toList
       String.intercalate "\n  " all ++ "\n⦘⦘"
 
   def ADFA.toString (a : ADFA σ) : String := ADFA.toStringAux a
     (fun l => ToString.toString l.toList)
-  
+
   instance : ToString (ADFA σ) where
     toString := ADFA.toString
 
@@ -297,7 +297,7 @@ section
 end
 
 def CharGrouping.toStringForChar (cg : CharGrouping Char) : String :=
-  CharGrouping.toStringAux cg (fun l => 
+  CharGrouping.toStringAux cg (fun l =>
     let sorted := sort (l.toList.map Char.toNat)
     let str := String.mk (sorted.map Char.ofNat)
     ToString.toString (repr str))
@@ -306,7 +306,7 @@ instance : ToString (CharGrouping Char) where
   toString := CharGrouping.toStringForChar
 
 def ADFA.toStringForChar (a : ADFA Char) : String :=
-  ADFA.toStringAux a (fun l => 
+  ADFA.toStringAux a (fun l =>
     let sorted := sort (l.toList.map Char.toNat)
     let str := String.mk (sorted.map Char.ofNat)
     ToString.toString (repr str))
@@ -316,38 +316,38 @@ instance : ToString (ADFA Char) where
 
 def ERE.charGrouping (e : ERE) : CharGrouping Char := Id.run <| do
   let hsets := e.brackets.map EREBracket.toHashSet
-  let mut all := hsets.foldl (fun hs nhs => hs.insertMany nhs) HashSet.empty
-  let mut charMap := all.fold (fun hs c => hs.insert c 0) HashMap.empty
+  let mut all := hsets.foldl (fun hs nhs => hs.insertMany nhs) Std.HashSet.empty
+  let mut charMap := all.fold (fun hs c => hs.insert c 0) Std.HashMap.empty
   -- Current number of groups
   let mut curidx := 1
   for hset in hsets do
-    let mut reloc : HashMap Nat Nat := {}
+    let mut reloc : Std.HashMap Nat Nat := {}
     for c in hset do
-      let cidx := charMap.find! c
-      match reloc.find? cidx with
+      let cidx := charMap.get! c
+      match reloc.get? cidx with
       | .some r => charMap := charMap.insert c r
       | .none => reloc := reloc.insert cidx curidx;
                  charMap := charMap.insert c curidx;
                  curidx := curidx + 1
   let mut ridx := 0
-  let mut reloc : HashMap Nat Nat := {}
+  let mut reloc : Std.HashMap Nat Nat := {}
   for (_, i) in charMap.toList do
-    match reloc.find? i with
+    match reloc.get? i with
     | .some _ => continue
     | .none   => reloc := reloc.insert i ridx; ridx := ridx + 1
-  charMap := HashMap.ofList (charMap.toList.map (fun (c, i) => (c, reloc.find! i)))
+  charMap := Std.HashMap.ofList (charMap.toList.map (fun (c, i) => (c, reloc.get! i)))
   return CharGrouping.mk ridx all charMap
 
 private partial def ERE.toNFAAux (cg : CharGrouping Char) : ERE → (NFA Nat)
 | .bracket b     =>
   let bs := toString b
-  let states := bs.foldl (fun hs c => hs.insert (cg.charMap.find! c)) HashSet.empty
+  let states := bs.foldl (fun hs c => hs.insert (cg.charMap.get! c)) Std.HashSet.empty
   NFA.ofSymbPlus states.toArray
 | .bracketN b    =>
   let bs := toString b
   -- All `utf-8` characters
-  let initHs := HashSet.empty.insertMany ((cg.ngroup + 2) :: List.range cg.ngroup)
-  let states := bs.foldl (fun hs c => hs.erase (cg.charMap.find! c)) initHs
+  let initHs := Std.HashSet.empty.insertMany ((cg.ngroup + 2) :: List.range cg.ngroup)
+  let states := bs.foldl (fun hs c => hs.erase (cg.charMap.get! c)) initHs
   NFA.ofSymbPlus states.toArray
 | .startp        => NFA.ofSymb (cg.ngroup)
 | .endp          => NFA.ofSymb (cg.ngroup + 1)
@@ -587,4 +587,4 @@ private def testit (a : ADFA Char) (s : Substring) (short:=false) (strict:=false
 
 end Regex
 
-end Auto
\ No newline at end of file
+end Auto
diff --git a/Auto/Parser/NDFA.lean b/Auto/Parser/NDFA.lean
index b59c949..0ea5eb9 100644
--- a/Auto/Parser/NDFA.lean
+++ b/Auto/Parser/NDFA.lean
@@ -5,7 +5,7 @@ open Lean
 
 namespace Auto
 
-private def sort : List Nat → List Nat := 
+private def sort : List Nat → List Nat :=
   have : DecidableRel Nat.le := fun (x y : Nat) => inferInstanceAs (Decidable (x <= y))
   List.mergeSort Nat.le
 
@@ -38,11 +38,11 @@ section NFA
     However, the initial state might have incoming edges
   -/
   structure NFA where
-    tr    : Array (HashMap (Unit ⊕ σ) (Array Nat))
+    tr    : Array (Std.HashMap (Unit ⊕ σ) (Array Nat))
     -- Each state (including the accept state) is associated
     --   with an array of attributes. So the length of `attrs`
     --   should be `tr.size + 1`
-    attrs : Array (HashSet String)
+    attrs : Array (Std.HashSet String)
   deriving Inhabited
 
   variable {σ : Type} [BEq σ] [Hashable σ]
@@ -61,12 +61,12 @@ section NFA
         c.toArray.map (fun el => snatS idx el))
       let tr := tr.concatMap id
       let attrs := n.attrs.mapIdx (fun idx attrs => s!"{idx} : {attrs.toList}")
-      let all := "NFA ⦗⦗" :: s!"Accept state := {n.tr.size}" :: tr.data ++ attrs.data
+      let all := "NFA ⦗⦗" :: s!"Accept state := {n.tr.size}" :: tr.toList ++ attrs.toList
       String.intercalate "\n  " all ++ "\n⦘⦘"
-  
+
     instance : ToString (NFA σ) where
       toString := NFA.toString
-  
+
     private def NFA.nextStatesOfState (r : NFA σ) (s : Nat) (c : Unit ⊕ σ) : Array Nat :=
       if h₁ : s > r.tr.size then
         panic! s!"NFA.nextStates :: State {s} is not valid for {r}"
@@ -80,12 +80,12 @@ section NFA
              have h₄ : (s = Array.size r.tr) = False := eq_false h₂
              simp [h₄] at h₃; simp [h₃]
         )
-        match hmap.find? c with
+        match hmap.get? c with
         | .some arr => arr
         | .none     => #[]
-    
+
     -- Why this does not need `partial`?
-    def NFA.εClosureOfStates (r : NFA σ) (ss : HashSet Nat) := Id.run <| do
+    def NFA.εClosureOfStates (r : NFA σ) (ss : Std.HashSet Nat) := Id.run <| do
       let mut front := ss.toArray
       let mut cur := 0
       let mut ret := ss
@@ -99,15 +99,15 @@ section NFA
             ret := ret.insert n
       return ret
 
-    def NFA.move (r : NFA σ) (ss : HashSet Nat) (c : σ) :=
+    def NFA.move (r : NFA σ) (ss : Std.HashSet Nat) (c : σ) :=
       let sss := ss.toArray.map (fun s => NFA.nextStatesOfState r s (.inr c))
-      sss.foldl (fun hs s => hs.insertMany s) HashSet.empty
+      sss.foldl (fun hs s => hs.insertMany s) Std.HashSet.empty
 
     -- Valid moves from a set of states `ss`, ignoring `ε` transitions
     -- Returns a hashmap from symbol to HashSet of states
-    def NFA.moves [ToString σ] (r : NFA σ) (ss : HashSet Nat) : HashMap σ (HashSet Nat) :=
+    def NFA.moves [ToString σ] (r : NFA σ) (ss : Std.HashSet Nat) : Std.HashMap σ (Std.HashSet Nat) :=
       Id.run <| do
-        let mut ret : HashMap σ (HashSet Nat) := {}
+        let mut ret : Std.HashMap σ (Std.HashSet Nat) := {}
         for i in ss do
           if i > r.tr.size then
             panic! s!"NFA.moves :: {i} from state set {ss.toList} is not a valid state of {r}"
@@ -121,22 +121,22 @@ section NFA
               -- Ignore `ε` transitions
               | .inl .unit => continue
               | .inr c =>
-                if let some d := ret.find? c then
+                if let some d := ret.get? c then
                   ret := ret.insert c (d.insertMany dests)
                 else
-                  ret := ret.insert c (HashSet.empty.insertMany dests)
+                  ret := ret.insert c (Std.HashSet.empty.insertMany dests)
         return ret
-  
+
     -- Move, then compute ε-closure
-    def NFA.moveε (r : NFA σ) (ss : HashSet Nat) (c : σ) : HashSet Nat :=
+    def NFA.moveε (r : NFA σ) (ss : Std.HashSet Nat) (c : σ) : Std.HashSet Nat :=
       r.εClosureOfStates (r.move ss c)
 
-    def NFA.moveεMany (r : NFA σ) (ss : HashSet Nat) (cs : Array σ) :=
+    def NFA.moveεMany (r : NFA σ) (ss : Std.HashSet Nat) (cs : Array σ) :=
       cs.foldl (fun ss' c => r.moveε ss' c) ss
 
     def NFA.run (r : NFA σ) (cs : Array σ) :=
-      r.moveεMany (r.εClosureOfStates (HashSet.empty.insert 0)) cs
-  
+      r.moveεMany (r.εClosureOfStates (Std.HashSet.empty.insert 0)) cs
+
   end Run
 
   /-- Criterion : The destination of all transitions should be ≤ n.size -/
@@ -149,10 +149,10 @@ section NFA
   def NFA.normalize (n : NFA σ) : NFA σ :=
     let size := n.tr.size
     let normEntry (x : _ × Array Nat) :=
-      (x.fst, (HashSet.empty.insertMany (x.snd.filter (· <= size))).toArray)
-    let tr' := n.tr.map (fun hs => HashMap.ofList (hs.toList.map normEntry))
+      (x.fst, (Std.HashSet.empty.insertMany (x.snd.filter (· <= size))).toArray)
+    let tr' := n.tr.map (fun hs => Std.HashMap.ofList (hs.toList.map normEntry))
     let attrs' := n.attrs[0:size+1].toArray
-    let attrs' := attrs'.append ⟨(List.range (size + 1 - attrs'.size)).map (fun _ => HashSet.empty)⟩
+    let attrs' := attrs'.append ⟨(List.range (size + 1 - attrs'.size)).map (fun _ => Std.HashSet.empty)⟩
     NFA.mk tr' attrs'
 
   /-- Whether the NFA's initial state has incoming edges -/
@@ -162,11 +162,11 @@ section NFA
   private def NFA.relocateEntry (x : α × Array Nat) (off : Nat) :=
     (x.fst, x.snd.map (· + off))
 
-  private def NFA.relocateHMap (x : HashMap (Unit ⊕ σ) (Array Nat)) (off : Nat) :=
-    HashMap.ofList (x.toList.map (relocateEntry · off))
+  private def NFA.relocateHMap (x : Std.HashMap (Unit ⊕ σ) (Array Nat)) (off : Nat) :=
+    Std.HashMap.ofList (x.toList.map (relocateEntry · off))
 
-  private def NFA.addEdgesToHMap (x : HashMap (Unit ⊕ σ) (Array Nat)) (e : (Unit ⊕ σ) × Array Nat) :=
-      x.insert e.fst (match x.find? e.fst with | some arr => arr ++ e.snd | none => e.snd)
+  private def NFA.addEdgesToHMap (x : Std.HashMap (Unit ⊕ σ) (Array Nat)) (e : (Unit ⊕ σ) × Array Nat) :=
+      x.insert e.fst (match x.get? e.fst with | some arr => arr ++ e.snd | none => e.snd)
 
   /-- Add attribute to a specific state -/
   def NFA.addAttrToState (n : NFA σ) (s : Nat) (attr : String) :=
@@ -185,15 +185,15 @@ section NFA
       NFA.mk n.tr new_attrs
 
   /-- Does not accept any string -/
-  def NFA.zero : NFA σ := NFA.mk #[HashMap.empty] #[.empty, .empty]
+  def NFA.zero : NFA σ := NFA.mk #[Std.HashMap.empty] #[.empty, .empty]
 
   /-- Only accepts empty string -/
   def NFA.epsilon : NFA σ :=
-    NFA.mk #[HashMap.empty.insert (.inl .unit) #[1]] #[.empty, .empty]
+    NFA.mk #[Std.HashMap.empty.insert (.inl .unit) #[1]] #[.empty, .empty]
 
   /-- Accepts a character -/
   def NFA.ofSymb (c : σ) : NFA σ :=
-    NFA.mk #[HashMap.empty.insert (.inr c) #[1]] #[.empty, .empty]
+    NFA.mk #[Std.HashMap.empty.insert (.inr c) #[1]] #[.empty, .empty]
 
   /-- Produce an NFA whose language is the union of `m`'s and `n`'s -/
   def NFA.plus (m n : NFA σ) : NFA σ :=
@@ -202,16 +202,16 @@ section NFA
     let off_n := m.tr.size + 2
     -- `acc'` is the new accept state
     let acc' := m.tr.size + n.tr.size + 3
-    let initTrans : HashMap (Unit ⊕ σ) (Array Nat) :=
-      HashMap.empty.insert (Sum.inl .unit) #[off_m, off_n]
+    let initTrans : Std.HashMap (Unit ⊕ σ) (Array Nat) :=
+      Std.HashMap.empty.insert (Sum.inl .unit) #[off_m, off_n]
     -- Move the states of `m` by `off_m`
     let new_mtr := m.tr.map (relocateHMap · off_m)
-    let new_mtr := new_mtr.push (HashMap.empty.insert (.inl .unit) #[acc'])
+    let new_mtr := new_mtr.push (Std.HashMap.empty.insert (.inl .unit) #[acc'])
     -- Move the states of `n` by `off_n`
     let new_ntr := n.tr.map (relocateHMap · off_n)
-    let new_ntr := new_ntr.push (HashMap.empty.insert (.inl .unit) #[acc'])
+    let new_ntr := new_ntr.push (Std.HashMap.empty.insert (.inl .unit) #[acc'])
     let new_tr := #[initTrans] ++ new_mtr ++ new_ntr
-    let new_attrs := #[HashSet.empty] ++ m.attrs ++ n.attrs ++ #[HashSet.empty]
+    let new_attrs := #[Std.HashSet.empty] ++ m.attrs ++ n.attrs ++ #[Std.HashSet.empty]
     NFA.mk new_tr new_attrs
 
   def NFA.multiPlus (as : Array (NFA σ)) :=
@@ -221,16 +221,16 @@ section NFA
     | _ =>
       let (acc', offs) : Nat × Array Nat :=
         as.foldl (fun (cur, acc) (arr : NFA σ) => (cur + arr.tr.size + 1, acc.push cur)) (1, #[])
-      let initTrans : HashMap (Unit ⊕ σ) (Array Nat) :=
-        HashMap.empty.insert (Sum.inl .unit) offs
+      let initTrans : Std.HashMap (Unit ⊕ σ) (Array Nat) :=
+        Std.HashMap.empty.insert (Sum.inl .unit) offs
       let trs := (as.zip offs).map (fun ((a, off) : NFA σ × Nat) =>
           let new_a := a.tr.map (relocateHMap · off)
-          new_a.push (HashMap.empty.insert (.inl .unit) #[acc'])
+          new_a.push (Std.HashMap.empty.insert (.inl .unit) #[acc'])
         )
       let new_tr := (#[#[initTrans]] ++ trs).concatMap id
-      let new_attrs := #[HashSet.empty] ++
+      let new_attrs := #[Std.HashSet.empty] ++
                        (as.map (fun (⟨_, attrs⟩ : NFA σ) => attrs)).concatMap id ++
-                       #[HashSet.empty]
+                       #[Std.HashSet.empty]
       NFA.mk new_tr new_attrs
 
   def NFA.comp (m n : NFA σ) : NFA σ :=
@@ -267,11 +267,11 @@ section NFA
     let acc' := m.tr.size + 2
     -- The new location of the original accept state of `m`
     -- let macc' := m.size + 1
-    let initTrans : HashMap (Unit ⊕ σ) (Array Nat) :=
-      HashMap.empty.insert (Sum.inl .unit) #[1, acc']
+    let initTrans : Std.HashMap (Unit ⊕ σ) (Array Nat) :=
+      Std.HashMap.empty.insert (Sum.inl .unit) #[1, acc']
     -- Move the states of `m` by `1`
     let new_mtr := m.tr.map (relocateHMap · 1)
-    let new_mtr := new_mtr.push (HashMap.empty.insert (.inl .unit) #[1, acc'])
+    let new_mtr := new_mtr.push (Std.HashMap.empty.insert (.inl .unit) #[1, acc'])
     let new_tr := #[initTrans] ++ new_mtr
     let new_attrs := #[.empty] ++ m.attrs ++ #[.empty]
     NFA.mk new_tr new_attrs
@@ -282,7 +282,7 @@ section NFA
   | .cons a .nil => a
   | a :: as => NFA.comp a (NFA.multiCompAux as)
 
-  def NFA.multiComp (a : Array (NFA σ)) := NFA.multiCompAux a.data
+  def NFA.multiComp (a : Array (NFA σ)) := NFA.multiCompAux a.toList
 
   def NFA.repeatN (r : NFA σ) (n : Nat) := NFA.multiComp ⟨(List.range n).map (fun _ => r)⟩
 
@@ -296,7 +296,7 @@ section NFA
         if r.hasEdgeToInit then
           -- Add a new state as the initial state so that the
           --   new initial state has no incoming edges
-          let new_tr := #[HashMap.empty.insert (.inl .unit) #[1]] ++ r.tr.map (relocateHMap · 1)
+          let new_tr := #[Std.HashMap.empty.insert (.inl .unit) #[1]] ++ r.tr.map (relocateHMap · 1)
           let new_attrs := #[.empty] ++ r.attrs
           NFA.mk new_tr new_attrs
         else
@@ -309,7 +309,7 @@ section NFA
           new_r.modify 0 (fun hm => NFA.addEdgesToHMap hm (.inl .unit, #[acc']))
         )
       let new_tr := new_trs.concatMap id
-      let new_attrs : Array (HashSet String) :=
+      let new_attrs : Array (Std.HashSet String) :=
         ((Array.mk (List.range (n - 1))).map (fun _ => r.attrs[:r.tr.size].toArray)).concatMap id ++
         r.attrs
       NFA.mk new_tr new_attrs
@@ -322,11 +322,11 @@ section NFA
 
   /-- Accepts all characters in an array of characters -/
   def NFA.ofSymbPlus (cs : Array σ) : NFA σ :=
-    NFA.mk #[HashMap.ofList (cs.map (fun c => (.inr c,#[1]))).data] #[.empty, .empty]
+    NFA.mk #[Std.HashMap.ofList (cs.map (fun c => (.inr c,#[1]))).toList] #[.empty, .empty]
 
   /-- An `NFA UInt32` that accepts exactly a string -/
   def NFA.ofSymbComp (s : Array σ) : NFA σ :=
-    let tr := (Array.mk s.data).mapIdx (fun idx c => HashMap.empty.insert (.inr c) #[idx.val + 1])
+    let tr := (Array.mk s.toList).mapIdx (fun idx c => Std.HashMap.empty.insert (.inr c) #[idx.val + 1])
     let attrs := Array.mk ((List.range (s.size + 1)).map (fun _ => .empty))
     NFA.mk tr attrs
 
@@ -339,7 +339,7 @@ section NFA
       HashMap.ofList [(.inr "a", #[5]), (.inr "b", #[1, 0])],
       HashMap.ofList [(.inl .unit, #[1]), (.inr "c", #[2, 4]), (.inr "a", #[6,1,2])]
     ], #[]⟩
-  
+
   def test₂ : NFA String := test₁.normalize
 
   #eval IO.println test₁
@@ -370,13 +370,13 @@ section NFA
 end NFA
 
 section DFA
-  
+
   -- Alphabet of DFA
   variable (σ : Type) [BEq σ] [Hashable σ]
 
   structure DFA where
     -- Array of accept states
-    accepts : HashSet Nat
+    accepts : Std.HashSet Nat
     -- Transition function
     -- `0` is the initial statet
     -- `{0, 1, ⋯, tr.size}` are the set of allowed states, where
@@ -385,13 +385,13 @@ section DFA
     -- If the transition map of state `i` does not include
     --   an entry for character `c`, then the transition from
     --   `i` to `c` ends in `malformed input` state
-    tr      : Array (HashMap σ Nat)
+    tr      : Array (Std.HashMap σ Nat)
     -- Each state (except for the `malformed input` state)
     --   is associated with an array of attributes.
     -- So, we should have `attrs.size == tr.size`
-    attrs   : Array (HashSet String)
+    attrs   : Array (Std.HashSet String)
   deriving Inhabited
-  
+
   variable {σ : Type} [BEq σ] [Hashable σ] [ToString σ]
 
   def DFA.toString (d : DFA σ) : String :=
@@ -402,7 +402,7 @@ section DFA
     let all := "DFA ⦗⦗" ::
                s!"Accept states := {d.accepts.toList}" ::
                s!"Size (Malformed-input state) = {d.tr.size}" ::
-               tr.data ++ attrs.data
+               tr.toList ++ attrs.toList
     String.intercalate "\n  " all ++ "\n⦘⦘"
 
   instance : ToString (DFA σ) where
@@ -422,7 +422,7 @@ section DFA
            have h₄ : (s = Array.size _) = False := eq_false h₂
            simp [h₄] at h₃; simp [h₃]
       )
-      match hmap.find? c with
+      match hmap.get? c with
       | .some s => s
       -- `malformed input`
       | .none   => d.tr.size
@@ -431,17 +431,17 @@ section DFA
     if !n.wf then
       panic! s!"DFA.ofNFA :: {n} is not well-formed"
     -- Array of states
-    let mut dstates : Array (List Nat) := #[sort (n.εClosureOfStates (HashSet.empty.insert 0)).toList]
+    let mut dstates : Array (List Nat) := #[sort (n.εClosureOfStates (Std.HashSet.empty.insert 0)).toList]
     -- Map from state to idx of state
-    let mut idxmap : HashMap (List Nat) Nat :=
-      HashMap.empty.insert dstates[0]! 0
+    let mut idxmap : Std.HashMap (List Nat) Nat :=
+      Std.HashMap.empty.insert dstates[0]! 0
     -- `Unit` represents the `malformed input` state
-    let mut tr : Array (HashMap σ (Nat ⊕ Unit)) := #[{}]
+    let mut tr : Array (Std.HashMap σ (Nat ⊕ Unit)) := #[{}]
     -- Next state to process
     let mut cur := 0
     while h : cur < dstates.size do
       let st := dstates[cur]
-      let moves := n.moves (HashSet.empty.insertMany st)
+      let moves := n.moves (Std.HashSet.empty.insertMany st)
       for (c, st) in moves.toList do
         -- If `st` is empty, then the move ends in `malformed input` state
         if st.size == 0 then
@@ -454,11 +454,11 @@ section DFA
           idxmap := idxmap.insert εst idxmap.size
           tr := tr.push {}
         -- Now `idxmap` contains `εst`
-        let idx := idxmap.find! εst
+        let idx := idxmap.get! εst
         tr := tr.modify cur (fun hmap => hmap.insert c (.inl idx))
       cur := cur + 1
     let rettr := tr.map (
-      fun hmap => HashMap.ofList (hmap.toList.map (
+      fun hmap => Std.HashMap.ofList (hmap.toList.map (
         fun (s, nu) =>
           match nu with
           | .inl n => (s, n)
@@ -466,9 +466,9 @@ section DFA
       ))
     )
     let accepts := dstates.mapIdx (fun idx l => if l.contains n.tr.size then some idx.val else none)
-    let accepts := accepts.foldl (fun hs o => if let some x := o then hs.insert x else hs) HashSet.empty
-    let attrs := dstates.map (fun l => 
-      (Array.mk l).foldl (fun acc s => if let some x := n.attrs[s]? then acc.insertMany x else acc) HashSet.empty)
+    let accepts := accepts.foldl (fun hs o => if let some x := o then hs.insert x else hs) Std.HashSet.empty
+    let attrs := dstates.map (fun l =>
+      (Array.mk l).foldl (fun acc s => if let some x := n.attrs[s]? then acc.insertMany x else acc) Std.HashSet.empty)
     return DFA.mk accepts rettr attrs
 
   /-
diff --git a/Auto/Parser/SMTParser.lean b/Auto/Parser/SMTParser.lean
index 4523ba0..98129eb 100644
--- a/Auto/Parser/SMTParser.lean
+++ b/Auto/Parser/SMTParser.lean
@@ -99,7 +99,7 @@ open Term
 
 partial def Term.toString : Term → String
 | .atom l => ToString.toString l
-| .app ls => "(" ++ String.intercalate " " (ls.map toString).data ++ ")"
+| .app ls => "(" ++ String.intercalate " " (ls.map toString).toList ++ ")"
 
 instance : ToString Term where
   toString e := Term.toString e
diff --git a/Auto/Translation/Assumptions.lean b/Auto/Translation/Assumptions.lean
index 6c26579..c2311d9 100644
--- a/Auto/Translation/Assumptions.lean
+++ b/Auto/Translation/Assumptions.lean
@@ -17,7 +17,7 @@ deriving Inhabited, Hashable, BEq
 
 partial def DTr.toString : DTr → String
 | .node s dtrs =>
-  s ++ " [" ++ String.intercalate ", " (dtrs.map DTr.toString).data ++ "]"
+  s ++ " [" ++ String.intercalate ", " (dtrs.map DTr.toString).toList ++ "]"
 | .leaf s => s
 
 instance : ToString DTr where
@@ -103,7 +103,7 @@ def Lemma.equivQuick (lem₁ lem₂ : Lemma) : MetaM Bool := do
 
 /-- Reorder top-level `∀` so that (non-prop / dependent) ones precede other ones -/
 def Lemma.reorderForallInstDep (lem : Lemma) : MetaM Lemma := do
-  let depargs := HashSet.empty.insertMany (Expr.depArgs lem.type)
+  let depargs := Std.HashSet.empty.insertMany (Expr.depArgs lem.type)
   Meta.forallTelescope lem.type fun xs body => do
     let mut prec := #[]
     let mut trail := #[]
@@ -279,7 +279,7 @@ deriving Inhabited, Hashable, BEq
 instance : ToMessageData MLemmaInst where
   toMessageData mi := MessageData.compose
     m!"MLemmaInst ⦗⦗ {mi.origProof} " (.compose
-      (MessageData.intercalate " " (mi.args.data.map (fun e => m!"({e})")))
+      (MessageData.intercalate " " (mi.args.toList.map (fun e => m!"({e})")))
         m!" : {mi.type} ⦘⦘")
 
 def MLemmaInst.ofLemmaInst (li : LemmaInst) : MetaM (Array Level × Array Expr × MLemmaInst) := do
@@ -313,13 +313,13 @@ def LemmaInst.ofMLemmaInst (mi : MLemmaInst) : MetaM LemmaInst := do
   let lem : Lemma := ⟨⟨proof, type, deriv⟩, s.paramNames⟩
   return ⟨lem, nbinders, nargs⟩
 
-partial def collectUniverseLevels : Expr → MetaM (HashSet Level)
-| .bvar _ => return HashSet.empty
+partial def collectUniverseLevels : Expr → MetaM (Std.HashSet Level)
+| .bvar _ => return Std.HashSet.empty
 | e@(.fvar _) => do collectUniverseLevels (← instantiateMVars (← Meta.inferType e))
 | e@(.mvar _) => do collectUniverseLevels (← instantiateMVars (← Meta.inferType e))
-| .sort u => return HashSet.empty.insert u
+| .sort u => return Std.HashSet.empty.insert u
 | e@(.const _ us) => do
-  let hus := HashSet.empty.insertMany us
+  let hus := Std.HashSet.empty.insertMany us
   let tys ← collectUniverseLevels (← instantiateMVars (← Meta.inferType e))
   return mergeHashSet hus tys
 | .app fn arg => do
@@ -339,14 +339,14 @@ partial def collectUniverseLevels : Expr → MetaM (HashSet Level)
   let vs ← collectUniverseLevels v
   let bodys ← collectUniverseLevels body
   return mergeHashSet (mergeHashSet tys vs) bodys
-| .lit _ => return HashSet.empty.insert (.succ .zero)
+| .lit _ => return Std.HashSet.empty.insert (.succ .zero)
 | .mdata _ e' => collectUniverseLevels e'
 | .proj .. => throwError "Please unfold projections before collecting universe levels"
 
 def computeMaxLevel (facts : Array UMonoFact) : MetaM Level := do
   let levels ← facts.foldlM (fun hs ⟨_, ty, _⟩ => do
     let tyUs ← collectUniverseLevels ty
-    return mergeHashSet tyUs hs) HashSet.empty
+    return mergeHashSet tyUs hs) Std.HashSet.empty
   -- Compute the universe level that we need to lift to
   -- Use `.succ` two times to reveal bugs
   let level := Level.succ (.succ (levels.fold (fun l l' => Level.max l l') Level.zero))
diff --git a/Auto/Translation/Inhabitation.lean b/Auto/Translation/Inhabitation.lean
index b401db5..14cf56e 100644
--- a/Auto/Translation/Inhabitation.lean
+++ b/Auto/Translation/Inhabitation.lean
@@ -5,7 +5,7 @@ open Lean
 
 namespace Auto.Inhabitation
 
-private def logicalConsts : HashSet Name := HashSet.empty.insertMany
+private def logicalConsts : Std.HashSet Name := Std.HashSet.empty.insertMany
   #[``Eq, ``Exists, ``And, ``Or, ``Iff, ``Not]
 
 /--
@@ -28,7 +28,7 @@ where go (pos : Array Bool) (e : Expr) : Array (Array Bool) :=
   | _ => #[pos]
 
 def getExprNonImpPosition (pos : Array Bool) (e : Expr) : Option Expr :=
-  go pos.data e
+  go pos.toList e
 where go (pos : List Bool) (e : Expr) : Option Expr :=
   match pos with
   | .nil => .some e
diff --git a/Auto/Translation/Lam2DAtomAsFVar.lean b/Auto/Translation/Lam2DAtomAsFVar.lean
index b471ed7..ce5f137 100644
--- a/Auto/Translation/Lam2DAtomAsFVar.lean
+++ b/Auto/Translation/Lam2DAtomAsFVar.lean
@@ -50,11 +50,11 @@ structure State where
   -- Etoms to be abstracted
   etomsToAbstract : Array (FVarId × Nat)  := #[]
   -- Type atoms that are used in the expressions sent to external prover
-  typeAtomFVars   : HashMap Nat Expr      := {}
+  typeAtomFVars   : Std.HashMap Nat Expr      := {}
   -- Term atoms that are used in the expressions sent to external prover
-  termAtomFVars   : HashMap Nat Expr      := {}
+  termAtomFVars   : Std.HashMap Nat Expr      := {}
   -- Etoms that are used in the expression sent to external prover
-  etomFVars       : HashMap Nat Expr      := {}
+  etomFVars       : Std.HashMap Nat Expr      := {}
 
 abbrev ExternM := StateRefT State MetaStateM
 
diff --git a/Auto/Translation/Lam2TH0.lean b/Auto/Translation/Lam2TH0.lean
index 585890c..b1996fa 100644
--- a/Auto/Translation/Lam2TH0.lean
+++ b/Auto/Translation/Lam2TH0.lean
@@ -40,6 +40,6 @@ def lam2TH0 (lamVarTy : Array LamSort) (lamEVarTy : Array LamSort) (facts : Arra
     | .ok ts => return s!"thf(fact{i}, axiom, {ts})."
     | .error e => throwError e)
   let sep := "\n"
-  return s!"{String.intercalate sep sorts}\n\n{String.intercalate sep types}\n\n{String.intercalate sep facts.data}"
+  return s!"{String.intercalate sep sorts}\n\n{String.intercalate sep types}\n\n{String.intercalate sep facts.toList}"
 
 end Auto
diff --git a/Auto/Translation/LamFOL2SMT.lean b/Auto/Translation/LamFOL2SMT.lean
index 56570cc..a2f397f 100644
--- a/Auto/Translation/LamFOL2SMT.lean
+++ b/Auto/Translation/LamFOL2SMT.lean
@@ -50,19 +50,19 @@ instance : ToString LamAtomic where
   toString := LamAtomic.toString
 
 def LamAtomic.toLeanExpr
-  (tyValMap varValMap etomValMap : HashMap Nat Expr)
+  (tyValMap varValMap etomValMap : Std.HashMap Nat Expr)
   (atomic : LamAtomic) : MetaM Expr:=
   match atomic with
   | .sort n => do
-    let .some e := tyValMap.find? n
+    let .some e := tyValMap.get? n
       | throwError "SMT.printValuation :: Unknown sort atom {n}"
     return e
   | .term n => do
-    let .some e := varValMap.find? n
+    let .some e := varValMap.get? n
       | throwError "SMT.printValuation :: Unknown term atom {n}"
     return e
   | .etom n => do
-    let .some e := etomValMap.find? n
+    let .some e := etomValMap.get? n
       | throwError "SMT.printValuation :: Unknown etom {n}"
     return e
   | .bvOfNat n => do
@@ -600,11 +600,11 @@ def termAuxDecls : Array IR.SMT.Command :=
   `printFn : (tyValMap : _) → (varValMap : _) → (etomValMap : _) → MetaM α`
 -/
 def withExprValuation
-  {α : Type} [Inhabited α] (sni : SMTNamingInfo) (h2lMap : HashMap LamAtomic String)
-  (printFn : HashMap Nat Expr → HashMap Nat Expr → HashMap Nat Expr → MetaM α) :
+  {α : Type} [Inhabited α] (sni : SMTNamingInfo) (h2lMap : Std.HashMap LamAtomic String)
+  (printFn : Std.HashMap Nat Expr → Std.HashMap Nat Expr → Std.HashMap Nat Expr → MetaM α) :
   MetaM α := do
-  let tyValMap := HashMap.ofList (sni.tyVal.zipWithIndex.map (fun ((e, _), n) => (n, e))).data
-  let varValMap := HashMap.ofList (sni.varVal.zipWithIndex.map (fun ((e, _), n) => (n, e))).data
+  let tyValMap := Std.HashMap.ofList (sni.tyVal.zipWithIndex.map (fun ((e, _), n) => (n, e))).toList
+  let varValMap := Std.HashMap.ofList (sni.varVal.zipWithIndex.map (fun ((e, _), n) => (n, e))).toList
   let etomsWithName := h2lMap.toArray.filterMap (fun (atomic, name) =>
     match atomic with | .etom n => .some (n, name) | _ => .none)
   let declInfos ← etomsWithName.mapM (fun (n, name) => do
@@ -613,7 +613,7 @@ def withExprValuation
     let type ← Lam2D.interpLamSortAsUnlifted tyValMap s
     return (Name.mkSimple name, .default, fun _ => pure type))
   Meta.withLocalDecls declInfos (fun etomFVars => do
-    let etomValMap := HashMap.ofList ((etomsWithName.zip etomFVars).map (fun ((n, _), e) => (n, e))).data
+    let etomValMap := Std.HashMap.ofList ((etomsWithName.zip etomFVars).map (fun ((n, _), e) => (n, e))).toList
     printFn tyValMap varValMap etomValMap)
 
 end SMT
@@ -651,7 +651,7 @@ open SMT in
 def lamFOL2SMTWithExtraInfo
   (sni : SMTNamingInfo) (lamVarTy lamEVarTy : Array LamSort)
   (facts : Array LamTerm) (minds : Array MutualIndInfo) :
-  TransM LamAtomic (Array IR.SMT.Command × Array STerm × HashMap String LamAtomic × Array SelectorInfo) := do
+  TransM LamAtomic (Array IR.SMT.Command × Array STerm × Std.HashMap String LamAtomic × Array SelectorInfo) := do
   let _ ← sortAuxDecls.mapM addCommand
   let _ ← termAuxDecls.mapM addCommand
   let mut selInfos : Array SelectorInfo := #[]
diff --git a/Auto/Translation/LamReif.lean b/Auto/Translation/LamReif.lean
index 8350e58..e1baac8 100644
--- a/Auto/Translation/LamReif.lean
+++ b/Auto/Translation/LamReif.lean
@@ -33,13 +33,13 @@ open Embedding.Lam
 -/
 structure State where
   -- Maps previously reified type to their type atom index
-  tyVarMap      : HashMap Expr Nat                := {}
+  tyVarMap      : Std.HashMap Expr Nat                := {}
   -- Maps previously reified expressions to their term atom index
   -- Whenever we encounter an atomic expression, we look up
   --   `varMap`. If it's already reified, then `varMap`
   --   tells us about its index. If it's not reified, insert
   --   it to `varMap`.
-  varMap        : HashMap Expr Nat                := {}
+  varMap        : Std.HashMap Expr Nat                := {}
   -- `tyVal` is the inverse of `tyVarMap`
   -- The `e : Expr` is the un-lifted valuation of the type atom
   -- The `lvl : level` is the sort level of `e`
@@ -54,7 +54,7 @@ structure State where
   -- lamILTy
   lamILTy       : Array LamSort                   := #[]
   -- Inverse of `lamILTy`
-  isomTyMap     : HashMap LamSort Nat             := {}
+  isomTyMap     : Std.HashMap LamSort Nat             := {}
   /-
     This hashmap contains assertions that have external (lean) proof
     · The key `t : LamTerm` is the corresponding λ term,
@@ -67,7 +67,7 @@ structure State where
 
     This field also corresponds to the `ImportTable` in `LamChecker.lean`
   -/
-  assertions    : HashMap LamTerm (Expr × DTr × LamTerm × Nat)   := {}
+  assertions    : Std.HashMap LamTerm (Expr × DTr × LamTerm × Nat)   := {}
   /-
     This hashmap contains lamsorts who has external proof of inhabitation
     · The key `s : LamSort` is the corresponding `λ` sort
@@ -75,12 +75,12 @@ structure State where
     · The second `DTr` is the derivation of `e` from the context
     · The third `n : Nat` is the position of the inhabitation fact in the `ImportTable`
   -/
-  inhabitations : HashMap LamSort (Expr × DTr × Nat)    := {}
+  inhabitations : Std.HashMap LamSort (Expr × DTr × Nat)    := {}
   -- Records the EvalResult and etoms generated by checksteps
   --   that produce etoms
-  chkStepCache  : HashMap ChkStep (EvalResult × Array Nat) := {}
+  chkStepCache  : Std.HashMap ChkStep (EvalResult × Array Nat) := {}
   -- The check step that produces a given etom
-  etomChkStep   : HashMap Nat ChkStep             := {}
+  etomChkStep   : Std.HashMap Nat ChkStep             := {}
   -- We insert entries into `rTable` through two different ways
   -- 1. Calling `newChkStep`
   -- 2. Validness facts from the ImportTable are treated in `newAssertions`
@@ -110,7 +110,7 @@ def getLamEVarTy : ReifM (Array LamSort) := do return (← getRst).lamEVarTy
 
 def getLamEVarTyTree : ReifM (BinTree LamSort) := do return (← getRst).lamEVarTyTree
 
-def getChkMap : ReifM (HashMap REntry ChkStep) := do return (← getRst).chkMap
+def getChkMap : ReifM (Std.HashMap REntry ChkStep) := do return (← getRst).chkMap
 
 def checkerStats : ReifM (Array (String × Nat)) := do
   return #[("tyVal", (← getTyVal).size), ("varVal", (← getVarVal).size),
@@ -120,7 +120,7 @@ def checkerStats : ReifM (Array (String × Nat)) := do
 def printCheckerStats : ReifM Unit := do
   let stats := (← checkerStats).map (fun (s, n) => "  " ++ s ++ s!": {n}")
   let ss := #["Checker Statistics:"] ++ stats
-  trace[auto.buildChecker] (String.intercalate "\n" ss.data)
+  trace[auto.buildChecker] (String.intercalate "\n" ss.toList)
 
 def printValuation : ReifM Unit := do
   let tyVal ← getTyVal
@@ -139,30 +139,30 @@ def printValuation : ReifM Unit := do
 def printProofs : ReifM Unit := do
   let chkMap ← getChkMap
   for re in (← getRTable) do
-    if let .some cs := chkMap.find? re then
+    if let .some cs := chkMap.get? re then
       let .some n := (← getRst).findPos? re
         | throwError "printProofs :: Unexpected error"
       let etoms :=
-        match (← getChkStepCache).find? cs with
+        match (← getChkStepCache).get? cs with
         | .some (_, arr) =>
-          if arr.size == 0 then m!"" else m!" and produces etoms {arr.data}"
+          if arr.size == 0 then m!"" else m!" and produces etoms {arr.toList}"
         | .none => m!""
       trace[auto.lamReif.printProofs] "{n} : ChkStep ⦗⦗{cs}⦘⦘ proves ⦗⦗{re}⦘⦘{etoms}"
     else
       match re with
       | .valid [] t =>
-        let .some (expr, _, n) := (← getAssertions).find? t
+        let .some (expr, _, n) := (← getAssertions).get? t
           | throwError "printProofs :: Unable to find assertion associated with {t}"
         trace[auto.lamReif.printProofs] "{n} : External fact ⦗⦗{← Meta.inferType expr}⦘⦘ proves ⦗⦗{re}⦘⦘"
       | .nonempty s =>
-        let .some (expr, _, n) := (← getInhabitations).find? s
+        let .some (expr, _, n) := (← getInhabitations).get? s
           | throwError "printProofs :: Unable to find inhabitation fact associated with {s}"
         trace[auto.lamReif.printProofs] "{n} : Inhabitation fact ⦗⦗{← Meta.inferType expr}⦘⦘ proves ⦗⦗{re}⦘⦘"
       | _ => throwError "printProofs :: Unexpected entry {re}"
 
 def sort2LamILTyIdx (s : LamSort) : ReifM Nat := do
   let isomTyMap ← getIsomTyMap
-  match isomTyMap.find? s with
+  match isomTyMap.get? s with
   | .some n => return n
   | .none =>
     let lamILTy ← getLamILTy
@@ -191,7 +191,7 @@ def lookupLamILTy! (idx : Nat) : ReifM LamSort := do
     throwError "lookupLamILTy! :: Unknown index {idx}"
 
 def lookupAssertion! (t : LamTerm) : ReifM (Expr × DTr × LamTerm × Nat) := do
-  if let .some r := (← getAssertions).find? t then
+  if let .some r := (← getAssertions).get? t then
     return r
   else
     throwError "lookupAssertion! :: Unknown assertion {t}"
@@ -208,11 +208,11 @@ def lookupREntryPos! (re : REntry) : ReifM Nat := do
   | .none =>
     match re with
     | .valid [] t =>
-      match (← getAssertions).find? t with
+      match (← getAssertions).get? t with
       | .some (_, _, _, n) => return n
       | .none => throwError "lookupREntryPos! :: Unknown REntry {re}"
     | .nonempty s =>
-      match (← getInhabitations).find? s with
+      match (← getInhabitations).get? s with
       | .some (_, _, n) => return n
       | .none => throwError "lookupREntryPos! :: Unknown REntry {re}"
     | _ => throwError "lookupREntryPos! :: Unknown REntry {re}"
@@ -223,16 +223,16 @@ inductive REntryProof where
   | assertion    : Expr → DTr → LamTerm → REntryProof
 
 def lookupREntryProof? (re : REntry) : ReifM (Option REntryProof) := do
-  match (← getChkMap).find? re with
+  match (← getChkMap).get? re with
   | .some cs => return .some (.chkStep cs)
   | .none =>
     match re with
     | .valid [] t =>
-      match (← getAssertions).find? t with
+      match (← getAssertions).get? t with
       | .some (e, deriv, t, _) => return .some (.assertion e deriv t)
       | .none => return .none
     | .nonempty s =>
-      match (← getInhabitations).find? s with
+      match (← getInhabitations).get? s with
       | .some (e, deriv, _) => return .some (.inhabitation e deriv s)
       | .none => return .none
     | _ => return .none
@@ -249,19 +249,19 @@ def lookupLamEVarTy! (idx : Nat) : ReifM LamSort := do
     throwError "lookupLamEVarTy! :: Unknown etom {idx}"
 
 def lookupChkStepEtom! (cs : ChkStep) : ReifM (Array Nat) := do
-  if let .some (_, arr) := (← getChkStepCache).find? cs then
+  if let .some (_, arr) := (← getChkStepCache).get? cs then
     return arr
   else
     throwError "lookupChkStepEtom! :: ChkStep {cs} did not produce new etom"
 
 def lookupChkStepResult! (cs : ChkStep) : ReifM EvalResult := do
-  if let .some (er, _) := (← getChkStepCache).find? cs then
+  if let .some (er, _) := (← getChkStepCache).get? cs then
     return er
   else
     throwError "lookupChkStepEtom! :: ChkStep {cs} did not produce new etom"
 
 def lookupEtomChkStep! (eidx : Nat) : ReifM ChkStep := do
-  if let .some c := (← getEtomChkStep).find? eidx then
+  if let .some c := (← getEtomChkStep).get? eidx then
     return c
   else
     throwError "lookupEtomChkStep! :: Unknown etom {eidx}"
@@ -337,7 +337,7 @@ def newChkStep (c : ChkStep) (res? : Option EvalResult) : ReifM (Bool × EvalRes
   --   twice may yield different results. So, we lookup
   --   `chkStepCache` to see whether this checkstep has
   --   been evaluated before
-  if let .some (res, _) := (← getChkStepCache).find? c then
+  if let .some (res, _) := (← getChkStepCache).get? c then
     return (false, res)
   let ltv ← getLamTyValAtMeta
   let res := c.eval ltv.lamVarTy ltv.lamILTy ⟨← getRTableTree, ← getMaxEVarSucc, ← getLamEVarTyTree⟩
@@ -694,7 +694,7 @@ section Checker
   def validOfBVarLowers (v : REntry) (ns : Array REntry) : ReifM REntry := do
     let pv ← lookupREntryPos! v
     let pns ← ns.mapM lookupREntryPos!
-    let (_, .addEntry re) ← newChkStep (.i (.validOfBVarLowers pv pns.data)) .none
+    let (_, .addEntry re) ← newChkStep (.i (.validOfBVarLowers pv pns.toList)) .none
       | throwError "validOfBVarLowers :: Unexpected evaluation result"
     return re
 
@@ -716,20 +716,20 @@ section Checker
   def validOfImps (impV : REntry) (hypVs : Array REntry) : ReifM REntry := do
     let imp ← lookupREntryPos! impV
     let ps ← hypVs.mapM lookupREntryPos!
-    let (_, .addEntry re) ← newChkStep (.i (.validOfImps imp ps.data)) .none
+    let (_, .addEntry re) ← newChkStep (.i (.validOfImps imp ps.toList)) .none
       | throwError "validOfImps :: Unexpected evaluation result"
     return re
 
   /-- Repeated instantiation -/
   def validOfInstantiate (v : REntry) (args : Array LamTerm) : ReifM REntry := do
     let p ← lookupREntryPos! v
-    let (_, .addEntry re) ← newChkStep (.i (.validOfInstantiate p args.data)) .none
+    let (_, .addEntry re) ← newChkStep (.i (.validOfInstantiate p args.toList)) .none
       | throwError "validOfInstantiate :: Unexpected evaluation result"
     return re
 
   def validOfInstantiateRev (v : REntry) (args : Array LamTerm) : ReifM REntry := do
     let p ← lookupREntryPos! v
-    let (_, .addEntry re) ← newChkStep (.i (.validOfInstantiateRev p args.data)) .none
+    let (_, .addEntry re) ← newChkStep (.i (.validOfInstantiateRev p args.toList)) .none
       | throwError "validOfInstantiateRev :: Unexpected evaluation result"
     return re
 
@@ -980,7 +980,7 @@ def newTypeExpr (e : Expr) : ReifM LamSort := do
 def processTypeExpr (e : Expr) : ReifM LamSort := do
   let tyVarMap ← getTyVarMap
   let e ← Reif.resolveTy e
-  if let .some idx := tyVarMap.find? e then
+  if let .some idx := tyVarMap.get? e then
     return .atom idx
   match e with
   | .sort lvl =>
@@ -1019,16 +1019,16 @@ def newTermExpr (e : Expr) : ReifM LamTerm := do
   let lamTy ← reifType eTy
   newTermExprAux e lamTy
 
-def reifMapIL : HashMap Name (LamSort → LamBaseTerm) :=
-  HashMap.ofList [
+def reifMapIL : Std.HashMap Name (LamSort → LamBaseTerm) :=
+  Std.HashMap.ofList [
     (``Eq,                .eq),
     (``Embedding.forallF, .forallE),
     (``Exists,            .existE),
     (``Bool.ite',         .ite)
   ]
 
-def reifMapConstNilLvl : HashMap Name LamTerm :=
-  HashMap.ofList [
+def reifMapConstNilLvl : Std.HashMap Name LamTerm :=
+  Std.HashMap.ofList [
     (``True,              .base .trueE),
     (``False,             .base .falseE),
     (``Not,               .base .not),
@@ -1070,8 +1070,8 @@ def reifMapConstNilLvl : HashMap Name LamTerm :=
     (``String.replace,    .base .srepall)
   ]
 
-def reifMapBVConst1 : HashMap Name (Nat → LamTerm) :=
-  HashMap.ofList [
+def reifMapBVConst1 : Std.HashMap Name (Nat → LamTerm) :=
+  Std.HashMap.ofList [
     (``BitVec.ofNat,       fun n => .base (.bvofNat n)),
     (``BitVec.toNat,       fun n => .base (.bvtoNat n)),
     (``BitVec.ofInt,       fun n => .base (.bvofInt n)),
@@ -1102,21 +1102,21 @@ def reifMapBVConst1 : HashMap Name (Nat → LamTerm) :=
     (``BitVec.rotateRight, fun n => .bvrotateRight n)
   ]
 
-def reifMapBVConst2 : HashMap Name (Nat → Nat → LamTerm) :=
-  HashMap.ofList [
+def reifMapBVConst2 : Std.HashMap Name (Nat → Nat → LamTerm) :=
+  Std.HashMap.ofList [
     (``BitVec.append,     fun n m => .base (.bvappend n m)),
     (``BitVec.replicate,  fun w i => .base (.bvrepeat w i)),
     (``BitVec.zeroExtend, fun w v => .base (.bvzeroExtend w v)),
     (``BitVec.signExtend, fun w v => .base (.bvsignExtend w v))
   ]
 
-def reifMapBVConst3 : HashMap Name (Nat → Nat → Nat → LamTerm) :=
-  HashMap.ofList [
+def reifMapBVConst3 : Std.HashMap Name (Nat → Nat → Nat → LamTerm) :=
+  Std.HashMap.ofList [
     (``BitVec.extractLsb, fun n h l => .base (.bvextract n h l))
   ]
 
-def reifMapAttributesProp : HashMap Name String :=
-  HashMap.ofList [
+def reifMapAttributesProp : Std.HashMap Name String :=
+  Std.HashMap.ofList [
     (``SMT.Attribute.trigger, "pattern")
   ]
 
@@ -1126,7 +1126,7 @@ def processSimpleLit (l : Literal) : LamTerm :=
   | .strVal s => .base (.strVal s)
 
 def processSimpleConst (name : Name) (lvls : List Level) : ReifM (Option LamTerm) := do
-  if let .some t := reifMapConstNilLvl.find? name then
+  if let .some t := reifMapConstNilLvl.get? name then
     if lvls.length != 0 then
       throwError "processSimpleConst :: ConstNilLvl constants should have nil level list"
     return t
@@ -1144,20 +1144,20 @@ def processSimpleApp (fn arg : Expr) : ReifM (Option LamTerm) := do
   let fn := fn.getAppFn
   let .const name lvls := fn
     | return .none
-  match args.data with
+  match args.toList with
   | [] => throwError "processSimpleApp :: Unexpected error"
   | [arg] =>
-    if let .some tcon := reifMapBVConst1.find? name then
+    if let .some tcon := reifMapBVConst1.get? name then
       if lvls.length != 0 then
         throwError "processSimpleApp :: BVConst1 should have nil level list"
       if let .some n ← @id (MetaM _) (Meta.evalNat arg) then
         return .some (tcon n)
       return .none
-    if let .some attrName := reifMapAttributesProp.find? name then
+    if let .some attrName := reifMapAttributesProp.get? name then
       if lvls.length != 1 then
         throwError "processSimpleApp :: Attribute should have one level"
       return .some (.base (.ocst (.smtAttr1T attrName (← reifType arg) (.base .prop))))
-    if let .some tcon := reifMapIL.find? name then
+    if let .some tcon := reifMapIL.get? name then
       if name == ``Embedding.forallF then
         let [lvl₁, lvl₂] := lvls
           | throwError "processSimpleApp :: Auto.Embedding.forallF should have two levels"
@@ -1166,7 +1166,7 @@ def processSimpleApp (fn arg : Expr) : ReifM (Option LamTerm) := do
       return .some (.base (tcon (← reifType arg)))
     return .none
   | [arg₁, arg₂] =>
-    if let .some tcon := reifMapBVConst2.find? name then
+    if let .some tcon := reifMapBVConst2.get? name then
       if lvls.length != 0 then
         throwError "processSimpleApp :: BVConst2 should have nil level list"
       match ← @id (MetaM _) (Meta.evalNat arg₁),
@@ -1175,7 +1175,7 @@ def processSimpleApp (fn arg : Expr) : ReifM (Option LamTerm) := do
       | _,       _       => return .none
     return .none
   | [arg₁, arg₂, arg₃] =>
-    if let .some tcon := reifMapBVConst3.find? name then
+    if let .some tcon := reifMapBVConst3.get? name then
       if lvls.length != 0 then
         throwError "processSimpleApp :: BVConst2 should have nil level list"
       match ← @id (MetaM _) (Meta.evalNat arg₁),
@@ -1191,8 +1191,8 @@ open LamCstrD in
   fn   : .const _ _
   arg₁ : .const _ _
 -/
-def reifMapLam0Arg2NoLit : HashMap (Name × Name) (Expr × LamTerm) :=
-  HashMap.ofList [
+def reifMapLam0Arg2NoLit : Std.HashMap (Name × Name) (Expr × LamTerm) :=
+  Std.HashMap.ofList [
     ((``NatCast.natCast, ``Int), (.const ``Int.ofNat [], .base .iofNat)),
     ((``Neg.neg, ``Int),         (.const ``Int.neg [], .base .ineg)),
     ((`Abs.abs, ``Int),          (.const ``Int.abs [], .base .iabs)),
@@ -1219,8 +1219,8 @@ open LamCstrD in
   fn   : .const _ _
   arg₁ : .app (.const _ _) natlit
 -/
-def reifMapLam0Arg2Natlit : HashMap (Name × Name) (Array ((Nat → Expr) × (Nat → LamTerm))) :=
-  HashMap.ofList [
+def reifMapLam0Arg2Natlit : Std.HashMap (Name × Name) (Array ((Nat → Expr) × (Nat → LamTerm))) :=
+  Std.HashMap.ofList [
     ((``Neg.neg, ``BitVec),
               #[(fun n => .app (.const ``BitVec.neg []) (.lit (.natVal n)), fun n => .base (.bvneg n))]),
     ((`Abs.abs, ``BitVec),
@@ -1246,8 +1246,8 @@ def reifMapLam0Arg2Natlit : HashMap (Name × Name) (Array ((Nat → Expr) × (Na
   arg₁ : .const _ _
   arg₂ : .const _ _
 -/
-def reifMapLam0Arg4NoLit : HashMap (Name × Name × Name) (Expr × LamTerm) :=
-  HashMap.ofList [
+def reifMapLam0Arg4NoLit : Std.HashMap (Name × Name × Name) (Expr × LamTerm) :=
+  Std.HashMap.ofList [
     ((``HAdd.hAdd, ``Nat, ``Nat),             (.const ``Nat.add [], .base .nadd)),
     ((``HAdd.hAdd, ``Int, ``Int),             (.const ``Int.add [], .base .iadd)),
     ((``HSub.hSub, ``Nat, ``Nat),             (.const ``Nat.sub [], .base .nsub)),
@@ -1265,8 +1265,8 @@ def reifMapLam0Arg4NoLit : HashMap (Name × Name × Name) (Expr × LamTerm) :=
   arg₂ : .app (.const _ _) natlit₂
   |- natlit₁ = natlit₂
 -/
-def reifMapLam0Arg4NatLitNatLitEq : HashMap (Name × Name) (Array ((Nat → Expr) × (Nat → LamTerm))) :=
-  HashMap.ofList [
+def reifMapLam0Arg4NatLitNatLitEq : Std.HashMap (Name × Name) (Array ((Nat → Expr) × (Nat → LamTerm))) :=
+  Std.HashMap.ofList [
     ((``HAdd.hAdd, ``BitVec),
       #[(fun n => .app (.const ``BitVec.add []) (.lit (.natVal n)), fun n => .base (.bvadd n))]),
     ((``HSub.hSub, ``BitVec),
@@ -1291,8 +1291,8 @@ open LamCstrD in
   arg₂ : .app (.const _ _) natlit₂
   |- natlit₁ ?? natlit₂
 -/
-def reifMapLam0Arg4NatLitNatLitH : HashMap (Name × Name) (Array ((Nat → Nat → Expr) × (Nat → Nat → LamTerm))) :=
-  HashMap.ofList [
+def reifMapLam0Arg4NatLitNatLitH : Std.HashMap (Name × Name) (Array ((Nat → Nat → Expr) × (Nat → Nat → LamTerm))) :=
+  Std.HashMap.ofList [
     ((``HAppend.hAppend, ``BitVec),
       #[(fun n m => mkApp2 (.const ``BitVec.append []) (.lit (.natVal n)) (.lit (.natVal m)), fun n m => .base (.bvappend n m))]),
     ((``HShiftLeft.hShiftLeft, ``BitVec),
@@ -1307,8 +1307,8 @@ def reifMapLam0Arg4NatLitNatLitH : HashMap (Name × Name) (Array ((Nat → Nat 
   arg₁ : .app (.const _ _) natlit
   arg₂ : .const _ _
 -/
-def reifMapLam0Arg4NatLit : HashMap (Name × Name) (Array ((Nat → Expr) × (Nat → LamTerm))) :=
-  HashMap.ofList [
+def reifMapLam0Arg4NatLit : Std.HashMap (Name × Name) (Array ((Nat → Expr) × (Nat → LamTerm))) :=
+  Std.HashMap.ofList [
     ((``HShiftLeft.hShiftLeft, ``BitVec),
       #[(fun n => .app (.const ``BitVec.shiftLeft []) (.lit (.natVal n)), fun n => .base (.bvshl n))]),
     ((``HShiftRight.hShiftRight, ``BitVec),
@@ -1322,14 +1322,14 @@ def processLam0Arg2 (e fn arg₁ arg₂ : Expr) : MetaM (Option LamTerm) := do
   if arg₁.isConst then
     let .const arg₁Name _ := arg₁
       | throwError "processLam0Arg2 :: Unexpected error"
-    if let .some (e', t) := reifMapLam0Arg2NoLit.find? (fnName, arg₁Name) then
+    if let .some (e', t) := reifMapLam0Arg2NoLit.get? (fnName, arg₁Name) then
       if (← Meta.isDefEqD e e') then
         return .some t
   if arg₁.isApp then
     let .app arg₁fn arg₁arg := arg₁
       | throwError "processLam0Arg2 :: Unexpected error"
     if let .const arg₁FnName _ := arg₁fn then
-      if let .some candidates := reifMapLam0Arg2Natlit.find? (fnName, arg₁FnName) then
+      if let .some candidates := reifMapLam0Arg2Natlit.get? (fnName, arg₁FnName) then
         if let .some n ← Meta.evalNat arg₁arg then
           for (e'con, tcon) in candidates do
             if (← Meta.isDefEqD e (e'con n)) then
@@ -1370,7 +1370,7 @@ def processLam0Arg4 (e fn arg₁ arg₂ arg₃ arg₄ : Expr) : MetaM (Option La
       | throwError "processLam0Arg4 :: Unexpected error"
     let .const arg₂name _ := arg₂
       | throwError "processLam0Arg4 :: Unexpected error"
-    if let .some (e', t) := reifMapLam0Arg4NoLit.find? (fnName, arg₁name, arg₂name) then
+    if let .some (e', t) := reifMapLam0Arg4NoLit.get? (fnName, arg₁name, arg₂name) then
       if (← Meta.isDefEqD e e') then
         return .some t
       return .none
@@ -1380,7 +1380,7 @@ def processLam0Arg4 (e fn arg₁ arg₂ arg₃ arg₄ : Expr) : MetaM (Option La
     if arg₁fn.isConst then
       let .const arg₁fnName _ := arg₁fn
         | throwError "processLam0Arg4 :: Unexpected error {arg₁fn}"
-      if let .some candidates := reifMapLam0Arg4NatLit.find? (fnName, arg₁fnName) then
+      if let .some candidates := reifMapLam0Arg4NatLit.get? (fnName, arg₁fnName) then
         for (e'con, tcon) in candidates do
           if let .some n ← Meta.evalNat arg₁arg then
             if (← Meta.isDefEqD e (e'con n)) then
@@ -1393,12 +1393,12 @@ def processLam0Arg4 (e fn arg₁ arg₂ arg₃ arg₄ : Expr) : MetaM (Option La
     if arg₁fn.isConst && arg₂fn.isConst then
       let .const arg₁fnName _ := arg₁fn
         | throwError "processLam0Arg4 :: Unexpected error"
-      if let .some candidates := reifMapLam0Arg4NatLitNatLitEq.find? (fnName, arg₁fnName) then
+      if let .some candidates := reifMapLam0Arg4NatLitNatLitEq.get? (fnName, arg₁fnName) then
         for (e'con, tcon) in candidates do
           if let .some n ← Meta.evalNat arg₁arg then
             if (← Meta.isDefEqD e (e'con n)) then
               return tcon n
-      if let .some candidates := reifMapLam0Arg4NatLitNatLitH.find? (fnName, arg₁fnName) then
+      if let .some candidates := reifMapLam0Arg4NatLitNatLitH.get? (fnName, arg₁fnName) then
         for (e'con, tcon) in candidates do
           match ← Meta.evalNat arg₁arg, ← Meta.evalNat arg₂arg with
           | .some n , .some m =>
@@ -1415,7 +1415,7 @@ def processComplexTermExpr (e : Expr) : MetaM (Option LamTerm) := do
   | 0 =>
     let fn := e.getAppFn
     let args := e.getAppArgs
-    match args.data with
+    match args.toList with
     | [] => return .none
     | [_] => return .none
     | [arg₁, arg₂] => processLam0Arg2 e fn arg₁ arg₂
@@ -1444,24 +1444,24 @@ where
       return res
     newTermExpr e
 
-def processTermExpr (lctx : HashMap FVarId Nat) (e : Expr) : ReifM LamTerm := do
+def processTermExpr (lctx : Std.HashMap FVarId Nat) (e : Expr) : ReifM LamTerm := do
   if let .fvar fid := e then
     if let .some n := deBruijn? lctx fid then
       return .bvar n
   let e ← Reif.resolveVal e
   let varMap ← getVarMap
   -- If the expression has already been processed
-  if let .some id := varMap.find? e then
+  if let .some id := varMap.get? e then
     return .atom id
   -- If the expression has not been processed
   processNewTermExpr e
 where
-  deBruijn? (lctx : HashMap FVarId Nat) (id : FVarId) : Option Nat :=
-    match lctx.find? id with
+  deBruijn? (lctx : Std.HashMap FVarId Nat) (id : FVarId) : Option Nat :=
+    match lctx.get? id with
     | .some n => lctx.size - 1 - n
     | .none   => none
 
-partial def reifTerm (lctx : HashMap FVarId Nat) : Expr → ReifM LamTerm
+partial def reifTerm (lctx : Std.HashMap FVarId Nat) : Expr → ReifM LamTerm
 | .app fn arg => do
   let lamFn ← reifTerm lctx fn
   let lamArg ← reifTerm lctx arg
@@ -1512,7 +1512,7 @@ def reifInd (ind : SimpleIndVal) : ReifM (Option IndInfo) := do
   let rty ← reifType type
   let rctors ← ctors.mapM (fun (e, _) => reifTermCheckType e)
   let rprojs ← projs.mapM (fun ps => ps.mapM reifTermCheckType)
-  let ret := ⟨rty, rctors.data, rprojs.bind (·.data)⟩
+  let ret := ⟨rty, rctors.toList, rprojs.bind (·.toList)⟩
   trace[auto.lamReif.printResult] "Successfully reified inductive info {← ind.zetaReduce} to {ret}"
   return .some ret
 
@@ -1522,7 +1522,7 @@ def reifMutInd (mind : Array SimpleIndVal) : ReifM (Option MutualIndInfo) := do
     let .some ii ← reifInd ind
       | return .none
     ret := ret.push ii
-  return ret.data
+  return ret.toList
 
 def reifMutInds (minds : Array (Array SimpleIndVal)) : ReifM (Array MutualIndInfo) := do
   let mut ret := #[]
@@ -1580,7 +1580,7 @@ section BuildChecker
           | throwError "buildChkStepsExpr :: Unexpected error"
         chkSteps := chkSteps.push (cs, n)
     -- `ChkMap` are run using `foldl`, so we use `BinTree.ofListFoldl`
-    let e := Lean.toExpr (BinTree.ofListFoldl chkSteps.data)
+    let e := Lean.toExpr (BinTree.ofListFoldl chkSteps.toList)
     return e
 
     -- Given a list of expression of type `ty`, construct the corresponding `BinTree`
@@ -1594,7 +1594,7 @@ section BuildChecker
   def buildTyVal : ReifM Expr := do
     let u ← getU
     -- `tyVal : List (Type u)`
-    let tyVal : List Expr := (← getTyVal).data.map (fun (e, lvl) =>
+    let tyVal : List Expr := (← getTyVal).toList.map (fun (e, lvl) =>
       Expr.app (.const ``Embedding.GLift [lvl, u]) e)
     -- `tyValExpr : Nat → Type u`
     let tyValExpr := exprListToLCtx tyVal (.succ u) (.sort (.succ u)) (.sort u)
@@ -1604,7 +1604,7 @@ section BuildChecker
   def buildVarExpr (tyValExpr : Expr) : ReifM Expr := do
     let u ← getU
     let lamSortExpr := Expr.const ``LamSort []
-    let varValPair := (← getVarVal).data
+    let varValPair := (← getVarVal).toList
     let vars ← varValPair.mapM (fun (e, s) => do
       let sExpr := toExpr s
       return Lean.mkApp3 (.const ``varSigmaMk [u]) tyValExpr sExpr (← varValInterp e s))
@@ -1616,7 +1616,7 @@ section BuildChecker
   def buildILExpr (tyValExpr : Expr) : ReifM Expr := do
     let u ← getU
     let lamSortExpr := Expr.const ``LamSort []
-    let lamILTy := (← getLamILTy).data
+    let lamILTy := (← getLamILTy).toList
     -- `ils : List ((s : LamSort) × ILLift.{u} (s.interp tyVal))`
     let ils ← lamILTy.mapM (fun s => do
       let sExpr := toExpr s
@@ -1704,8 +1704,8 @@ section BuildChecker
     printCheckerStats
     let startTime ← IO.monoMsNow
     let u ← getU
-    let lvtExpr := Lean.toExpr (BinTree.ofListGet ((← getVarVal).map Prod.snd).data)
-    let litExpr := Lean.toExpr (BinTree.ofListGet (← getLamILTy).data)
+    let lvtExpr := Lean.toExpr (BinTree.ofListGet ((← getVarVal).map Prod.snd).toList)
+    let litExpr := Lean.toExpr (BinTree.ofListGet (← getLamILTy).toList)
     let cpvExpr ← buildCPValExpr
     let cpvTy := Expr.const ``CPVal [u]
     let checker ← Meta.withLetDecl `cpval cpvTy cpvExpr fun cpvFVarExpr => do
@@ -1757,9 +1757,9 @@ section BuildChecker
     printCheckerStats
     let startTime ← IO.monoMsNow
     let u ← getU
-    let lvtExpr := Lean.toExpr (BinTree.ofListGet ((← getVarVal).map Prod.snd).data)
+    let lvtExpr := Lean.toExpr (BinTree.ofListGet ((← getVarVal).map Prod.snd).toList)
     let lvtNativeName ← mkNativeAuxDecl `lam_ssrefl_lvt (Expr.app (.const ``BinTree [.zero]) (Lean.mkConst ``LamSort)) lvtExpr
-    let litExpr := Lean.toExpr (BinTree.ofListGet (← getLamILTy).data)
+    let litExpr := Lean.toExpr (BinTree.ofListGet (← getLamILTy).toList)
     let litNativeName ← mkNativeAuxDecl `lam_ssrefl_lit (Expr.app (.const ``BinTree [.zero]) (Lean.mkConst ``LamSort)) litExpr
     let cpvExpr ← buildCPValExpr
     let cpvTy := Expr.const ``CPVal [u]
@@ -1804,16 +1804,16 @@ namespace Lam2Lam
 open Embedding.Lam LamReif
 
   structure TState where
-    typeH2lMap : HashMap Nat Nat            := {}
+    typeH2lMap : Std.HashMap Nat Nat            := {}
     -- This field should be in sync with `LamReif.State.tyVal`
     typeL2hMap : Array Nat                  := #[]
-    termH2lMap : HashMap Nat Nat            := {}
+    termH2lMap : Std.HashMap Nat Nat            := {}
     -- This field should be in sync with `LamReif.State.varVal`
     termL2hMap : Array Nat                  := #[]
-    etomH2lMap : HashMap Nat Nat            := {}
-    etomL2hMap : HashMap Nat Nat            := {}
+    etomH2lMap : Std.HashMap Nat Nat            := {}
+    etomL2hMap : Std.HashMap Nat Nat            := {}
     -- Maps from high-level chkstep to low-level chkstep
-    csH2lMap   : HashMap ChkStep ChkStep    := {}
+    csH2lMap   : Std.HashMap ChkStep ChkStep    := {}
 
   abbrev TransM := StateRefT TState ReifM
 
@@ -1833,7 +1833,7 @@ open Embedding.Lam LamReif
 
   def transTypeAtom (a : Nat) (val : Expr × Level) : TransM Nat := do
     let typeH2lMap ← getTypeH2lMap
-    match typeH2lMap.find? a with
+    match typeH2lMap.get? a with
     | .some n => return n
     | .none =>
       let idx := typeH2lMap.size
@@ -1849,7 +1849,7 @@ open Embedding.Lam LamReif
   -/
   def transTermAtom (a : Nat) (val : Expr × LamSort) : TransM Nat := do
     let termH2lMap ← getTermH2lMap
-    match termH2lMap.find? a with
+    match termH2lMap.get? a with
     | .some n => return n
     | .none =>
       let idx := termH2lMap.size
@@ -1893,7 +1893,7 @@ open Embedding.Lam LamReif
         let (cs, _) ← (lookupEtomChkStep! e).run ref
         trace[auto.buildChecker] "Collecting for etom {e} by ChkStep {cs}"
         let _ ← processChkStep ref cs
-      let .some n := (← getEtomH2lMap).find? e
+      let .some n := (← getEtomH2lMap).get? e
         | throwError "transEtom :: Cannot find translation of etom {e}"
       return n
 
@@ -1993,7 +1993,7 @@ open Embedding.Lam LamReif
       | .wfOfBetaBounded pos bound => return .wfOfBetaBounded (← transPos ref pos) bound
 
     partial def processChkStep (ref : State) (cs : ChkStep) : TransM EvalResult := do
-      if let .some cs' := (← getCsH2lMap).find? cs then
+      if let .some cs' := (← getCsH2lMap).get? cs then
         return ← LamReif.lookupChkStepResult! cs'
       let cs' ← transChkStep ref cs
       setCsH2lMap ((← getCsH2lMap).insert cs cs')
@@ -2012,7 +2012,7 @@ open Embedding.Lam LamReif
     -- Collect essential chksteps and assertions from the high-level `lam`
     --   into the low-level `lam` such that the low-level `lam` proves `re`
     partial def collectProofFor (ref : State) (hre : REntry) : TransM Unit := do
-      if let .some _ := (← getChkMap).find? hre then
+      if let .some _ := (← getChkMap).get? hre then
         return
       let (highLvlProof, _) ← (lookupREntryProof! hre).run ref
       match highLvlProof with
diff --git a/Auto/Translation/LamUtils.lean b/Auto/Translation/LamUtils.lean
index 5885c2e..840762b 100644
--- a/Auto/Translation/LamUtils.lean
+++ b/Auto/Translation/LamUtils.lean
@@ -48,24 +48,24 @@ namespace LamExportUtils
     "Import versions of polymorphic logical " ++
     "constants should have been eliminated"
 
-  def collectLamSortAtoms : LamSort → HashSet Nat
-  | .atom n => HashSet.empty.insert n
-  | .base _ => HashSet.empty
+  def collectLamSortAtoms : LamSort → Std.HashSet Nat
+  | .atom n => Std.HashSet.empty.insert n
+  | .base _ => Std.HashSet.empty
   | .func a b => (collectLamSortAtoms a).insertMany (collectLamSortAtoms b)
 
-  def collectLamSortsAtoms (ss : Array LamSort) : HashSet Nat :=
-    ss.foldl (fun hs s => hs.insertMany (collectLamSortAtoms s)) HashSet.empty
+  def collectLamSortsAtoms (ss : Array LamSort) : Std.HashSet Nat :=
+    ss.foldl (fun hs s => hs.insertMany (collectLamSortAtoms s)) Std.HashSet.empty
 
-  def collectLamSortBitVecLengths : LamSort → HashSet Nat
-  | .base (.bv n) => HashSet.empty.insert n
+  def collectLamSortBitVecLengths : LamSort → Std.HashSet Nat
+  | .base (.bv n) => Std.HashSet.empty.insert n
   | .func a b => (collectLamSortBitVecLengths a).insertMany (collectLamSortBitVecLengths b)
-  | _ => HashSet.empty
+  | _ => Std.HashSet.empty
 
-  def collectLamSortsBitVecLengths (ss : Array LamSort) : HashSet Nat :=
-    ss.foldl (fun hs s => hs.insertMany (collectLamSortBitVecLengths s)) HashSet.empty
+  def collectLamSortsBitVecLengths (ss : Array LamSort) : Std.HashSet Nat :=
+    ss.foldl (fun hs s => hs.insertMany (collectLamSortBitVecLengths s)) Std.HashSet.empty
 
   /-- Collect type atoms in a LamBaseTerm -/
-  def collectLamBaseTermAtoms (b : LamBaseTerm) : CoreM (HashSet Nat) := do
+  def collectLamBaseTermAtoms (b : LamBaseTerm) : CoreM (Std.HashSet Nat) := do
     let s? : Option LamSort ← (do
       match b with
       | .eqI _ => throwError ("collectAtoms :: " ++ exportError.ImpPolyLog)
@@ -80,7 +80,7 @@ namespace LamExportUtils
     if let .some s := s? then
       return collectLamSortAtoms s
     else
-      return HashSet.empty
+      return Std.HashSet.empty
 
   /--
     The first hashset is the type atoms
@@ -92,18 +92,18 @@ namespace LamExportUtils
       does not occur in the `LamTerm`
   -/
   def collectLamTermAtoms (lamVarTy : Array LamSort) (lamEVarTy : Array LamSort) :
-    LamTerm → CoreM (HashSet Nat × HashSet Nat × HashSet Nat)
+    LamTerm → CoreM (Std.HashSet Nat × Std.HashSet Nat × Std.HashSet Nat)
   | .atom n => do
     let .some s := lamVarTy[n]?
       | throwError "collectAtoms :: Unknown term atom {n}"
-    return (collectLamSortAtoms s, HashSet.empty.insert n, HashSet.empty)
+    return (collectLamSortAtoms s, Std.HashSet.empty.insert n, Std.HashSet.empty)
   | .etom n => do
     let .some s := lamEVarTy[n]?
       | throwError "collectAtoms :: Unknown etom {n}"
-    return (collectLamSortAtoms s, HashSet.empty, HashSet.empty.insert n)
+    return (collectLamSortAtoms s, Std.HashSet.empty, Std.HashSet.empty.insert n)
   | .base b => do
-    return (← collectLamBaseTermAtoms b, HashSet.empty, HashSet.empty)
-  | .bvar _ => pure (HashSet.empty, HashSet.empty, HashSet.empty)
+    return (← collectLamBaseTermAtoms b, Std.HashSet.empty, Std.HashSet.empty)
+  | .bvar _ => pure (Std.HashSet.empty, Std.HashSet.empty, Std.HashSet.empty)
   | .lam s t => do
     let (typeHs, termHs, etomHs) ← collectLamTermAtoms lamVarTy lamEVarTy t
     let sHs := collectLamSortAtoms s
@@ -116,56 +116,56 @@ namespace LamExportUtils
             mergeHashSet etomHs₁ etomHs₂)
 
   def collectLamTermsAtoms (lamVarTy : Array LamSort) (lamEVarTy : Array LamSort)
-    (ts : Array LamTerm) : CoreM (HashSet Nat × HashSet Nat × HashSet Nat) :=
+    (ts : Array LamTerm) : CoreM (Std.HashSet Nat × Std.HashSet Nat × Std.HashSet Nat) :=
     ts.foldlM (fun (tyHs, aHs, eHs) t => do
       let (tyHs', aHs', eHs') ← collectLamTermAtoms lamVarTy lamEVarTy t
       return (mergeHashSet tyHs tyHs', mergeHashSet aHs aHs', mergeHashSet eHs eHs'))
-      (HashSet.empty, HashSet.empty, HashSet.empty)
+      (Std.HashSet.empty, Std.HashSet.empty, Std.HashSet.empty)
 
-  def collectLamTermNatConsts : LamTerm → HashSet NatConst
-  | .base (.ncst nc) => HashSet.empty.insert nc
+  def collectLamTermNatConsts : LamTerm → Std.HashSet NatConst
+  | .base (.ncst nc) => Std.HashSet.empty.insert nc
   | .lam _ body => collectLamTermNatConsts body
   | .app _ fn arg => mergeHashSet (collectLamTermNatConsts fn) (collectLamTermNatConsts arg)
-  | _ => HashSet.empty
+  | _ => Std.HashSet.empty
 
-  def collectLamTermsNatConsts (ts : Array LamTerm) : HashSet NatConst :=
-    ts.foldl (fun hs t => mergeHashSet hs (collectLamTermNatConsts t)) HashSet.empty
+  def collectLamTermsNatConsts (ts : Array LamTerm) : Std.HashSet NatConst :=
+    ts.foldl (fun hs t => mergeHashSet hs (collectLamTermNatConsts t)) Std.HashSet.empty
 
-  def collectLamTermIntConsts : LamTerm → HashSet IntConst
-  | .base (.icst ic) => HashSet.empty.insert ic
+  def collectLamTermIntConsts : LamTerm → Std.HashSet IntConst
+  | .base (.icst ic) => Std.HashSet.empty.insert ic
   | .lam _ body => collectLamTermIntConsts body
   | .app _ fn arg => mergeHashSet (collectLamTermIntConsts fn) (collectLamTermIntConsts arg)
-  | _ => HashSet.empty
+  | _ => Std.HashSet.empty
 
-  def collectLamTermsIntConsts (ts : Array LamTerm) : HashSet IntConst :=
-    ts.foldl (fun hs t => mergeHashSet hs (collectLamTermIntConsts t)) HashSet.empty
+  def collectLamTermsIntConsts (ts : Array LamTerm) : Std.HashSet IntConst :=
+    ts.foldl (fun hs t => mergeHashSet hs (collectLamTermIntConsts t)) Std.HashSet.empty
 
-  def collectLamTermStringConsts : LamTerm → HashSet StringConst
-  | .base (.scst sc) => HashSet.empty.insert sc
+  def collectLamTermStringConsts : LamTerm → Std.HashSet StringConst
+  | .base (.scst sc) => Std.HashSet.empty.insert sc
   | .lam _ body => collectLamTermStringConsts body
   | .app _ fn arg => mergeHashSet (collectLamTermStringConsts fn) (collectLamTermStringConsts arg)
-  | _ => HashSet.empty
+  | _ => Std.HashSet.empty
 
-  def collectLamTermsStringConsts (ts : Array LamTerm) : HashSet StringConst :=
-    ts.foldl (fun hs t => mergeHashSet hs (collectLamTermStringConsts t)) HashSet.empty
+  def collectLamTermsStringConsts (ts : Array LamTerm) : Std.HashSet StringConst :=
+    ts.foldl (fun hs t => mergeHashSet hs (collectLamTermStringConsts t)) Std.HashSet.empty
 
-  def collectLamTermBitvecs : LamTerm → HashSet BitVecConst
-  | .base (.bvcst bvc) => HashSet.empty.insert bvc
+  def collectLamTermBitvecs : LamTerm → Std.HashSet BitVecConst
+  | .base (.bvcst bvc) => Std.HashSet.empty.insert bvc
   | .lam _ body => collectLamTermBitvecs body
   | .app _ fn arg => mergeHashSet (collectLamTermBitvecs fn) (collectLamTermBitvecs arg)
-  | _ => HashSet.empty
+  | _ => Std.HashSet.empty
 
-  def collectLamTermsBitvecs (ts : Array LamTerm) : HashSet BitVecConst :=
-    ts.foldl (fun hs t => mergeHashSet hs (collectLamTermBitvecs t)) HashSet.empty
+  def collectLamTermsBitvecs (ts : Array LamTerm) : Std.HashSet BitVecConst :=
+    ts.foldl (fun hs t => mergeHashSet hs (collectLamTermBitvecs t)) Std.HashSet.empty
 
-  def collectLamTermIteSorts : LamTerm → HashSet LamSort
-  | .base (.ite s) => HashSet.empty.insert s
+  def collectLamTermIteSorts : LamTerm → Std.HashSet LamSort
+  | .base (.ite s) => Std.HashSet.empty.insert s
   | .lam _ body => collectLamTermIteSorts body
   | .app _ fn arg => mergeHashSet (collectLamTermIteSorts fn) (collectLamTermIteSorts arg)
-  | _ => HashSet.empty
+  | _ => Std.HashSet.empty
 
-  def collectLamTermsIteSorts (ts : Array LamTerm) : HashSet LamSort :=
-    ts.foldl (fun hs t => mergeHashSet hs (collectLamTermIteSorts t)) HashSet.empty
+  def collectLamTermsIteSorts (ts : Array LamTerm) : Std.HashSet LamSort :=
+    ts.foldl (fun hs t => mergeHashSet hs (collectLamTermIteSorts t)) Std.HashSet.empty
 
 end LamExportUtils
 
@@ -303,16 +303,16 @@ namespace Lam2D
     Takes a `s : LamSort` and produces the `un-lifted` version of `s.interp`
       (note that `s.interp` is lifted)
   -/
-  def interpLamSortAsUnlifted (tyVal : HashMap Nat Expr) : LamSort → CoreM Expr
+  def interpLamSortAsUnlifted (tyVal : Std.HashMap Nat Expr) : LamSort → CoreM Expr
   | .atom n => do
-    let .some e := tyVal.find? n
+    let .some e := tyVal.get? n
       | throwError "interpLamSortAsUnlifted :: Cannot find fvarId assigned to type atom {n}"
     return e
   | .base b => return Lam2D.interpLamBaseSortAsUnlifted b
   | .func s₁ s₂ => do
     return .forallE `_ (← interpLamSortAsUnlifted tyVal s₁) (← interpLamSortAsUnlifted tyVal s₂) .default
 
-  def interpOtherConstAsUnlifted (tyVal : HashMap Nat Expr) (oc : OtherConst) : MetaM Expr := do
+  def interpOtherConstAsUnlifted (tyVal : Std.HashMap Nat Expr) (oc : OtherConst) : MetaM Expr := do
     let .some (.defnInfo constIdVal) := (← getEnv).find? ``constId
       | throwError "interpOtherConstAsUnlifted :: Unexpected error"
     let constIdExpr := fun params => constIdVal.value.instantiateLevelParams constIdVal.levelParams params
@@ -328,7 +328,7 @@ namespace Lam2D
         | throwError "interpOtherConstAsUnlifted :: Unexpected sort {sortterm}"
       return Lean.mkApp2 (constIdExpr [lvlattr, lvlterm]) tyattr tyterm
 
-  def interpLamBaseTermAsUnlifted (tyVal : HashMap Nat Expr) : LamBaseTerm → MetaM Expr
+  def interpLamBaseTermAsUnlifted (tyVal : Std.HashMap Nat Expr) : LamBaseTerm → MetaM Expr
   | .pcst pc    => Lam2D.interpPropConstAsUnlifted pc
   | .bcst bc    => Lam2D.interpBoolConstAsUnlifted bc
   | .ncst nc    => Lam2D.interpNatConstAsUnlifted nc
@@ -365,14 +365,14 @@ namespace Lam2D
     represent `etom`s.
   -/
   def interpLamTermAsUnlifted
-    (tyVal : HashMap Nat Expr) (varVal : HashMap Nat Expr) (etomVal : HashMap Nat Expr)
+    (tyVal : Std.HashMap Nat Expr) (varVal : Std.HashMap Nat Expr) (etomVal : Std.HashMap Nat Expr)
     (lctx : Nat) : LamTerm → MetaM Expr
   | .atom n => do
-    let .some e := varVal.find? n
+    let .some e := varVal.get? n
       | throwError "interpLamTermAsUnlifted :: Cannot find fvarId assigned to term atom {n}"
     return e
   | .etom n => do
-    let .some efvar := etomVal.find? n
+    let .some efvar := etomVal.get? n
       | throwError "interpLamSortAsUnlifted :: Cannot find fvarId assigned to etom {n}"
     return efvar
   | .base b => interpLamBaseTermAsUnlifted tyVal b
@@ -520,7 +520,7 @@ namespace Lam2D
   def lamBaseTermSimpNFList : List (Name × Expr) :=
     natConstSimpNFList ++ intConstSimpNFList ++ stringConstSimpNFList ++ bitVecConstSimpNFList
 
-  def lamBaseTermSimpNFMap : HashMap Name Expr := HashMap.ofList lamBaseTermSimpNFList
+  def lamBaseTermSimpNFMap : Std.HashMap Name Expr := Std.HashMap.ofList lamBaseTermSimpNFList
 
   section CheckDefEq
 
@@ -539,7 +539,7 @@ namespace Lam2D
   def approxSimpNF (e : Expr) : CoreM Expr := do
     let eRep := e.replace (fun sub =>
       match sub with
-      | .const name _ => lamBaseTermSimpNFMap.find? name
+      | .const name _ => lamBaseTermSimpNFMap.get? name
       | _ => .none)
     let eRep ← Core.betaReduce eRep
     let replaceNatCast (e : Expr) : Option Expr :=
diff --git a/Auto/Translation/Monomorphization.lean b/Auto/Translation/Monomorphization.lean
index f935081..89cd97e 100644
--- a/Auto/Translation/Monomorphization.lean
+++ b/Auto/Translation/Monomorphization.lean
@@ -85,7 +85,7 @@ def CiHead.ofExpr? : Expr → Option CiHead
 def CiHead.toExpr : CiHead → Expr
 | .fvar id => .fvar id
 | .mvar id => .mvar id
-| .const name lvls => .const name lvls.data
+| .const name lvls => .const name lvls.toList
 
 /-- Ignore constant's levels -/
 def CiHead.fingerPrint : CiHead → Expr
@@ -168,7 +168,7 @@ private def ConstInst.toMessageDataAux (ci : ConstInst) : MessageData :=
     let arr : Array (Option Expr) := Array.mk ((List.range narg).map (fun _ => .none))
     let arr := (ci.argsInst.zip ci.argsIdx).foldl (fun acc (arg, idx) => acc.setD idx (.some arg)) arr
     let arr := arr.map (fun e? => match e? with | .some e => m!" ({e})" | .none => m!" _")
-    MessageData.intercalate "" arr.data
+    MessageData.intercalate "" arr.toList
 
 instance : ToMessageData ConstInst where
   toMessageData ci := m!"ConstInst ⦗⦗ {ci.head}{ci.toMessageDataAux} ⦘⦘"
@@ -228,8 +228,8 @@ def ConstInst.matchExpr (e : Expr) (ci : ConstInst) : MetaM Bool := do
   · The expression does not contain level parameters in `params`
 -/
 def ConstInst.ofExpr? (params : Array Name) (bvars : Array Expr) (e : Expr) : MetaM (Option ConstInst) := do
-  let paramSet := HashSet.empty.insertMany params
-  let bvarSet := HashSet.empty.insertMany bvars
+  let paramSet := Std.HashSet.empty.insertMany params
+  let bvarSet := Std.HashSet.empty.insertMany bvars
   let fn := e.getAppFn
   -- If the head contains bound variable, then this is not
   --   a valid instance
@@ -306,7 +306,7 @@ def ConstInst.toExpr (ci : ConstInst) : MetaM Expr := do
   let mut args : Array (Option Expr) := (Array.mk (List.range nargs)).map (fun n => .none)
   for (arg, idx) in ci.argsInst.zip ci.argsIdx do
     args := args.setD idx (.some arg)
-  let .some ret := ConstInst.toExprAux args.data [] ci.head.toExpr type
+  let .some ret := ConstInst.toExprAux args.toList [] ci.head.toExpr type
     | throwError "ConstInst.toExpr :: Unexpected error"
   return ret
 
@@ -378,7 +378,7 @@ def ConstInsts.canonicalize? (cis : ConstInsts) (ci : ConstInst) : MetaM (Option
     try to match `e` and the subexpressions of `e` against `ci`.
   This function is used by `LemmaInst.matchConstInst` only
 -/
-private partial def MLemmaInst.matchConstInst (ci : ConstInst) (mi : MLemmaInst) : Expr → MetaM (HashSet LemmaInst)
+private partial def MLemmaInst.matchConstInst (ci : ConstInst) (mi : MLemmaInst) : Expr → MetaM (Std.HashSet LemmaInst)
 | .bvar _ => throwError "MLemmaInst.matchConstInst :: Loose bound variable"
 | e@(.app ..) => do
   let fn := e.getAppFn
@@ -406,14 +406,14 @@ private partial def MLemmaInst.matchConstInst (ci : ConstInst) (mi : MLemmaInst)
 | .letE .. => throwError "MLemmaInst.matchConstInst :: Let-expressions should have been reduced"
 | .mdata .. => throwError "MLemmaInst.matchConstInst :: mdata should have been consumed"
 | .proj .. => throwError "MLemmaInst.matchConstInst :: Projections should have been turned into ordinary expressions"
-| _ => return HashSet.empty
+| _ => return Std.HashSet.empty
 
 /-- Given a LemmaInst `li` and a ConstInst `ci`, try to match all subexpressions of `li` against `ci` -/
-def LemmaInst.matchConstInst (ci : ConstInst) (li : LemmaInst) : MetaM (HashSet LemmaInst) :=
+def LemmaInst.matchConstInst (ci : ConstInst) (li : LemmaInst) : MetaM (Std.HashSet LemmaInst) :=
   Meta.withNewMCtxDepth do
     let (lmvars, mvars, mi) ← MLemmaInst.ofLemmaInst li
     if lmvars.size == 0 && mvars.size == 0 then
-      return HashSet.empty
+      return Std.HashSet.empty
     MLemmaInst.matchConstInst ci mi mi.type
 
 /--
@@ -442,7 +442,7 @@ where
         | _ => false
       if hol && (← getMode) == .fol then
         return false
-      let fvarSet := HashSet.empty.insertMany fvars
+      let fvarSet := Std.HashSet.empty.insertMany fvars
       if ty.hasAnyFVar fvarSet.contains then
         return false
       leadingForallQuasiMonomorphicAux (fvars.push xid)  bodyi
@@ -500,7 +500,7 @@ def LemmaInst.monomorphic? (li : LemmaInst) : MetaM (Option LemmaInst) := do
 -/
 structure State where
   -- The `Expr` is the fingerprint of the `ConstInst`
-  ciMap    : HashMap Expr ConstInsts := {}
+  ciMap    : Std.HashMap Expr ConstInsts := {}
   -- The `Expr` is the fingerprint of the `ConstInst`
   activeCi : Std.Queue (Expr × Nat)  := Std.Queue.empty
   -- During initialization, we supply an array `lemmas` of lemmas
@@ -517,9 +517,9 @@ abbrev MonoM := StateRefT State MetaM
   2. `(ciMap.find? ci.name).getD #[]`
   3. Canonicalized ConstInst
 -/
-def CiMap.canonicalize? (ciMap : HashMap Expr ConstInsts) (ci : ConstInst) :
+def CiMap.canonicalize? (ciMap : Std.HashMap Expr ConstInsts) (ci : ConstInst) :
   MetaM (Bool × ConstInsts × ConstInst) := do
-  match ciMap.find? ci.fingerPrint with
+  match ciMap.get? ci.fingerPrint with
   | .some insts =>
     match ← insts.canonicalize? ci with
     | .some ci' => return (true, insts, ci')
@@ -570,7 +570,7 @@ def dequeueActiveCi? : MonoM (Option (Expr × Nat)) := do
   | .none => return .none
 
 def lookupActiveCi! (fgp : Expr) (idx : Nat) : MonoM ConstInst := do
-  let .some cis := (← getCiMap).find? fgp
+  let .some cis := (← getCiMap).get? fgp
     | throwError "lookupActiveCi :: Unknown CiHead {fgp}"
   let .some ci := cis[idx]?
     | throwError "lookupActiveCi :: Index {idx} out of bound"
@@ -656,25 +656,25 @@ namespace FVarRep
     bfvars   : Array FVarId             := #[]
     -- Free variables representing abstracted expressions
     ffvars   : Array FVarId             := #[]
-    exprMap  : HashMap Expr FVarId      := {}
-    ciMap    : HashMap Expr ConstInsts
-    ciIdMap  : HashMap ConstInst FVarId := {}
+    exprMap  : Std.HashMap Expr FVarId      := {}
+    ciMap    : Std.HashMap Expr ConstInsts
+    ciIdMap  : Std.HashMap ConstInst FVarId := {}
     -- Inverse of `ciIdMap`
-    idCiMap  : HashMap FVarId ConstInst := {}
+    idCiMap  : Std.HashMap FVarId ConstInst := {}
     -- Canonicalization map for types
-    tyCanMap : HashMap Expr Expr        := {}
+    tyCanMap : Std.HashMap Expr Expr        := {}
 
   abbrev FVarRepM := StateRefT State MetaState.MetaStateM
 
   #genMonadState FVarRepM
 
-  def getBfvarSet : FVarRepM (HashSet FVarId) := do
+  def getBfvarSet : FVarRepM (Std.HashSet FVarId) := do
     let bfvars ← getBfvars
-    return HashSet.empty.insertMany bfvars
+    return Std.HashSet.empty.insertMany bfvars
 
-  def getFfvarSet : FVarRepM (HashSet FVarId) := do
+  def getFfvarSet : FVarRepM (Std.HashSet FVarId) := do
     let ffvars ← getFfvars
-    return HashSet.empty.insertMany ffvars
+    return Std.HashSet.empty.insertMany ffvars
 
   /-- Similar to `Monomorphization.processConstInst` -/
   def processConstInst (ci : ConstInst) : FVarRepM Unit := do
@@ -722,7 +722,7 @@ namespace FVarRep
       | (true, _, ci') => return ci'
       | _ => throwError "constInst2FVarId :: Cannot find canonicalized instance of {ci}")
     let ciIdMap ← FVarRep.getCiIdMap
-    match ciIdMap.find? ci with
+    match ciIdMap.get? ci with
     | .some fid => return fid
     | .none => do
       let userName := (`cifvar).appendIndexAfter (← getCiIdMap).size
@@ -943,7 +943,7 @@ where
     let (inductiveVals, s) ← (fvarRepMInductAction inductiveVals).run s
     let exlis := s.exprMap.toList.map (fun (e, id) => (id, e))
     let cilis ← s.ciIdMap.toList.mapM (fun (ci, id) => do return (id, ← MetaState.runMetaM ci.toExpr))
-    let polyVal := HashMap.ofList (exlis ++ cilis)
+    let polyVal := Std.HashMap.ofList (exlis ++ cilis)
     return (s.ffvars, Reif.State.mk uvalids polyVal s.tyCanMap inhs inductiveVals none)
   fvarRepMFactAction (lis : Array LemmaInst) : FVarRep.FVarRepM (Array UMonoFact) := lis.filterMapM (fun li => do
     let liTypeRep? ← FVarRep.replacePolyWithFVar li.type
diff --git a/Auto/Translation/Preprocessing.lean b/Auto/Translation/Preprocessing.lean
index e567af8..b2430e9 100644
--- a/Auto/Translation/Preprocessing.lean
+++ b/Auto/Translation/Preprocessing.lean
@@ -99,28 +99,28 @@ def getConstUnfoldInfo (name : Name) : MetaM ConstUnfoldInfo := do
   If there is cyclic dependency, `topoSortUnfolds` throws an error
 -/
 partial def topoSortUnfolds (unfolds : Array ConstUnfoldInfo) : MetaM (Array ConstUnfoldInfo) := do
-  let mut depMap : HashMap Name (HashSet Name) := {}
+  let mut depMap : Std.HashMap Name (Std.HashSet Name) := {}
   for ⟨i, val, _⟩ in unfolds do
     for ⟨j, _, _⟩ in unfolds do
       if (val.find? (fun e => e.constName? == .some j)).isSome then
-        let deps := (depMap.find? i).getD {}
+        let deps := (depMap.get? i).getD {}
         depMap := depMap.insert i (deps.insert j)
   let (_, _, nameArr) ← (unfolds.mapM (fun n => go depMap {} n.name)).run ({}, #[])
-  let nameMap : HashMap Name _ := HashMap.ofList (unfolds.data.map (fun ui => (ui.name, ui)))
+  let nameMap : Std.HashMap Name _ := Std.HashMap.ofList (unfolds.toList.map (fun ui => (ui.name, ui)))
   let mut ret := #[]
   for name in nameArr do
-    let .some ui := nameMap.find? name
+    let .some ui := nameMap.get? name
       | throwError "topoSortUnfolds :: Unexpected error"
     ret := ret.push ui
   return ret.reverse
 where
-  go (depMap : HashMap Name (HashSet Name)) (stack : HashSet Name) (n : Name) : StateRefT (HashSet Name × Array Name) MetaM Unit := do
+  go (depMap : Std.HashMap Name (Std.HashSet Name)) (stack : Std.HashSet Name) (n : Name) : StateRefT (Std.HashSet Name × Array Name) MetaM Unit := do
     if stack.contains n then
       throwError "topoSortUnfolds :: Cyclic dependency"
     let (done, ret) ← get
     if done.contains n then
       return
-    let deps := (depMap.find? n).getD {}
+    let deps := (depMap.get? n).getD {}
     set (done.insert n, ret)
     for dep in deps do
       go depMap (stack.insert n) dep
@@ -139,7 +139,7 @@ def unfoldConsts (unfolds : Array Prep.ConstUnfoldInfo) (e : Expr) : Expr := Id.
       match e with
       | .const name lvls =>
         if name == uiname then
-          val.instantiateLevelParams params.data lvls
+          val.instantiateLevelParams params.toList lvls
         else
           .none
       | _ => .none)
diff --git a/Auto/Translation/Reduction.lean b/Auto/Translation/Reduction.lean
index c7e6869..7bc758d 100644
--- a/Auto/Translation/Reduction.lean
+++ b/Auto/Translation/Reduction.lean
@@ -32,9 +32,9 @@ def unfoldProj (e : Expr) : MetaM Expr :=
       | throwError s!"unfoldProj :: {name} is not a inductive type"
     let some structInfo := getStructureInfo? (← getEnv) name
       | throwError s!"unfoldProj :: {name} is not a structure"
-    let nameMap : HashMap Name StructureFieldInfo := HashMap.ofList
-      (structInfo.fieldInfo.map (fun sfi => (sfi.fieldName, sfi))).data
-    let sorted := structInfo.fieldNames.map (fun name => nameMap.find? name)
+    let nameMap : Std.HashMap Name StructureFieldInfo := Std.HashMap.ofList
+      (structInfo.fieldInfo.map (fun sfi => (sfi.fieldName, sfi))).toList
+    let sorted := structInfo.fieldNames.map (fun name => nameMap.get? name)
     let .some (.some sfi) := sorted[idx]?
       | throwError s!"unfoldProj :: Projection index out of bound"
     let nones : List (Option Expr) := (List.range indi.numParams).map (fun _ => .none)
@@ -78,4 +78,4 @@ def prepReduceDefeq (type : Expr) : MetaM (Option Expr) := do
     let eq' := Lean.mkApp3 (.const ``Eq lvls) ty lhs rhs
     return .some (← mkForallFVars xs eq')
 
-end Auto
\ No newline at end of file
+end Auto
diff --git a/Auto/Translation/ReifM.lean b/Auto/Translation/ReifM.lean
index 1ed5796..e5256ce 100644
--- a/Auto/Translation/ReifM.lean
+++ b/Auto/Translation/ReifM.lean
@@ -16,9 +16,9 @@ structure State where
   -- During monomorphization, constants will be turned
   --   into free variables. This map records the original expression
   --   corresponding to these free variables.
-  exprFVarVal     : HashMap FVarId Expr := {}
+  exprFVarVal     : Std.HashMap FVarId Expr := {}
   -- Canonicalization map for types
-  tyCanMap        : HashMap Expr Expr   := {}
+  tyCanMap        : Std.HashMap Expr Expr   := {}
   -- Inhabited canonicalized types
   -- The second `Expr` should be of the form `ty₁ → ty₂ → ⋯ → tyₙ`,
   --   where `ty₁, ty₂, ⋯, tyₙ` are canonicalized types within `tyCanMap`
@@ -36,11 +36,11 @@ abbrev ReifM := StateT State MetaM
 -/
 @[inline] def resolveVal (e : Expr) : ReifM Expr :=
   match e with
-  | .fvar id => do return ((← getExprFVarVal).find? id).getD e
+  | .fvar id => do return ((← getExprFVarVal).get? id).getD e
   | _ => return e
 
 @[inline] def resolveTy (e : Expr) : ReifM Expr := do
-  match (← getTyCanMap).find? (Expr.eraseMData e) with
+  match (← getTyCanMap).get? (Expr.eraseMData e) with
   | .some id => return id
   | .none => throwError "resolveTy :: Unable to resolve {e}"
 
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