fix small issues

Auto/Parser/NDFA.lean

@@ -336,8 +336,8 @@ section NFA
     hash c := hash c.val
 
   def test₁ : NFA String := ⟨#[
-      HashMap.ofList [(.inr "a", #[5]), (.inr "b", #[1, 0])],
-      HashMap.ofList [(.inl .unit, #[1]), (.inr "c", #[2, 4]), (.inr "a", #[6,1,2])]
+      Std.HashMap.ofList [(.inr "a", #[5]), (.inr "b", #[1, 0])],
+      Std.HashMap.ofList [(.inl .unit, #[1]), (.inr "c", #[2, 4]), (.inr "a", #[6,1,2])]
     ], #[]⟩
 
   def test₂ : NFA String := test₁.normalize
@@ -474,8 +474,8 @@ section DFA
   /-
 
   def test₄ : DFA String := ⟨HashSet.empty.insert 3, #[
-    HashMap.ofList [("a", 5), ("b", 0)],
-    HashMap.ofList [("q", 1), ("c", 4), ("a", 2)]], #[.empty, .empty]⟩
+    Std.HashMap.ofList [("a", 5), ("b", 0)],
+    Std.HashMap.ofList [("q", 1), ("c", 4), ("a", 2)]], #[.empty, .empty]⟩
 
   local instance : Hashable Char where
     hash c := hash c.val

Auto/Tactic.lean

@@ -160,7 +160,7 @@ def collectUserLemmas (terms : Array Term) : TacticM (Array Lemma) :=
     return lemmas
 
 def collectHintDBLemmas (names : Array Name) : TacticM (Array Lemma) := do
-  let mut hs : HashSet Name := HashSet.empty
+  let mut hs : Std.HashSet Name := Std.HashSet.empty
   let mut ret : Array Lemma := #[]
   for name in names do
     let .some db ← findLemDB name

Auto/Translation/Assumptions.lean

@@ -101,7 +101,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 := #[]