fix test

src/Lean/Compiler/LCNF/FloatLetIn.lean

@@ -117,7 +117,7 @@ up to this point, with respect to `cs`. The initial decisions are:
 - `unknown` otherwise
 -/
 def initialDecisions (cs : Cases) : BaseFloatM (Std.HashMap FVarId Decision) := do
-  let mut map := Std.HashMap.empty (← read).decls.length
+  let mut map := Std.HashMap.emptyWithCapacity (← read).decls.length
   let folder val acc := do
     if let .let decl := val then
       if (← ignore? decl) then
@@ -148,7 +148,7 @@ Compute the initial new arms. This will just set up a map from all arms of
 `cs` to empty `Array`s, plus one additional entry for `dont`.
 -/
 def initialNewArms (cs : Cases) : Std.HashMap Decision (List CodeDecl) := Id.run do
-  let mut map := Std.HashMap.empty (cs.alts.size + 1)
+  let mut map := Std.HashMap.emptyWithCapacity (cs.alts.size + 1)
   map := map.insert .dont []
   cs.alts.foldr (init := map) fun val acc => acc.insert (.ofAlt val) []
 

src/Lean/Compiler/LCNF/JoinPoints.lean

@@ -39,12 +39,12 @@ structure FindState where
   /--
   All current join point candidates accessible by their `FVarId`.
   -/
-  candidates : Std.HashMap FVarId CandidateInfo := .empty
+  candidates : Std.HashMap FVarId CandidateInfo := ∅
   /--
   The `FVarId`s of all `fun` declarations that were declared within the
   current `fun`.
   -/
-  scope : Std.HashSet FVarId := .empty
+  scope : Std.HashSet FVarId := ∅
 
 abbrev ReplaceCtx := Std.HashMap FVarId Name
 
@@ -88,7 +88,7 @@ private partial def removeCandidatesInLetValue (e : LetValue) : FindM Unit := do
 Add a new join point candidate to the state.
 -/
 private def addCandidate (fvarId : FVarId) (arity : Nat) : FindM Unit := do
-  let cinfo := { arity, associated := .empty }
+  let cinfo := { arity, associated := ∅ }
   modifyCandidates (fun cs => cs.insert fvarId cinfo )
 
 /--
@@ -177,7 +177,7 @@ and all calls to them with `jmp`s.
 -/
 partial def replace (decl : Decl) (state : FindState) : CompilerM Decl := do
   let mapper := fun acc cname _ => do return acc.insert cname (← mkFreshJpName)
-  let replaceCtx : ReplaceCtx ← state.candidates.foldM (init := .empty) mapper
+  let replaceCtx : ReplaceCtx ← state.candidates.foldM (init := ∅) mapper
   let newValue ← decl.value.mapCodeM go |>.run replaceCtx
   return { decl with value := newValue }
 where

src/Lean/Compiler/LCNF/Probing.lean

@@ -30,7 +30,7 @@ def sortedBySize : Probe Decl (Nat × Decl) := fun decls =>
     if sz₁ == sz₂ then Name.lt decl₁.name decl₂.name else sz₁ < sz₂
 
 def countUnique [ToString α] [BEq α] [Hashable α] : Probe α (α × Nat) := fun data => do
-  let mut map := Std.HashMap.empty
+  let mut map := Std.HashMap.emptyWithCapacity data.size
   for d in data do
     if let some count := map[d]? then
       map := map.insert d (count + 1)

src/Lean/Data/NameMap.lean

@@ -81,7 +81,7 @@ end NameSSet
 def NameHashSet := Std.HashSet Name
 
 namespace NameHashSet
-@[inline] def empty : NameHashSet := Std.HashSet.empty
+@[inline] def empty : NameHashSet := (∅ : Std.HashSet Name)
 instance : EmptyCollection NameHashSet := ⟨empty⟩
 instance : Inhabited NameHashSet := ⟨{}⟩
 def insert (s : NameHashSet) (n : Name) := Std.HashSet.insert s n

src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Basic.lean

@@ -116,7 +116,7 @@ def markUninterestingConst (n : Name) : PreProcessM Unit := do
 @[inline]
 def run (cfg : BVDecideConfig) (goal : MVarId) (x : PreProcessM α) : MetaM α := do
   let hyps ← goal.withContext do getPropHyps
-  ReaderT.run x cfg |>.run' { rewriteCache := Std.HashSet.empty hyps.size }
+  ReaderT.run x cfg |>.run' { rewriteCache := Std.HashSet.emptyWithCapacity hyps.size }
 
 end PreProcessM
 

src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/IntToBitVec.lean

@@ -122,7 +122,7 @@ where
               let argTypes := relevantTerms.map (fun _ => (`x, argType))
               let innerMotiveType ←
                 withLocalDeclsDND argTypes fun args => do
-                  let mut subst : Std.HashMap Expr Expr := Std.HashMap.empty (args.size + 1)
+                  let mut subst : Std.HashMap Expr Expr := Std.HashMap.emptyWithCapacity (args.size + 1)
                   subst := subst.insert (mkConst ``System.Platform.numBits) z
                   for term in relevantTerms, arg in args do
                     subst := subst.insert term arg

src/Lean/Elab/Tactic/Omega/OmegaM.lean

@@ -73,7 +73,7 @@ abbrev OmegaM := StateRefT Cache OmegaM'
 
 /-- Run a computation in the `OmegaM` monad, starting with no recorded atoms. -/
 def OmegaM.run (m : OmegaM α) (cfg : OmegaConfig) : MetaM α :=
-  m.run' Std.HashMap.empty |>.run' {} { cfg } |>.run'
+  m.run' (∅ : Std.HashMap ..) |>.run' {} { cfg } |>.run'
 
 /-- Retrieve the user-specified configuration options. -/
 def cfg : OmegaM OmegaConfig := do pure (← read).cfg
@@ -168,7 +168,7 @@ def analyzeAtom (e : Expr) : OmegaM (Std.HashSet Expr) := do
   match e.getAppFnArgs with
   | (``Nat.cast, #[.const ``Int [], _, e']) =>
     -- Casts of natural numbers are non-negative.
-    let mut r := Std.HashSet.empty.insert (Expr.app (.const ``Int.ofNat_nonneg []) e')
+    let mut r := (∅ : Std.HashSet Expr).insert (Expr.app (.const ``Int.ofNat_nonneg []) e')
     match (← cfg).splitNatSub, e'.getAppFnArgs with
       | true, (``HSub.hSub, #[_, _, _, _, a, b]) =>
         -- `((a - b : Nat) : Int)` gives a dichotomy
@@ -190,7 +190,7 @@ def analyzeAtom (e : Expr) : OmegaM (Std.HashSet Expr) := do
       let ne_zero := mkApp3 (.const ``Ne [1]) (.const ``Int []) k (toExpr (0 : Int))
       let pos := mkApp4 (.const ``LT.lt [0]) (.const ``Int []) (.const ``Int.instLTInt [])
         (toExpr (0 : Int)) k
-      pure <| Std.HashSet.empty.insert
+      pure <| (∅ : Std.HashSet Expr).insert
         (mkApp3 (.const ``Int.mul_ediv_self_le []) x k (← mkDecideProof ne_zero)) |>.insert
           (mkApp3 (.const ``Int.lt_mul_ediv_self_add []) x k (← mkDecideProof pos))
   | (``HMod.hMod, #[_, _, _, _, x, k]) =>
@@ -202,7 +202,7 @@ def analyzeAtom (e : Expr) : OmegaM (Std.HashSet Expr) := do
         let b_pos := mkApp4 (.const ``LT.lt [0]) (.const ``Int []) (.const ``Int.instLTInt [])
           (toExpr (0 : Int)) b
         let pow_pos := mkApp3 (.const ``Lean.Omega.Int.pos_pow_of_pos []) b exp (← mkDecideProof b_pos)
-        pure <| Std.HashSet.empty.insert
+        pure <| (∅ : Std.HashSet Expr).insert
           (mkApp3 (.const ``Int.emod_nonneg []) x k
               (mkApp3 (.const ``Int.ne_of_gt []) k (toExpr (0 : Int)) pow_pos)) |>.insert
             (mkApp3 (.const ``Int.emod_lt_of_pos []) x k pow_pos)
@@ -216,7 +216,7 @@ def analyzeAtom (e : Expr) : OmegaM (Std.HashSet Expr) := do
             (toExpr (0 : Nat)) b
           let pow_pos := mkApp3 (.const ``Nat.pos_pow_of_pos []) b exp (← mkDecideProof b_pos)
           let cast_pos := mkApp2 (.const ``Int.ofNat_pos_of_pos []) k' pow_pos
-          pure <| Std.HashSet.empty.insert
+          pure <| (∅ : Std.HashSet Expr).insert
             (mkApp3 (.const ``Int.emod_nonneg []) x k
                 (mkApp3 (.const ``Int.ne_of_gt []) k (toExpr (0 : Int)) cast_pos)) |>.insert
               (mkApp3 (.const ``Int.emod_lt_of_pos []) x k cast_pos)
@@ -224,18 +224,18 @@ def analyzeAtom (e : Expr) : OmegaM (Std.HashSet Expr) := do
         | (``Nat.cast, #[.const ``Int [], _, x']) =>
           -- Since we push coercions inside `%`, we need to record here that
           -- `(x : Int) % (y : Int)` is non-negative.
-          pure <| Std.HashSet.empty.insert (mkApp2 (.const ``Int.emod_ofNat_nonneg []) x' k)
+          pure <| (∅ : Std.HashSet Expr).insert (mkApp2 (.const ``Int.emod_ofNat_nonneg []) x' k)
         | _ => pure ∅
     | _ => pure ∅
   | (``Min.min, #[_, _, x, y]) =>
-    pure <| Std.HashSet.empty.insert (mkApp2 (.const ``Int.min_le_left []) x y) |>.insert
+    pure <| (∅ : Std.HashSet Expr).insert (mkApp2 (.const ``Int.min_le_left []) x y) |>.insert
       (mkApp2 (.const ``Int.min_le_right []) x y)
   | (``Max.max, #[_, _, x, y]) =>
-    pure <| Std.HashSet.empty.insert (mkApp2 (.const ``Int.le_max_left []) x y) |>.insert
+    pure <| (∅ : Std.HashSet Expr).insert (mkApp2 (.const ``Int.le_max_left []) x y) |>.insert
       (mkApp2 (.const ``Int.le_max_right []) x y)
   | (``ite, #[α, i, dec, t, e]) =>
       if α == (.const ``Int []) then
-        pure <| Std.HashSet.empty.insert <| mkApp5 (.const ``ite_disjunction [0]) α i dec t e
+        pure <| (∅ : Std.HashSet Expr).insert <| mkApp5 (.const ``ite_disjunction [0]) α i dec t e
       else
         pure {}
   | _ => pure ∅

src/Lean/Environment.lean

@@ -1767,8 +1767,8 @@ def finalizeImport (s : ImportState) (imports : Array Import) (opts : Options) (
     (leakEnv := false) : IO Environment := do
   let numConsts := s.moduleData.foldl (init := 0) fun numConsts mod =>
     numConsts + mod.constants.size + mod.extraConstNames.size
-  let mut const2ModIdx : Std.HashMap Name ModuleIdx := Std.HashMap.empty (capacity := numConsts)
-  let mut constantMap : Std.HashMap Name ConstantInfo := Std.HashMap.empty (capacity := numConsts)
+  let mut const2ModIdx : Std.HashMap Name ModuleIdx := Std.HashMap.emptyWithCapacity (capacity := numConsts)
+  let mut constantMap : Std.HashMap Name ConstantInfo := Std.HashMap.emptyWithCapacity (capacity := numConsts)
   for h : modIdx in [0:s.moduleData.size] do
     let mod := s.moduleData[modIdx]
     for cname in mod.constNames, cinfo in mod.constants do

src/Lean/Linter/UnusedVariables.lean

@@ -364,17 +364,17 @@ structure References where
   the spans for `foo`, `bar`, and `baz`. Global definitions are always treated as used.
   (It would be nice to be able to detect unused global definitions but this requires more
   information than the linter framework can provide.) -/
-  constDecls : Std.HashSet String.Range := .empty
+  constDecls : Std.HashSet String.Range := ∅
   /-- The collection of all local declarations, organized by the span of the declaration.
   We collapse all declarations declared at the same position into a single record using
   `FVarDefinition.aliases`. -/
-  fvarDefs : Std.HashMap String.Range FVarDefinition := .empty
+  fvarDefs : Std.HashMap String.Range FVarDefinition := ∅
   /-- The set of `FVarId`s that are used directly. These may or may not be aliases. -/
-  fvarUses : Std.HashSet FVarId := .empty
+  fvarUses : Std.HashSet FVarId := ∅
   /-- A mapping from alias to original FVarId. We don't guarantee that the value is not itself
   an alias, but we use `followAliases` when adding new elements to try to avoid long chains. -/
   -- TODO: use a `UnionFind` data structure here
-  fvarAliases : Std.HashMap FVarId FVarId := .empty
+  fvarAliases : Std.HashMap FVarId FVarId := ∅
   /-- Collection of all `MetavarContext`s following the execution of a tactic. We trawl these
   if needed to find additional `fvarUses`. -/
   assignments : Array (PersistentHashMap MVarId Expr) := #[]

src/Lean/Meta/Canonicalizer.lean

@@ -49,7 +49,7 @@ State for the `CanonM` monad.
 structure State where
   /-- Mapping from `Expr` to hash. -/
   -- We use `HashMap.Raw` to ensure we don't have to tag `State` as `unsafe`.
-  cache      : Std.HashMap.Raw ExprVisited UInt64 := Std.HashMap.Raw.empty
+  cache      : Std.HashMap.Raw ExprVisited UInt64 := ∅
   /--
   Given a hashcode `k` and `keyToExprs.find? h = some es`, we have that all `es` have hashcode `k`, and
   are not definitionally equal modulo the transparency setting used. -/

src/Lean/Meta/Tactic/AC/Main.lean

@@ -66,9 +66,9 @@ inductive PreExpr
 def toACExpr (op l r : Expr) : MetaM (Array Expr × ACExpr) := do
   let (preExpr, vars) ←
     toPreExpr (mkApp2 op l r)
-    |>.run Std.HashSet.empty
+    |>.run ∅
   let vars := vars.toArray.insertionSort Expr.lt
-  let varMap := vars.foldl (fun xs x => xs.insert x xs.size) Std.HashMap.empty |>.get!
+  let varMap := vars.foldl (fun xs x => xs.insert x xs.size) (∅ : Std.HashMap Expr Nat) |>.get!
 
   return (vars, toACExpr varMap preExpr)
   where

src/Lean/Namespace.lean

@@ -20,7 +20,7 @@ builtin_initialize namespacesExt : SimplePersistentEnvExtension Name NameSSet
       6.18% of the runtime is here. It was 9.31% before the `HashMap` optimization.
       -/
       let capacity := as.foldl (init := 0) fun r e => r + e.size
-      let map : Std.HashMap Name Unit := Std.HashMap.empty capacity
+      let map : Std.HashMap Name Unit := Std.HashMap.emptyWithCapacity capacity
       let map := mkStateFromImportedEntries (fun map name => map.insert name ()) map as
       SMap.fromHashMap map |>.switch
     addEntryFn      := fun s n => s.insert n

src/Lean/Server/References.lean

@@ -263,7 +263,7 @@ all identifiers that are being collapsed into one.
 -/
 partial def combineIdents (trees : Array InfoTree) (refs : Array Reference) : Array Reference := Id.run do
   -- Deduplicate definitions based on their exact range
-  let mut posMap : Std.HashMap Lsp.Range RefIdent := Std.HashMap.empty
+  let mut posMap : Std.HashMap Lsp.Range RefIdent := ∅
   for ref in refs do
     if let { ident, range, isBinder := true, .. } := ref then
       posMap := posMap.insert range ident
@@ -318,7 +318,7 @@ where
       canonicalRepresentative := idMap[canonicalRepresentative]
     return canonicalRepresentative
 
-  buildIdMap posMap := Id.run <| StateT.run' (s := Std.HashMap.empty) do
+  buildIdMap posMap := Id.run <| StateT.run' (s := ∅) do
     -- map fvar defs to overlapping fvar defs/uses
     for ref in refs do
       let baseId := ref.ident
@@ -348,7 +348,7 @@ are added to the `aliases` of the representative of the group.
 Yields to separate groups for declaration and usages if `allowSimultaneousBinderUse` is set.
 -/
 def dedupReferences (refs : Array Reference) (allowSimultaneousBinderUse := false) : Array Reference := Id.run do
-  let mut refsByIdAndRange : Std.HashMap (RefIdent × Option Bool × Lsp.Range) Reference := Std.HashMap.empty
+  let mut refsByIdAndRange : Std.HashMap (RefIdent × Option Bool × Lsp.Range) Reference := ∅
   for ref in refs do
     let isBinder := if allowSimultaneousBinderUse then some ref.isBinder else none
     let key := (ref.ident, isBinder, ref.range)

src/Lean/Util/Diff.lean

@@ -133,7 +133,7 @@ cautious when applying it to larger workloads.
 partial def lcs (left right : Subarray α) : Array α := Id.run do
   let (pref, left, right) := matchPrefix left right
   let (left, right, suff) := matchSuffix left right
-  let mut hist : Histogram α left.size right.size := .empty
+  let mut hist : Histogram α left.size right.size := (∅ : Std.HashMap ..)
   for h : i in [0:left.size] do
     hist := hist.addLeft ⟨i, Membership.get_elem_helper h rfl⟩ left[i]
   for h : i in [0:right.size] do

src/Lean/Util/HasConstCache.lean

@@ -10,7 +10,7 @@ import Std.Data.HashMap.Raw
 namespace Lean
 
 structure HasConstCache (declNames : Array Name) where
-  cache : Std.HashMap.Raw Expr Bool := Std.HashMap.Raw.empty
+  cache : Std.HashMap.Raw Expr Bool := ∅
 
 unsafe def HasConstCache.containsUnsafe (e : Expr) : StateM (HasConstCache declNames) Bool := do
   if let some r := (← get).cache.get? (beq := ⟨ptrEq⟩) e then

src/Lean/Util/MonadCache.lean

@@ -68,7 +68,7 @@ instance  : MonadHashMapCacheAdapter α β (MonadCacheT α β m) where
   modifyCache f := (modify f : StateRefT' ..)
 
 @[inline] def run {σ} (x : MonadCacheT α β m σ) : m σ :=
-  x.run' Std.HashMap.empty
+  x.run' ∅
 
 instance : Monad (MonadCacheT α β m) := inferInstanceAs (Monad (StateRefT' _ _ _))
 instance : MonadLift m (MonadCacheT α β m) := inferInstanceAs (MonadLift m (StateRefT' _ _ _))
@@ -92,7 +92,7 @@ instance  : MonadHashMapCacheAdapter α β (MonadStateCacheT α β m) where
   modifyCache f := (modify f : StateT ..)
 
 @[always_inline, inline] def run {σ} (x : MonadStateCacheT α β m σ) : m σ :=
-  x.run' Std.HashMap.empty
+  x.run' ∅
 
 instance : Monad (MonadStateCacheT α β m) := inferInstanceAs (Monad (StateT _ _))
 instance : MonadLift m (MonadStateCacheT α β m) := inferInstanceAs (MonadLift m (StateT _ _))

src/Lean/Util/PtrSet.lean

@@ -28,7 +28,7 @@ unsafe def PtrSet (α : Type) :=
   Std.HashSet (Ptr α)
 
 unsafe def mkPtrSet {α : Type} (capacity : Nat := 64) : PtrSet α :=
-  Std.HashSet.empty capacity
+  Std.HashSet.emptyWithCapacity capacity
 
 unsafe abbrev PtrSet.insert (s : PtrSet α) (a : α) : PtrSet α :=
   Std.HashSet.insert s { value := a }
@@ -43,7 +43,7 @@ unsafe def PtrMap (α : Type) (β : Type) :=
   Std.HashMap (Ptr α) β
 
 unsafe def mkPtrMap {α β : Type} (capacity : Nat := 64) : PtrMap α β :=
-  Std.HashMap.empty capacity
+  Std.HashMap.emptyWithCapacity capacity
 
 unsafe abbrev PtrMap.insert (s : PtrMap α β) (a : α) (b : β) : PtrMap α β :=
   Std.HashMap.insert s { value := a } b

src/Lean/Util/ShareCommon.lean

@@ -15,8 +15,8 @@ namespace Lean.ShareCommon
 
 def objectFactory :=
   StateFactory.mk {
-    Map := Std.HashMap, mkMap := (Std.HashMap.empty ·), mapFind? := (·.get?), mapInsert := (·.insert)
-    Set := Std.HashSet, mkSet := (Std.HashSet.empty ·), setFind? := (·.get?), setInsert := (·.insert)
+    Map := Std.HashMap, mkMap := (Std.HashMap.emptyWithCapacity ·), mapFind? := (·.get?), mapInsert := (·.insert)
+    Set := Std.HashSet, mkSet := (Std.HashSet.emptyWithCapacity ·), setFind? := (·.get?), setInsert := (·.insert)
   }
 
 def persistentObjectFactory :=

src/Lean/Util/SortExprs.lean

@@ -20,7 +20,7 @@ def sortExprs (es : Array Expr) (lt := true) : Array Expr × Perm :=
     es.qsort fun (e₁, _) (e₂, _) => e₁.lt e₂
   else
     es.qsort fun (e₁, _) (e₂, _) => e₂.lt e₁
-  let (_, perm) := es.foldl (init := (0, Std.HashMap.empty)) fun (i, perm) (_, j) => (i+1, perm.insert j i)
+  let (_, perm) := es.foldl (init := (0, ∅)) fun (i, perm) (_, j) => (i+1, perm.insert j i)
   let es := es.map (·.1)
   (es, perm)
 

src/Std/Data/DHashMap/Basic.lean

@@ -62,11 +62,14 @@ def DHashMap (α : Type u) (β : α → Type v) [BEq α] [Hashable α] := { m :
 
 namespace DHashMap
 
-@[inline, inherit_doc Raw.empty] def empty [BEq α] [Hashable α] (capacity := 8) : DHashMap α β :=
-  ⟨Raw.empty capacity, .empty₀⟩
+@[inline, inherit_doc Raw.emptyWithCapacity] def emptyWithCapacity [BEq α] [Hashable α] (capacity := 8) : DHashMap α β :=
+  ⟨Raw.emptyWithCapacity capacity, .emptyWithCapacity₀⟩
+
+@[deprecated emptyWithCapacity (since := "2025-03-12"), inherit_doc emptyWithCapacity]
+abbrev empty := @emptyWithCapacity
 
 instance [BEq α] [Hashable α] : EmptyCollection (DHashMap α β) where
-  emptyCollection := empty
+  emptyCollection := emptyWithCapacity
 
 instance [BEq α] [Hashable α] : Inhabited (DHashMap α β) where
   default := ∅
@@ -82,7 +85,7 @@ structure Equiv (m₁ m₂ : DHashMap α β) where
     (b : β a) : DHashMap α β :=
   ⟨Raw₀.insert ⟨m.1, m.2.size_buckets_pos⟩ a b, .insert₀ m.2⟩
 
-instance : Singleton ((a : α) × β a) (DHashMap α β) := ⟨fun ⟨a, b⟩ => DHashMap.empty.insert a b⟩
+instance : Singleton ((a : α) × β a) (DHashMap α β) := ⟨fun ⟨a, b⟩ => (∅ : DHashMap α β).insert a b⟩
 
 instance : Insert ((a : α) × β a) (DHashMap α β) := ⟨fun ⟨a, b⟩ s => s.insert a b⟩
 

src/Std/Data/DHashMap/Internal/Defs.lean

@@ -170,10 +170,13 @@ abbrev Raw₀ (α : Type u) (β : α → Type v) :=
 namespace Raw₀
 
 /-- Internal implementation detail of the hash map -/
-@[inline] def empty (capacity := 8) : Raw₀ α β :=
+@[inline] def emptyWithCapacity (capacity := 8) : Raw₀ α β :=
   ⟨⟨0, mkArray (numBucketsForCapacity capacity).nextPowerOfTwo AssocList.nil⟩,
     by simpa using Nat.pos_of_isPowerOfTwo (Nat.isPowerOfTwo_nextPowerOfTwo _)⟩
 
+@[deprecated emptyWithCapacity (since := "2025-03-12"), inherit_doc emptyWithCapacity]
+abbrev empty := @emptyWithCapacity
+
 -- Take `hash` as a function instead of `Hashable α` as per
 -- https://github.com/leanprover/lean4/issues/4191
 /-- Internal implementation detail of the hash map -/

src/Std/Data/DHashMap/Internal/Raw.lean

@@ -24,9 +24,11 @@ namespace Std.DHashMap.Internal
 
 namespace Raw
 
-theorem empty_eq [BEq α] [Hashable α] {c : Nat} : (Raw.empty c : Raw α β) = (Raw₀.empty c).1 := rfl
+-- TODO: the next two lemmas need to be renamed, but there is a bootstrapping obstacle.
 
-theorem emptyc_eq [BEq α] [Hashable α] : (∅ : Raw α β) = Raw₀.empty.1 := rfl
+theorem empty_eq [BEq α] [Hashable α] {c : Nat} : (Raw.emptyWithCapacity c : Raw α β) = (Raw₀.emptyWithCapacity c).1 := rfl
+
+theorem emptyc_eq [BEq α] [Hashable α] : (∅ : Raw α β) = Raw₀.emptyWithCapacity.1 := rfl
 
 theorem insert_eq [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {a : α} {b : β a} :
     m.insert a b = (Raw₀.insert ⟨m, h.size_buckets_pos⟩ a b).1 := by
@@ -122,7 +124,7 @@ theorem insertMany_eq [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {ρ : Ty
   simp [Raw.insertMany, h.size_buckets_pos]
 
 theorem ofList_eq [BEq α] [Hashable α] {l : List ((a : α) × β a)} :
-    Raw.ofList l = Raw₀.insertMany Raw₀.empty l := by
+    Raw.ofList l = Raw₀.insertMany Raw₀.emptyWithCapacity l := by
   simp only [Raw.ofList, Raw.insertMany, (Raw.WF.empty).size_buckets_pos ∅, ↓reduceDIte]
   congr
 
@@ -143,7 +145,7 @@ theorem Const.insertMany_eq [BEq α] [Hashable α] {m : Raw α (fun _ => β)} (h
   simp [Raw.Const.insertMany, h.size_buckets_pos]
 
 theorem Const.ofList_eq [BEq α] [Hashable α] {l : List (α × β)} :
-    Raw.Const.ofList l = Raw₀.Const.insertMany Raw₀.empty l := by
+    Raw.Const.ofList l = Raw₀.Const.insertMany Raw₀.emptyWithCapacity l := by
   simp only [Raw.Const.ofList, Raw.Const.insertMany, (Raw.WF.empty).size_buckets_pos ∅, ↓reduceDIte]
   congr
 
@@ -153,7 +155,7 @@ theorem Const.insertManyIfNewUnit_eq {ρ : Type w} [ForIn Id ρ α] [BEq α] [Ha
   simp [Raw.Const.insertManyIfNewUnit, h.size_buckets_pos]
 
 theorem Const.unitOfList_eq [BEq α] [Hashable α] {l : List α} :
-    Raw.Const.unitOfList l = Raw₀.Const.insertManyIfNewUnit Raw₀.empty l := by
+    Raw.Const.unitOfList l = Raw₀.Const.insertManyIfNewUnit Raw₀.emptyWithCapacity l := by
   simp only [Raw.Const.unitOfList, Raw.Const.insertManyIfNewUnit, (Raw.WF.empty).size_buckets_pos ∅,
     ↓reduceDIte]
   congr

src/Std/Data/DHashMap/Internal/WF.lean

@@ -217,14 +217,22 @@ namespace Raw₀
 /-! # Raw₀.empty -/
 
 @[simp]
-theorem toListModel_buckets_empty {c} : toListModel (empty c : Raw₀ α β).1.buckets = [] :=
+theorem toListModel_buckets_emptyWithCapacity {c} : toListModel (emptyWithCapacity c : Raw₀ α β).1.buckets = [] :=
   toListModel_mkArray_nil
 
-theorem wfImp_empty [BEq α] [Hashable α] {c} : Raw.WFImp (empty c : Raw₀ α β).1 where
-  buckets_hash_self := by simp [Raw.empty, Raw₀.empty]
-  size_eq := by simp [Raw.empty, Raw₀.empty]
+set_option linter.missingDocs false in
+@[deprecated toListModel_buckets_emptyWithCapacity (since := "2025-03-12")]
+abbrev toListModel_buckets_empty := @toListModel_buckets_emptyWithCapacity
+
+theorem wfImp_emptyWithCapacity [BEq α] [Hashable α] {c} : Raw.WFImp (emptyWithCapacity c : Raw₀ α β).1 where
+  buckets_hash_self := by simp [Raw.emptyWithCapacity, Raw₀.emptyWithCapacity]
+  size_eq := by simp [Raw.emptyWithCapacity, Raw₀.emptyWithCapacity]
   distinct := by simp
 
+set_option linter.missingDocs false in
+@[deprecated wfImp_emptyWithCapacity (since := "2025-03-12")]
+abbrev wfImp_empty := @wfImp_emptyWithCapacity
+
 theorem isHashSelf_reinsertAux [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α]
     (data : {d : Array (AssocList α β) // 0 < d.size}) (a : α) (b : β a) (h : IsHashSelf data.1) :
     IsHashSelf (reinsertAux hash data a b).1 := by
@@ -1064,7 +1072,7 @@ theorem WF.out [BEq α] [Hashable α] [i₁ : EquivBEq α] [i₂ : LawfulHashabl
     (h : m.WF) : Raw.WFImp m := by
   induction h generalizing i₁ i₂
   · next h => apply h
-  · exact Raw₀.wfImp_empty
+  · exact Raw₀.wfImp_emptyWithCapacity
   · next h => exact Raw₀.wfImp_insert (by apply h)
   · next h => exact Raw₀.wfImp_containsThenInsert (by apply h)
   · next h => exact Raw₀.wfImp_containsThenInsertIfNew (by apply h)

src/Std/Data/DHashMap/Lemmas.lean

@@ -30,12 +30,16 @@ namespace Std.DHashMap
 variable {m : DHashMap α β}
 
 @[simp]
-theorem isEmpty_empty {c} : (empty c : DHashMap α β).isEmpty :=
-  Raw₀.isEmpty_empty
+theorem isEmpty_emptyWithCapacity {c} : (emptyWithCapacity c : DHashMap α β).isEmpty :=
+  Raw₀.isEmpty_emptyWithCapacity
 
 @[simp]
-theorem isEmpty_emptyc : (∅ : DHashMap α β).isEmpty :=
-  isEmpty_empty
+theorem isEmpty_empty : (∅ : DHashMap α β).isEmpty :=
+  isEmpty_emptyWithCapacity
+
+set_option linter.missingDocs false in
+@[deprecated isEmpty_empty (since := "2025-03-12")]
+abbrev isEmpty_emptyc := @isEmpty_empty
 
 @[simp]
 theorem isEmpty_insert [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
@@ -52,17 +56,26 @@ theorem contains_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a ==
 theorem mem_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) : a ∈ m ↔ b ∈ m := by
   simp [mem_iff_contains, contains_congr hab]
 
-@[simp] theorem contains_empty {a : α} {c} : (empty c : DHashMap α β).contains a = false :=
-  Raw₀.contains_empty
+@[simp]
+theorem contains_emptyWithCapacity {a : α} {c} : (emptyWithCapacity c : DHashMap α β).contains a = false :=
+  Raw₀.contains_emptyWithCapacity
 
-@[simp] theorem not_mem_empty {a : α} {c} : ¬a ∈ (empty c : DHashMap α β) := by
+@[simp] theorem not_mem_emptyWithCapacity {a : α} {c} : ¬a ∈ (emptyWithCapacity c : DHashMap α β) := by
   simp [mem_iff_contains]
 
-@[simp] theorem contains_emptyc {a : α} : (∅ : DHashMap α β).contains a = false :=
-  contains_empty
+@[simp] theorem contains_empty {a : α} : (∅ : DHashMap α β).contains a = false :=
+  contains_emptyWithCapacity
 
-@[simp] theorem not_mem_emptyc {a : α} : ¬a ∈ (∅ : DHashMap α β) :=
-  not_mem_empty
+set_option linter.missingDocs false in
+@[deprecated contains_empty (since := "2025-03-12")]
+abbrev contains_emptyc := @contains_empty
+
+@[simp] theorem not_mem_empty {a : α} : ¬a ∈ (∅ : DHashMap α β) :=
+  not_mem_emptyWithCapacity
+
+set_option linter.missingDocs false in
+@[deprecated not_mem_empty (since := "2025-03-12")]
+abbrev not_mem_emptyc := @not_mem_empty
 
 theorem contains_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
     m.isEmpty → m.contains a = false :=
@@ -119,12 +132,16 @@ theorem mem_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
     k ∈ m.insert k v := by simp
 
 @[simp]
-theorem size_empty {c} : (empty c : DHashMap α β).size = 0 :=
-  Raw₀.size_empty
+theorem size_emptyWithCapacity {c} : (emptyWithCapacity c : DHashMap α β).size = 0 :=
+  Raw₀.size_emptyWithCapacity
 
 @[simp]
-theorem size_emptyc : (∅ : DHashMap α β).size = 0 :=
-  size_empty
+theorem size_empty : (∅ : DHashMap α β).size = 0 :=
+  size_emptyWithCapacity
+
+set_option linter.missingDocs false in
+@[deprecated size_empty (since := "2025-03-12")]
+abbrev size_emptyc := @size_empty
 
 theorem isEmpty_eq_size_eq_zero : m.isEmpty = (m.size == 0) := rfl
 
@@ -141,12 +158,16 @@ theorem size_insert_le [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
   Raw₀.size_insert_le ⟨m.1, _⟩ m.2
 
 @[simp]
-theorem erase_empty {k : α} {c : Nat} : (empty c : DHashMap α β).erase k = empty c :=
-  Subtype.eq (congrArg Subtype.val (Raw₀.erase_empty (k := k)) :) -- Lean code is happy
+theorem erase_emptyWithCapacity {k : α} {c : Nat} : (emptyWithCapacity c : DHashMap α β).erase k = emptyWithCapacity c :=
+  Subtype.eq (congrArg Subtype.val (Raw₀.erase_emptyWithCapacity (k := k)) :)
 
 @[simp]
-theorem erase_emptyc {k : α} : (∅ : DHashMap α β).erase k = ∅ :=
-  erase_empty
+theorem erase_empty {k : α} : (∅ : DHashMap α β).erase k = ∅ :=
+  erase_emptyWithCapacity
+
+set_option linter.missingDocs false in
+@[deprecated erase_empty (since := "2025-03-12")]
+abbrev erase_emptyc := @erase_empty
 
 @[simp]
 theorem isEmpty_erase [EquivBEq α] [LawfulHashable α] {k : α} :
@@ -200,12 +221,16 @@ theorem containsThenInsertIfNew_snd {k : α} {v : β k} :
   Subtype.eq <| (congrArg Subtype.val (Raw₀.containsThenInsertIfNew_snd _ (k := k)) :)
 
 @[simp]
-theorem get?_empty [LawfulBEq α] {a : α} {c} : (empty c : DHashMap α β).get? a = none :=
-  Raw₀.get?_empty
+theorem get?_emptyWithCapacity [LawfulBEq α] {a : α} {c} : (emptyWithCapacity c : DHashMap α β).get? a = none :=
+  Raw₀.get?_emptyWithCapacity
 
 @[simp]
-theorem get?_emptyc [LawfulBEq α] {a : α} : (∅ : DHashMap α β).get? a = none :=
-  get?_empty
+theorem get?_empty [LawfulBEq α] {a : α} : (∅ : DHashMap α β).get? a = none :=
+  get?_emptyWithCapacity
+
+set_option linter.missingDocs false in
+@[deprecated get?_empty (since := "2025-03-12")]
+abbrev get?_emptyc := @get?_empty
 
 theorem get?_of_isEmpty [LawfulBEq α] {a : α} : m.isEmpty = true → m.get? a = none :=
   Raw₀.get?_of_isEmpty ⟨m.1, _⟩ m.2
@@ -241,12 +266,16 @@ namespace Const
 variable {β : Type v} {m : DHashMap α (fun _ => β)}
 
 @[simp]
-theorem get?_empty {a : α} {c} : get? (empty c : DHashMap α (fun _ => β)) a = none :=
-  Raw₀.Const.get?_empty
+theorem get?_emptyWithCapacity {a : α} {c} : get? (emptyWithCapacity c : DHashMap α (fun _ => β)) a = none :=
+  Raw₀.Const.get?_emptyWithCapacity
 
 @[simp]
-theorem get?_emptyc {a : α} : get? (∅ : DHashMap α (fun _ => β)) a = none :=
-  get?_empty
+theorem get?_empty {a : α} : get? (∅ : DHashMap α (fun _ => β)) a = none :=
+  get?_emptyWithCapacity
+
+set_option linter.missingDocs false in
+@[deprecated get?_empty (since := "2025-03-12")]
+abbrev get?_emptyc := @get?_empty
 
 theorem get?_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
     m.isEmpty = true → get? m a = none :=
@@ -342,14 +371,18 @@ theorem get_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) {h
 end Const
 
 @[simp]
-theorem get!_empty [LawfulBEq α] {a : α} [Inhabited (β a)] {c} :
-    (empty c : DHashMap α β).get! a = default :=
-  Raw₀.get!_empty
+theorem get!_emptyWithCapacity [LawfulBEq α] {a : α} [Inhabited (β a)] {c} :
+    (emptyWithCapacity c : DHashMap α β).get! a = default :=
+  Raw₀.get!_emptyWithCapacity
 
 @[simp]
-theorem get!_emptyc [LawfulBEq α] {a : α} [Inhabited (β a)] :
+theorem get!_empty [LawfulBEq α] {a : α} [Inhabited (β a)] :
     (∅ : DHashMap α β).get! a = default :=
-  get!_empty
+  get!_emptyWithCapacity
+
+set_option linter.missingDocs false in
+@[deprecated get!_empty (since := "2025-03-12")]
+abbrev get!_emptyc := @get!_empty
 
 theorem get!_of_isEmpty [LawfulBEq α] {a : α} [Inhabited (β a)] :
     m.isEmpty = true → m.get! a = default :=
@@ -403,13 +436,17 @@ namespace Const
 variable {β : Type v} {m : DHashMap α (fun _ => β)}
 
 @[simp]
-theorem get!_empty [Inhabited β] {a : α} {c} :
-    get! (empty c : DHashMap α (fun _ => β)) a = default :=
-  Raw₀.Const.get!_empty
+theorem get!_emptyWithCapacity [Inhabited β] {a : α} {c} :
+    get! (emptyWithCapacity c : DHashMap α (fun _ => β)) a = default :=
+  Raw₀.Const.get!_emptyWithCapacity
 
 @[simp]
-theorem get!_emptyc [Inhabited β] {a : α} : get! (∅ : DHashMap α (fun _ => β)) a = default :=
-  get!_empty
+theorem get!_empty [Inhabited β] {a : α} : get! (∅ : DHashMap α (fun _ => β)) a = default :=
+  get!_emptyWithCapacity
+
+set_option linter.missingDocs false in
+@[deprecated get!_empty (since := "2025-03-12")]
+abbrev get!_emptyc := @get!_empty
 
 theorem get!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
     m.isEmpty = true → get! m a = default :=
@@ -468,14 +505,18 @@ theorem get!_congr [EquivBEq α] [LawfulHashable α] [Inhabited β] {a b : α} (
 end Const
 
 @[simp]
-theorem getD_empty [LawfulBEq α] {a : α} {fallback : β a} {c} :
-    (empty c : DHashMap α β).getD a fallback = fallback :=
-  Raw₀.getD_empty
+theorem getD_emptyWithCapacity [LawfulBEq α] {a : α} {fallback : β a} {c} :
+    (emptyWithCapacity c : DHashMap α β).getD a fallback = fallback :=
+  Raw₀.getD_emptyWithCapacity
 
 @[simp]
-theorem getD_emptyc [LawfulBEq α] {a : α} {fallback : β a} :
+theorem getD_empty [LawfulBEq α] {a : α} {fallback : β a} :
     (∅ : DHashMap α β).getD a fallback = fallback :=
-  getD_empty
+  getD_emptyWithCapacity
+
+set_option linter.missingDocs false in
+@[deprecated getD_empty (since := "2025-03-12")]
+abbrev getD_emptyc := @getD_empty
 
 theorem getD_of_isEmpty [LawfulBEq α] {a : α} {fallback : β a} :
     m.isEmpty = true → m.getD a fallback = fallback :=
@@ -533,14 +574,18 @@ namespace Const
 variable {β : Type v} {m : DHashMap α (fun _ => β)}
 
 @[simp]
-theorem getD_empty {a : α} {fallback : β} {c} :
-    getD (empty c : DHashMap α (fun _ => β)) a fallback = fallback :=
-  Raw₀.Const.getD_empty
+theorem getD_emptyWithCapacity {a : α} {fallback : β} {c} :
+    getD (emptyWithCapacity c : DHashMap α (fun _ => β)) a fallback = fallback :=
+  Raw₀.Const.getD_emptyWithCapacity
 
 @[simp]
-theorem getD_emptyc {a : α} {fallback : β} :
+theorem getD_empty {a : α} {fallback : β} :
     getD (∅ : DHashMap α (fun _ => β)) a fallback = fallback :=
-  getD_empty
+  getD_emptyWithCapacity
+
+set_option linter.missingDocs false in
+@[deprecated getD_empty (since := "2025-03-12")]
+abbrev getD_emptyc := @getD_empty
 
 theorem getD_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} :
     m.isEmpty = true → getD m a fallback = fallback :=
@@ -603,12 +648,16 @@ theorem getD_congr [EquivBEq α] [LawfulHashable α] {a b : α} {fallback : β}
 end Const
 
 @[simp]
-theorem getKey?_empty {a : α} {c} : (empty c : DHashMap α β).getKey? a = none :=
-  Raw₀.getKey?_empty
+theorem getKey?_emptyWithCapacity {a : α} {c} : (emptyWithCapacity c : DHashMap α β).getKey? a = none :=
+  Raw₀.getKey?_emptyWithCapacity
 
 @[simp]
-theorem getKey?_emptyc {a : α} : (∅ : DHashMap α β).getKey? a = none :=
-  Raw₀.getKey?_empty
+theorem getKey?_empty {a : α} : (∅ : DHashMap α β).getKey? a = none :=
+  getKey?_emptyWithCapacity
+
+set_option linter.missingDocs false in
+@[deprecated getKey?_empty (since := "2025-03-12")]
+abbrev getKey?_emptyc := @getKey?_empty
 
 theorem getKey?_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
     m.isEmpty = true → m.getKey? a = none :=
@@ -691,14 +740,18 @@ theorem getKey_eq [LawfulBEq α] {k : α} (h : k ∈ m) : m.getKey k h = k :=
   Raw₀.getKey_eq ⟨m.1, _⟩ m.2 h
 
 @[simp]
-theorem getKey!_empty [Inhabited α] {a : α} {c} :
-    (empty c : DHashMap α β).getKey! a = default :=
-  Raw₀.getKey!_empty
+theorem getKey!_emptyWithCapacity [Inhabited α] {a : α} {c} :
+    (emptyWithCapacity c : DHashMap α β).getKey! a = default :=
+  Raw₀.getKey!_emptyWithCapacity
 
 @[simp]
-theorem getKey!_emptyc [Inhabited α] {a : α} :
+theorem getKey!_empty [Inhabited α] {a : α} :
     (∅ : DHashMap α β).getKey! a = default :=
-  getKey!_empty
+  getKey!_emptyWithCapacity
+
+set_option linter.missingDocs false in
+@[deprecated getKey!_empty (since := "2025-03-12")]
+abbrev getKey!_emptyc := @getKey!_empty
 
 theorem getKey!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
     m.isEmpty = true → m.getKey! a = default :=
@@ -760,14 +813,18 @@ theorem getKey!_eq_of_mem [LawfulBEq α] [Inhabited α] {k : α} (h : k ∈ m) :
   getKey!_eq_of_contains h
 
 @[simp]
-theorem getKeyD_empty {a fallback : α} {c} :
-    (empty c : DHashMap α β).getKeyD a fallback = fallback :=
-  Raw₀.getKeyD_empty
+theorem getKeyD_emptyWithCapacity {a fallback : α} {c} :
+    (emptyWithCapacity c : DHashMap α β).getKeyD a fallback = fallback :=
+  Raw₀.getKeyD_emptyWithCapacity
 
 @[simp]
-theorem getKeyD_emptyc {a fallback : α} :
+theorem getKeyD_empty {a fallback : α} :
     (∅ : DHashMap α β).getKeyD a fallback = fallback :=
-  getKeyD_empty
+  getKeyD_emptyWithCapacity
+
+set_option linter.missingDocs false in
+@[deprecated getKeyD_empty (since := "2025-03-12")]
+abbrev getKeyD_emptyc := @getKeyD_empty
 
 theorem getKeyD_of_isEmpty [EquivBEq α] [LawfulHashable α] {a fallback : α} :
     m.isEmpty = true → m.getKeyD a fallback = fallback :=
@@ -1753,22 +1810,22 @@ namespace DHashMap
 @[simp]
 theorem ofList_nil :
     ofList ([] : List ((a : α) × (β a))) = ∅ :=
-  Subtype.eq (congrArg Subtype.val (Raw₀.insertMany_empty_list_nil (α := α)) :)
+  Subtype.eq (congrArg Subtype.val (Raw₀.insertMany_emptyWithCapacity_list_nil (α := α)) :)
 
 @[simp]
 theorem ofList_singleton {k : α} {v : β k} :
     ofList [⟨k, v⟩] = (∅: DHashMap α β).insert k v :=
-  Subtype.eq (congrArg Subtype.val (Raw₀.insertMany_empty_list_singleton (α := α)) :)
+  Subtype.eq (congrArg Subtype.val (Raw₀.insertMany_emptyWithCapacity_list_singleton (α := α)) :)
 
 theorem ofList_cons {k : α} {v : β k} {tl : List ((a : α) × (β a))} :
     ofList (⟨k, v⟩ :: tl) = ((∅ : DHashMap α β).insert k v).insertMany tl :=
-  Subtype.eq (congrArg Subtype.val (Raw₀.insertMany_empty_list_cons (α := α)) :)
+  Subtype.eq (congrArg Subtype.val (Raw₀.insertMany_emptyWithCapacity_list_cons (α := α)) :)
 
 @[simp]
 theorem contains_ofList [EquivBEq α] [LawfulHashable α]
     {l : List ((a : α) × β a)} {k : α} :
     (ofList l).contains k = (l.map Sigma.fst).contains k :=
-  Raw₀.contains_insertMany_empty_list
+  Raw₀.contains_insertMany_emptyWithCapacity_list
 
 @[simp]
 theorem mem_ofList [EquivBEq α] [LawfulHashable α]
@@ -1780,14 +1837,14 @@ theorem get?_ofList_of_contains_eq_false [LawfulBEq α]
     {l : List ((a : α) × β a)} {k : α}
     (contains_eq_false : (l.map Sigma.fst).contains k = false) :
     (ofList l).get? k = none :=
-  Raw₀.get?_insertMany_empty_list_of_contains_eq_false contains_eq_false
+  Raw₀.get?_insertMany_emptyWithCapacity_list_of_contains_eq_false contains_eq_false
 
 theorem get?_ofList_of_mem [LawfulBEq α]
     {l : List ((a : α) × β a)} {k k' : α} (k_beq : k == k') {v : β k}
     (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
     (mem : ⟨k, v⟩ ∈ l) :
     (ofList l).get? k' = some (cast (by congr; apply LawfulBEq.eq_of_beq k_beq) v) :=
-  Raw₀.get?_insertMany_empty_list_of_mem k_beq distinct mem
+  Raw₀.get?_insertMany_emptyWithCapacity_list_of_mem k_beq distinct mem
 
 theorem get_ofList_of_mem [LawfulBEq α]
     {l : List ((a : α) × β a)} {k k' : α} (k_beq : k == k') {v : β k}
@@ -1795,39 +1852,39 @@ theorem get_ofList_of_mem [LawfulBEq α]
     (mem : ⟨k, v⟩ ∈ l)
     {h} :
     (ofList l).get k' h = cast (by congr; apply LawfulBEq.eq_of_beq k_beq) v :=
-  Raw₀.get_insertMany_empty_list_of_mem k_beq distinct mem
+  Raw₀.get_insertMany_emptyWithCapacity_list_of_mem k_beq distinct mem
 
 theorem get!_ofList_of_contains_eq_false [LawfulBEq α]
     {l : List ((a : α) × β a)} {k : α} [Inhabited (β k)]
     (contains_eq_false : (l.map Sigma.fst).contains k = false) :
     (ofList l).get! k = default :=
-  Raw₀.get!_insertMany_empty_list_of_contains_eq_false contains_eq_false
+  Raw₀.get!_insertMany_emptyWithCapacity_list_of_contains_eq_false contains_eq_false
 
 theorem get!_ofList_of_mem [LawfulBEq α]
     {l : List ((a : α) × β a)} {k k' : α} (k_beq : k == k') {v : β k} [Inhabited (β k')]
     (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
     (mem : ⟨k, v⟩ ∈ l) :
     (ofList l).get! k' = cast (by congr; apply LawfulBEq.eq_of_beq k_beq) v :=
-  Raw₀.get!_insertMany_empty_list_of_mem k_beq distinct mem
+  Raw₀.get!_insertMany_emptyWithCapacity_list_of_mem k_beq distinct mem
 
 theorem getD_ofList_of_contains_eq_false [LawfulBEq α]
     {l : List ((a : α) × β a)} {k : α} {fallback : β k}
     (contains_eq_false : (l.map Sigma.fst).contains k = false) :
     (ofList l).getD k fallback = fallback :=
-  Raw₀.getD_insertMany_empty_list_of_contains_eq_false contains_eq_false
+  Raw₀.getD_insertMany_emptyWithCapacity_list_of_contains_eq_false contains_eq_false
 
 theorem getD_ofList_of_mem [LawfulBEq α]
     {l : List ((a : α) × β a)} {k k' : α} (k_beq : k == k') {v : β k} {fallback : β k'}
     (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
     (mem : ⟨k, v⟩ ∈ l) :
     (ofList l).getD k' fallback = cast (by congr; apply LawfulBEq.eq_of_beq k_beq) v :=
-  Raw₀.getD_insertMany_empty_list_of_mem k_beq distinct mem
+  Raw₀.getD_insertMany_emptyWithCapacity_list_of_mem k_beq distinct mem
 
 theorem getKey?_ofList_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
     {l : List ((a : α) × β a)} {k : α}
     (contains_eq_false : (l.map Sigma.fst).contains k = false) :
     (ofList l).getKey? k = none :=
-  Raw₀.getKey?_insertMany_empty_list_of_contains_eq_false contains_eq_false
+  Raw₀.getKey?_insertMany_emptyWithCapacity_list_of_contains_eq_false contains_eq_false
 
 theorem getKey?_ofList_of_mem [EquivBEq α] [LawfulHashable α]
     {l : List ((a : α) × β a)}
@@ -1835,7 +1892,7 @@ theorem getKey?_ofList_of_mem [EquivBEq α] [LawfulHashable α]
     (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
     (mem : k ∈ l.map Sigma.fst) :
     (ofList l).getKey? k' = some k :=
-  Raw₀.getKey?_insertMany_empty_list_of_mem k_beq distinct mem
+  Raw₀.getKey?_insertMany_emptyWithCapacity_list_of_mem k_beq distinct mem
 
 theorem getKey_ofList_of_mem [EquivBEq α] [LawfulHashable α]
     {l : List ((a : α) × β a)}
@@ -1844,13 +1901,13 @@ theorem getKey_ofList_of_mem [EquivBEq α] [LawfulHashable α]
     (mem : k ∈ l.map Sigma.fst)
     {h} :
     (ofList l).getKey k' h = k :=
-  Raw₀.getKey_insertMany_empty_list_of_mem k_beq distinct mem
+  Raw₀.getKey_insertMany_emptyWithCapacity_list_of_mem k_beq distinct mem
 
 theorem getKey!_ofList_of_contains_eq_false [EquivBEq α] [LawfulHashable α] [Inhabited α]
     {l : List ((a : α) × β a)} {k : α}
     (contains_eq_false : (l.map Sigma.fst).contains k = false) :
     (ofList l).getKey! k = default :=
-  Raw₀.getKey!_insertMany_empty_list_of_contains_eq_false contains_eq_false
+  Raw₀.getKey!_insertMany_emptyWithCapacity_list_of_contains_eq_false contains_eq_false
 
 theorem getKey!_ofList_of_mem [EquivBEq α] [LawfulHashable α] [Inhabited α]
     {l : List ((a : α) × β a)}
@@ -1858,13 +1915,13 @@ theorem getKey!_ofList_of_mem [EquivBEq α] [LawfulHashable α] [Inhabited α]
     (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
     (mem : k ∈ l.map Sigma.fst) :
     (ofList l).getKey! k' = k :=
-  Raw₀.getKey!_insertMany_empty_list_of_mem k_beq distinct mem
+  Raw₀.getKey!_insertMany_emptyWithCapacity_list_of_mem k_beq distinct mem
 
 theorem getKeyD_ofList_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
     {l : List ((a : α) × β a)} {k fallback : α}
     (contains_eq_false : (l.map Sigma.fst).contains k = false) :
     (ofList l).getKeyD k fallback = fallback :=
-  Raw₀.getKeyD_insertMany_empty_list_of_contains_eq_false contains_eq_false
+  Raw₀.getKeyD_insertMany_emptyWithCapacity_list_of_contains_eq_false contains_eq_false
 
 theorem getKeyD_ofList_of_mem [EquivBEq α] [LawfulHashable α]
     {l : List ((a : α) × β a)}
@@ -1872,23 +1929,23 @@ theorem getKeyD_ofList_of_mem [EquivBEq α] [LawfulHashable α]
     (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
     (mem : k ∈ l.map Sigma.fst) :
     (ofList l).getKeyD k' fallback = k :=
-  Raw₀.getKeyD_insertMany_empty_list_of_mem k_beq distinct mem
+  Raw₀.getKeyD_insertMany_emptyWithCapacity_list_of_mem k_beq distinct mem
 
 theorem size_ofList [EquivBEq α] [LawfulHashable α]
     {l : List ((a : α) × β a)} (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) :
     (ofList l).size = l.length :=
-  Raw₀.size_insertMany_empty_list distinct
+  Raw₀.size_insertMany_emptyWithCapacity_list distinct
 
 theorem size_ofList_le [EquivBEq α] [LawfulHashable α]
     {l : List ((a : α) × β a)} :
     (ofList l).size ≤ l.length :=
-  Raw₀.size_insertMany_empty_list_le
+  Raw₀.size_insertMany_emptyWithCapacity_list_le
 
 @[simp]
 theorem isEmpty_ofList [EquivBEq α] [LawfulHashable α]
     {l : List ((a : α) × β a)} :
     (ofList l).isEmpty = l.isEmpty :=
-  Raw₀.isEmpty_insertMany_empty_list
+  Raw₀.isEmpty_insertMany_emptyWithCapacity_list
 
 namespace Const
 
@@ -1897,22 +1954,22 @@ variable {β : Type v}
 @[simp]
 theorem ofList_nil :
     ofList ([] : List (α × β)) = ∅ :=
-  Subtype.eq (congrArg Subtype.val (Raw₀.Const.insertMany_empty_list_nil (α:= α)) :)
+  Subtype.eq (congrArg Subtype.val (Raw₀.Const.insertMany_emptyWithCapacity_list_nil (α:= α)) :)
 
 @[simp]
 theorem ofList_singleton {k : α} {v : β} :
     ofList [⟨k, v⟩] = (∅ : DHashMap α (fun _ => β)).insert k v :=
-  Subtype.eq (congrArg Subtype.val (Raw₀.Const.insertMany_empty_list_singleton (α:= α)) :)
+  Subtype.eq (congrArg Subtype.val (Raw₀.Const.insertMany_emptyWithCapacity_list_singleton (α:= α)) :)
 
 theorem ofList_cons {k : α} {v : β} {tl : List (α × β)} :
     ofList (⟨k, v⟩ :: tl) = insertMany ((∅ : DHashMap α (fun _ => β)).insert k v) tl :=
-  Subtype.eq (congrArg Subtype.val (Raw₀.Const.insertMany_empty_list_cons (α:= α)) :)
+  Subtype.eq (congrArg Subtype.val (Raw₀.Const.insertMany_emptyWithCapacity_list_cons (α:= α)) :)
 
 @[simp]
 theorem contains_ofList [EquivBEq α] [LawfulHashable α]
     {l : List (α × β)} {k : α} :
     (ofList l).contains k = (l.map Prod.fst).contains k :=
-  Raw₀.Const.contains_insertMany_empty_list
+  Raw₀.Const.contains_insertMany_emptyWithCapacity_list
 
 @[simp]
 theorem mem_ofList [EquivBEq α] [LawfulHashable α]
@@ -1924,14 +1981,14 @@ theorem get?_ofList_of_contains_eq_false [LawfulBEq α]
     {l : List (α × β)} {k : α}
     (contains_eq_false : (l.map Prod.fst).contains k = false) :
     get? (ofList l) k = none :=
-  Raw₀.Const.get?_insertMany_empty_list_of_contains_eq_false contains_eq_false
+  Raw₀.Const.get?_insertMany_emptyWithCapacity_list_of_contains_eq_false contains_eq_false
 
 theorem get?_ofList_of_mem [LawfulBEq α]
     {l : List (α × β)} {k k' : α} (k_beq : k == k') {v : β}
     (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
     (mem : ⟨k, v⟩ ∈ l) :
     get? (ofList l) k' = some v :=
-  Raw₀.Const.get?_insertMany_empty_list_of_mem k_beq distinct mem
+  Raw₀.Const.get?_insertMany_emptyWithCapacity_list_of_mem k_beq distinct mem
 
 theorem get_ofList_of_mem [LawfulBEq α]
     {l : List (α × β)} {k k' : α} (k_beq : k == k') {v : β}
@@ -1939,39 +1996,39 @@ theorem get_ofList_of_mem [LawfulBEq α]
     (mem : ⟨k, v⟩ ∈ l)
     {h} :
     get (ofList l) k' h = v :=
-  Raw₀.Const.get_insertMany_empty_list_of_mem k_beq distinct mem
+  Raw₀.Const.get_insertMany_emptyWithCapacity_list_of_mem k_beq distinct mem
 
 theorem get!_ofList_of_contains_eq_false [LawfulBEq α]
     {l : List (α × β)} {k : α} [Inhabited β]
     (contains_eq_false : (l.map Prod.fst).contains k = false) :
     get! (ofList l) k = (default : β) :=
-  Raw₀.Const.get!_insertMany_empty_list_of_contains_eq_false contains_eq_false
+  Raw₀.Const.get!_insertMany_emptyWithCapacity_list_of_contains_eq_false contains_eq_false
 
 theorem get!_ofList_of_mem [LawfulBEq α]
     {l : List (α × β)} {k k' : α} (k_beq : k == k') {v : β} [Inhabited β]
     (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
     (mem : ⟨k, v⟩ ∈ l) :
     get! (ofList l) k' = v :=
-  Raw₀.Const.get!_insertMany_empty_list_of_mem k_beq distinct mem
+  Raw₀.Const.get!_insertMany_emptyWithCapacity_list_of_mem k_beq distinct mem
 
 theorem getD_ofList_of_contains_eq_false [LawfulBEq α]
     {l : List (α × β)} {k : α} {fallback : β}
     (contains_eq_false : (l.map Prod.fst).contains k = false) :
     getD (ofList l) k fallback = fallback :=
-  Raw₀.Const.getD_insertMany_empty_list_of_contains_eq_false contains_eq_false
+  Raw₀.Const.getD_insertMany_emptyWithCapacity_list_of_contains_eq_false contains_eq_false
 
 theorem getD_ofList_of_mem [LawfulBEq α]
     {l : List (α × β)} {k k' : α} (k_beq : k == k') {v : β} {fallback : β}
     (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
     (mem : ⟨k, v⟩ ∈ l) :
     getD (ofList l) k' fallback = v :=
-  Raw₀.Const.getD_insertMany_empty_list_of_mem k_beq distinct mem
+  Raw₀.Const.getD_insertMany_emptyWithCapacity_list_of_mem k_beq distinct mem
 
 theorem getKey?_ofList_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
     {l : List (α × β)} {k : α}
     (contains_eq_false : (l.map Prod.fst).contains k = false) :
     (ofList l).getKey? k = none :=
-  Raw₀.Const.getKey?_insertMany_empty_list_of_contains_eq_false contains_eq_false
+  Raw₀.Const.getKey?_insertMany_emptyWithCapacity_list_of_contains_eq_false contains_eq_false
 
 theorem getKey?_ofList_of_mem [EquivBEq α] [LawfulHashable α]
     {l : List (α × β)}
@@ -1979,7 +2036,7 @@ theorem getKey?_ofList_of_mem [EquivBEq α] [LawfulHashable α]
     (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
     (mem : k ∈ l.map Prod.fst) :
     (ofList l).getKey? k' = some k :=
-  Raw₀.Const.getKey?_insertMany_empty_list_of_mem k_beq distinct mem
+  Raw₀.Const.getKey?_insertMany_emptyWithCapacity_list_of_mem k_beq distinct mem
 
 theorem getKey_ofList_of_mem [EquivBEq α] [LawfulHashable α]
     {l : List (α × β)}
@@ -1988,13 +2045,13 @@ theorem getKey_ofList_of_mem [EquivBEq α] [LawfulHashable α]
     (mem : k ∈ l.map Prod.fst)
     {h} :
     (ofList l).getKey k' h = k :=
-  Raw₀.Const.getKey_insertMany_empty_list_of_mem k_beq distinct mem
+  Raw₀.Const.getKey_insertMany_emptyWithCapacity_list_of_mem k_beq distinct mem
 
 theorem getKey!_ofList_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
     [Inhabited α] {l : List (α × β)} {k : α}
     (contains_eq_false : (l.map Prod.fst).contains k = false) :
     (ofList l).getKey! k = default :=
-  Raw₀.Const.getKey!_insertMany_empty_list_of_contains_eq_false contains_eq_false
+  Raw₀.Const.getKey!_insertMany_emptyWithCapacity_list_of_contains_eq_false contains_eq_false
 
 theorem getKey!_ofList_of_mem [EquivBEq α] [LawfulHashable α] [Inhabited α]
     {l : List (α × β)}
@@ -2002,13 +2059,13 @@ theorem getKey!_ofList_of_mem [EquivBEq α] [LawfulHashable α] [Inhabited α]
     (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
     (mem : k ∈ l.map Prod.fst) :
     (ofList l).getKey! k' = k :=
-  Raw₀.Const.getKey!_insertMany_empty_list_of_mem k_beq distinct mem
+  Raw₀.Const.getKey!_insertMany_emptyWithCapacity_list_of_mem k_beq distinct mem
 
 theorem getKeyD_ofList_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
     {l : List (α × β)} {k fallback : α}
     (contains_eq_false : (l.map Prod.fst).contains k = false) :
     (ofList l).getKeyD k fallback = fallback :=
-  Raw₀.Const.getKeyD_insertMany_empty_list_of_contains_eq_false contains_eq_false
+  Raw₀.Const.getKeyD_insertMany_emptyWithCapacity_list_of_contains_eq_false contains_eq_false
 
 theorem getKeyD_ofList_of_mem [EquivBEq α] [LawfulHashable α]
     {l : List (α × β)}
@@ -2016,44 +2073,44 @@ theorem getKeyD_ofList_of_mem [EquivBEq α] [LawfulHashable α]
     (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
     (mem : k ∈ l.map Prod.fst) :
     (ofList l).getKeyD k' fallback = k :=
-  Raw₀.Const.getKeyD_insertMany_empty_list_of_mem k_beq distinct mem
+  Raw₀.Const.getKeyD_insertMany_emptyWithCapacity_list_of_mem k_beq distinct mem
 
 theorem size_ofList [EquivBEq α] [LawfulHashable α]
     {l : List (α × β)} (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) :
     (ofList l).size = l.length :=
-  Raw₀.Const.size_insertMany_empty_list distinct
+  Raw₀.Const.size_insertMany_emptyWithCapacity_list distinct
 
 theorem size_ofList_le [EquivBEq α] [LawfulHashable α]
     {l : List (α × β)} :
     (ofList l).size ≤ l.length :=
-  Raw₀.Const.size_insertMany_empty_list_le
+  Raw₀.Const.size_insertMany_emptyWithCapacity_list_le
 
 @[simp]
 theorem isEmpty_ofList [EquivBEq α] [LawfulHashable α]
     {l : List (α × β)} :
     (ofList l).isEmpty = l.isEmpty :=
-  Raw₀.Const.isEmpty_insertMany_empty_list
+  Raw₀.Const.isEmpty_insertMany_emptyWithCapacity_list
 
 @[simp]
 theorem unitOfList_nil :
     unitOfList ([] : List α) = ∅ :=
-  Subtype.eq (congrArg Subtype.val (Raw₀.Const.insertManyIfNewUnit_empty_list_nil (α := α)) :)
+  Subtype.eq (congrArg Subtype.val (Raw₀.Const.insertManyIfNewUnit_emptyWithCapacity_list_nil (α := α)) :)
 
 @[simp]
 theorem unitOfList_singleton {k : α} :
     unitOfList [k] = (∅ : DHashMap α (fun _ => Unit)).insertIfNew k () :=
-  Subtype.eq (congrArg Subtype.val (Raw₀.Const.insertManyIfNewUnit_empty_list_singleton (α := α)) :)
+  Subtype.eq (congrArg Subtype.val (Raw₀.Const.insertManyIfNewUnit_emptyWithCapacity_list_singleton (α := α)) :)
 
 theorem unitOfList_cons {hd : α} {tl : List α} :
     unitOfList (hd :: tl) =
       insertManyIfNewUnit ((∅ : DHashMap α (fun _ => Unit)).insertIfNew hd ()) tl :=
-  Subtype.eq (congrArg Subtype.val (Raw₀.Const.insertManyIfNewUnit_empty_list_cons (α := α)) :)
+  Subtype.eq (congrArg Subtype.val (Raw₀.Const.insertManyIfNewUnit_emptyWithCapacity_list_cons (α := α)) :)
 
 @[simp]
 theorem contains_unitOfList [EquivBEq α] [LawfulHashable α]
     {l : List α} {k : α} :
     (unitOfList l).contains k = l.contains k :=
-  Raw₀.Const.contains_insertManyIfNewUnit_empty_list
+  Raw₀.Const.contains_insertManyIfNewUnit_emptyWithCapacity_list
 
 @[simp]
 theorem mem_unitOfList [EquivBEq α] [LawfulHashable α]
@@ -2064,13 +2121,13 @@ theorem mem_unitOfList [EquivBEq α] [LawfulHashable α]
 theorem getKey?_unitOfList_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
     {l : List α} {k : α} (contains_eq_false : l.contains k = false) :
     getKey? (unitOfList l) k = none :=
-  Raw₀.Const.getKey?_insertManyIfNewUnit_empty_list_of_contains_eq_false contains_eq_false
+  Raw₀.Const.getKey?_insertManyIfNewUnit_emptyWithCapacity_list_of_contains_eq_false contains_eq_false
 
 theorem getKey?_unitOfList_of_mem [EquivBEq α] [LawfulHashable α]
     {l : List α} {k k' : α} (k_beq : k == k')
     (distinct : l.Pairwise (fun a b => (a == b) = false)) (mem : k ∈ l) :
     getKey? (unitOfList l) k' = some k :=
-  Raw₀.Const.getKey?_insertManyIfNewUnit_empty_list_of_mem k_beq distinct mem
+  Raw₀.Const.getKey?_insertManyIfNewUnit_emptyWithCapacity_list_of_mem k_beq distinct mem
 
 theorem getKey_unitOfList_of_mem [EquivBEq α] [LawfulHashable α]
     {l : List α}
@@ -2078,69 +2135,69 @@ theorem getKey_unitOfList_of_mem [EquivBEq α] [LawfulHashable α]
     (distinct : l.Pairwise (fun a b => (a == b) = false))
     (mem : k ∈ l) {h} :
     getKey (unitOfList l) k' h = k :=
-  Raw₀.Const.getKey_insertManyIfNewUnit_empty_list_of_mem k_beq distinct mem
+  Raw₀.Const.getKey_insertManyIfNewUnit_emptyWithCapacity_list_of_mem k_beq distinct mem
 
 theorem getKey!_unitOfList_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
     [Inhabited α] {l : List α} {k : α}
     (contains_eq_false : l.contains k = false) :
     getKey! (unitOfList l) k = default :=
-  Raw₀.Const.getKey!_insertManyIfNewUnit_empty_list_of_contains_eq_false contains_eq_false
+  Raw₀.Const.getKey!_insertManyIfNewUnit_emptyWithCapacity_list_of_contains_eq_false contains_eq_false
 
 theorem getKey!_unitOfList_of_mem [EquivBEq α] [LawfulHashable α]
     [Inhabited α] {l : List α} {k k' : α} (k_beq : k == k')
     (distinct : l.Pairwise (fun a b => (a == b) = false))
     (mem : k ∈ l) :
     getKey! (unitOfList l) k' = k :=
-  Raw₀.Const.getKey!_insertManyIfNewUnit_empty_list_of_mem k_beq distinct mem
+  Raw₀.Const.getKey!_insertManyIfNewUnit_emptyWithCapacity_list_of_mem k_beq distinct mem
 
 theorem getKeyD_unitOfList_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
     {l : List α} {k fallback : α}
     (contains_eq_false : l.contains k = false) :
     getKeyD (unitOfList l) k fallback = fallback :=
-  Raw₀.Const.getKeyD_insertManyIfNewUnit_empty_list_of_contains_eq_false contains_eq_false
+  Raw₀.Const.getKeyD_insertManyIfNewUnit_emptyWithCapacity_list_of_contains_eq_false contains_eq_false
 
 theorem getKeyD_unitOfList_of_mem [EquivBEq α] [LawfulHashable α]
     {l : List α} {k k' fallback : α} (k_beq : k == k')
     (distinct : l.Pairwise (fun a b => (a == b) = false))
     (mem : k ∈ l) :
     getKeyD (unitOfList l) k' fallback = k :=
-  Raw₀.Const.getKeyD_insertManyIfNewUnit_empty_list_of_mem k_beq distinct mem
+  Raw₀.Const.getKeyD_insertManyIfNewUnit_emptyWithCapacity_list_of_mem k_beq distinct mem
 
 theorem size_unitOfList [EquivBEq α] [LawfulHashable α]
     {l : List α}
     (distinct : l.Pairwise (fun a b => (a == b) = false)) :
     (unitOfList l).size = l.length :=
-  Raw₀.Const.size_insertManyIfNewUnit_empty_list distinct
+  Raw₀.Const.size_insertManyIfNewUnit_emptyWithCapacity_list distinct
 
 theorem size_unitOfList_le [EquivBEq α] [LawfulHashable α]
     {l : List α} :
     (unitOfList l).size ≤ l.length :=
-  Raw₀.Const.size_insertManyIfNewUnit_empty_list_le
+  Raw₀.Const.size_insertManyIfNewUnit_emptyWithCapacity_list_le
 
 @[simp]
 theorem isEmpty_unitOfList [EquivBEq α] [LawfulHashable α]
     {l : List α} :
     (unitOfList l).isEmpty = l.isEmpty :=
-  Raw₀.Const.isEmpty_insertManyIfNewUnit_empty_list
+  Raw₀.Const.isEmpty_insertManyIfNewUnit_emptyWithCapacity_list
 
 @[simp]
 theorem get?_unitOfList [EquivBEq α] [LawfulHashable α]
     {l : List α} {k : α} :
     get? (unitOfList l) k =
     if l.contains k then some () else none :=
-  Raw₀.Const.get?_insertManyIfNewUnit_empty_list
+  Raw₀.Const.get?_insertManyIfNewUnit_emptyWithCapacity_list
 
 @[simp]
 theorem get_unitOfList
     {l : List α} {k : α} {h} :
     get (unitOfList l) k h = () :=
-  Raw₀.Const.get_insertManyIfNewUnit_empty_list
+  Raw₀.Const.get_insertManyIfNewUnit_emptyWithCapacity_list
 
 @[simp]
 theorem get!_unitOfList
     {l : List α} {k : α} :
     get! (unitOfList l) k = () :=
-  Raw₀.Const.get!_insertManyIfNewUnit_empty_list
+  Raw₀.Const.get!_insertManyIfNewUnit_emptyWithCapacity_list
 
 @[simp]
 theorem getD_unitOfList
@@ -2991,23 +3048,30 @@ end Const
 end Equiv
 
 @[simp]
-theorem equiv_empty_iff_isEmpty [EquivBEq α] [LawfulHashable α] {c : Nat} :
-    m ~m empty c ↔ m.isEmpty :=
-  ⟨fun ⟨h⟩ => (Raw₀.equiv_empty_iff_isEmpty ⟨m.1, m.2.size_buckets_pos⟩ m.2).mp h,
-    fun h => ⟨(Raw₀.equiv_empty_iff_isEmpty ⟨m.1, m.2.size_buckets_pos⟩ m.2).mpr h⟩⟩
+theorem equiv_emptyWithCapacity_iff_isEmpty [EquivBEq α] [LawfulHashable α] {c : Nat} :
+    m ~m emptyWithCapacity c ↔ m.isEmpty :=
+  ⟨fun ⟨h⟩ => (Raw₀.equiv_emptyWithCapacity_iff_isEmpty ⟨m.1, m.2.size_buckets_pos⟩ m.2).mp h,
+    fun h => ⟨(Raw₀.equiv_emptyWithCapacity_iff_isEmpty ⟨m.1, m.2.size_buckets_pos⟩ m.2).mpr h⟩⟩
 
 @[simp]
-theorem equiv_emptyc_iff_isEmpty [EquivBEq α] [LawfulHashable α] : m ~m ∅ ↔ m.isEmpty :=
-  equiv_empty_iff_isEmpty
+theorem equiv_empty_iff_isEmpty [EquivBEq α] [LawfulHashable α] : m ~m ∅ ↔ m.isEmpty :=
+  equiv_emptyWithCapacity_iff_isEmpty
+
+set_option linter.missingDocs false in
+@[deprecated equiv_empty_iff_isEmpty (since := "2025-03-11")]
+abbrev equiv_emptyc_iff_isEmpty := @equiv_empty_iff_isEmpty
+
+theorem empty_equivWithCapacity_iff_isEmpty [EquivBEq α] [LawfulHashable α] {c : Nat} :
+    emptyWithCapacity c ~m m ↔ m.isEmpty :=
+  Equiv.comm.trans equiv_emptyWithCapacity_iff_isEmpty
 
 @[simp]
-theorem empty_equiv_iff_isEmpty [EquivBEq α] [LawfulHashable α] {c : Nat} :
-    empty c ~m m ↔ m.isEmpty :=
-  Equiv.comm.trans equiv_empty_iff_isEmpty
+theorem empty_equiv_iff_isEmpty [EquivBEq α] [LawfulHashable α] : ∅ ~m m ↔ m.isEmpty :=
+  empty_equivWithCapacity_iff_isEmpty
 
-@[simp]
-theorem emptyc_equiv_iff_isEmpty [EquivBEq α] [LawfulHashable α] : ∅ ~m m ↔ m.isEmpty :=
-  empty_equiv_iff_isEmpty
+set_option linter.missingDocs false in
+@[deprecated empty_equiv_iff_isEmpty (since := "2025-03-11")]
+abbrev emptyc_equiv_iff_isEmpty := @empty_equiv_iff_isEmpty
 
 theorem equiv_iff_toList_perm {m₁ m₂ : DHashMap α β} [EquivBEq α] [LawfulHashable α] :
     m₁ ~m m₂ ↔ m₁.toList.Perm m₂.toList :=

src/Std/Data/DHashMap/Raw.lean

@@ -48,11 +48,14 @@ map so that it can hold the given number of mappings without reallocating. It is
 use the empty collection notations `∅` and `{}` to create an empty hash map with the default
 capacity.
 -/
-@[inline] def empty (capacity := 8) : Raw α β :=
-  (Raw₀.empty capacity).1
+@[inline] def emptyWithCapacity (capacity := 8) : Raw α β :=
+  (Raw₀.emptyWithCapacity capacity).1
+
+@[deprecated emptyWithCapacity (since := "2025-03-12"), inherit_doc emptyWithCapacity]
+abbrev empty := @emptyWithCapacity
 
 instance : EmptyCollection (Raw α β) where
-  emptyCollection := empty
+  emptyCollection := emptyWithCapacity
 
 instance : Inhabited (Raw α β) where
   default := ∅
@@ -81,7 +84,7 @@ unchanged if a matching key is already present.
   else m -- will never happen for well-formed inputs
 
 instance [BEq α] [Hashable α] : Singleton ((a : α) × β a) (Raw α β) :=
-  ⟨fun ⟨a, b⟩ => Raw.empty.insert a b⟩
+  ⟨fun ⟨a, b⟩ => (∅ : Raw α β).insert a b⟩
 
 instance [BEq α] [Hashable α] : Insert ((a : α) × β a) (Raw α β) :=
   ⟨fun ⟨a, b⟩ s => s.insert a b⟩
@@ -581,7 +584,7 @@ inductive WF : {α : Type u} → {β : α → Type v} → [BEq α] → [Hashable
   | wf {α β} [BEq α] [Hashable α] {m : Raw α β} : 0 < m.buckets.size →
       (∀ [EquivBEq α] [LawfulHashable α], Raw.WFImp m) → WF m
   /-- Internal implementation detail of the hash map -/
-  | empty₀ {α β} [BEq α] [Hashable α] {c} : WF (Raw₀.empty c : Raw₀ α β).1
+  | emptyWithCapacity₀ {α β} [BEq α] [Hashable α] {c} : WF (Raw₀.emptyWithCapacity c : Raw₀ α β).1
   /-- Internal implementation detail of the hash map -/
   | insert₀ {α β} [BEq α] [Hashable α] {m : Raw α β} {h a b} : WF m → WF (Raw₀.insert ⟨m, h⟩ a b).1
   /-- Internal implementation detail of the hash map -/
@@ -616,10 +619,15 @@ inductive WF : {α : Type u} → {β : α → Type v} → [BEq α] → [Hashable
   | constAlter₀ {α} {β : Type v} [BEq α] [Hashable α] {m : Raw α (fun _ => β)} {h a}
       {f : Option β → Option β} : WF m → WF (Raw₀.Const.alter ⟨m, h⟩ a f).1
 
+-- TODO: this needs to be deprecated, but there is a bootstrapping issue.
+-- @[deprecated WF.emptyWithCapacity₀ (since := "2025-03-12")]
+@[inherit_doc Raw.WF.emptyWithCapacity₀]
+abbrev WF.empty₀ := @WF.emptyWithCapacity₀
+
 /-- Internal implementation detail of the hash map -/
 theorem WF.size_buckets_pos [BEq α] [Hashable α] (m : Raw α β) : WF m → 0 < m.buckets.size
   | wf h₁ _ => h₁
-  | empty₀ => (Raw₀.empty _).2
+  | emptyWithCapacity₀ => (Raw₀.emptyWithCapacity _).2
   | insert₀ _ => (Raw₀.insert ⟨_, _⟩ _ _).2
   | containsThenInsert₀ _ => (Raw₀.containsThenInsert ⟨_, _⟩ _ _).2.2
   | containsThenInsertIfNew₀ _ => (Raw₀.containsThenInsertIfNew ⟨_, _⟩ _ _).2.2
@@ -633,11 +641,15 @@ theorem WF.size_buckets_pos [BEq α] [Hashable α] (m : Raw α β) : WF m → 0
   | alter₀ _ => (Raw₀.alter _ _ _).2
   | constAlter₀ _ => (Raw₀.Const.alter _ _ _).2
 
-@[simp] theorem WF.empty [BEq α] [Hashable α] {c : Nat} : (Raw.empty c : Raw α β).WF :=
-  .empty₀
+@[simp] theorem WF.emptyWithCapacity [BEq α] [Hashable α] {c : Nat} : (Raw.emptyWithCapacity c : Raw α β).WF :=
+  .emptyWithCapacity₀
 
-@[simp] theorem WF.emptyc [BEq α] [Hashable α] : (∅ : Raw α β).WF :=
-  .empty
+@[simp] theorem WF.empty [BEq α] [Hashable α] : (∅ : Raw α β).WF :=
+  .emptyWithCapacity
+
+set_option linter.missingDocs false in
+@[deprecated WF.empty (since := "2025-03-12")]
+abbrev WF.emptyc := @WF.empty
 
 theorem WF.insert [BEq α] [Hashable α] {m : Raw α β} {a : α} {b : β a} (h : m.WF) :
     (m.insert a b).WF := by

src/Std/Data/DHashMap/RawLemmas.lean

@@ -67,12 +67,16 @@ open Internal.Raw₀ Internal.Raw
 variable {m : Raw α β}
 
 @[simp]
-theorem size_empty {c} : (empty c : Raw α β).size = 0 := by
-  simp_to_raw using Raw₀.size_empty
+theorem size_emptyWithCapacity {c} : (emptyWithCapacity c : Raw α β).size = 0 := by
+  simp_to_raw using Raw₀.size_emptyWithCapacity
 
 @[simp]
-theorem size_emptyc : (∅ : Raw α β).size = 0 :=
-  size_empty
+theorem size_empty : (∅ : Raw α β).size = 0 :=
+  size_emptyWithCapacity
+
+set_option linter.missingDocs false in
+@[deprecated size_empty (since := "2025-03-11")]
+abbrev size_emptyc := @size_empty
 
 theorem isEmpty_eq_size_eq_zero : m.isEmpty = (m.size == 0) := by
   simp [isEmpty]
@@ -80,12 +84,16 @@ theorem isEmpty_eq_size_eq_zero : m.isEmpty = (m.size == 0) := by
 variable [BEq α] [Hashable α]
 
 @[simp]
-theorem isEmpty_empty {c} : (empty c : Raw α β).isEmpty := by
-  simp_to_raw using Raw₀.isEmpty_empty
+theorem isEmpty_emptyWithCapacity {c} : (emptyWithCapacity c : Raw α β).isEmpty := by
+  simp_to_raw using Raw₀.isEmpty_emptyWithCapacity
 
 @[simp]
-theorem isEmpty_emptyc : (∅ : Raw α β).isEmpty :=
-  isEmpty_empty
+theorem isEmpty_empty : (∅ : Raw α β).isEmpty :=
+  isEmpty_emptyWithCapacity
+
+set_option linter.missingDocs false in
+@[deprecated isEmpty_empty (since := "2025-03-11")]
+abbrev isEmpty_emptyc := @isEmpty_empty
 
 @[simp]
 theorem isEmpty_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} :
@@ -103,17 +111,25 @@ theorem mem_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} (hab :
     a ∈ m ↔ b ∈ m := by
   simp [mem_iff_contains, contains_congr h hab]
 
-@[simp] theorem contains_empty {a : α} {c} : (empty c : Raw α β).contains a = false := by
-  simp_to_raw using Raw₀.contains_empty
+@[simp] theorem contains_emptyWithCapacity {a : α} {c} : (emptyWithCapacity c : Raw α β).contains a = false := by
+  simp_to_raw using Raw₀.contains_emptyWithCapacity
 
-@[simp] theorem not_mem_empty {a : α} {c} : ¬a ∈ (empty c : Raw α β) := by
+@[simp] theorem not_mem_emptyWithCapacity {a : α} {c} : ¬a ∈ (emptyWithCapacity c : Raw α β) := by
   simp [mem_iff_contains]
 
-@[simp] theorem contains_emptyc {a : α} : (∅ : Raw α β).contains a = false :=
-  contains_empty
+@[simp] theorem contains_empty {a : α} : (∅ : Raw α β).contains a = false :=
+  contains_emptyWithCapacity
 
-@[simp] theorem not_mem_emptyc {a : α} : ¬a ∈ (∅ : Raw α β) :=
-  not_mem_empty
+set_option linter.missingDocs false in
+@[deprecated contains_empty (since := "2025-03-11")]
+abbrev contains_emptyc := @contains_empty
+
+@[simp] theorem not_mem_empty {a : α} : ¬a ∈ (∅ : Raw α β) :=
+  not_mem_emptyWithCapacity
+
+set_option linter.missingDocs false in
+@[deprecated not_mem_empty (since := "2025-03-11")]
+abbrev not_mem_emptyc := @not_mem_empty
 
 theorem contains_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
     m.isEmpty → m.contains a = false := by
@@ -187,13 +203,17 @@ theorem size_insert_le [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v
   simp_to_raw using Raw₀.size_insert_le ⟨m, _⟩ h
 
 @[simp]
-theorem erase_empty {k : α} {c : Nat} : (empty c : Raw α β).erase k = empty c := by
+theorem erase_emptyWithCapacity {k : α} {c : Nat} : (emptyWithCapacity c : Raw α β).erase k = emptyWithCapacity c := by
   rw [erase_eq (by wf_trivial)]
-  exact congrArg Subtype.val Raw₀.erase_empty
+  exact congrArg Subtype.val Raw₀.erase_emptyWithCapacity
 
 @[simp]
-theorem erase_emptyc {k : α} : (∅ : Raw α β).erase k = ∅ :=
-  erase_empty
+theorem erase_empty {k : α} : (∅ : Raw α β).erase k = ∅ :=
+  erase_emptyWithCapacity
+
+set_option linter.missingDocs false in
+@[deprecated erase_empty (since := "2025-03-11")]
+abbrev erase_emptyc := @erase_empty
 
 @[simp]
 theorem isEmpty_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
@@ -252,12 +272,16 @@ theorem containsThenInsertIfNew_snd (h : m.WF) {k : α} {v : β k} :
   simp_to_raw using congrArg Subtype.val (Raw₀.containsThenInsertIfNew_snd _)
 
 @[simp]
-theorem get?_empty [LawfulBEq α] {a : α} {c} : (empty c : Raw α β).get? a = none := by
-  simp_to_raw using Raw₀.get?_empty
+theorem get?_emptyWithCapacity [LawfulBEq α] {a : α} {c} : (emptyWithCapacity c : Raw α β).get? a = none := by
+  simp_to_raw using Raw₀.get?_emptyWithCapacity
 
 @[simp]
-theorem get?_emptyc [LawfulBEq α] {a : α} : (∅ : Raw α β).get? a = none :=
-  get?_empty
+theorem get?_empty [LawfulBEq α] {a : α} : (∅ : Raw α β).get? a = none :=
+  get?_emptyWithCapacity
+
+set_option linter.missingDocs false in
+@[deprecated get?_empty (since := "2025-03-11")]
+abbrev get?_emptyc := @get?_empty
 
 theorem get?_of_isEmpty [LawfulBEq α] (h : m.WF) {a : α} : m.isEmpty = true → m.get? a = none := by
   simp_to_raw using Raw₀.get?_of_isEmpty ⟨m, _⟩
@@ -295,12 +319,16 @@ namespace Const
 variable {β : Type v} {m : DHashMap.Raw α (fun _ => β)} (h : m.WF)
 
 @[simp]
-theorem get?_empty {a : α} {c} : get? (empty c : Raw α (fun _ => β)) a = none := by
-  simp_to_raw using Raw₀.Const.get?_empty
+theorem get?_emptyWithCapacity {a : α} {c} : get? (emptyWithCapacity c : Raw α (fun _ => β)) a = none := by
+  simp_to_raw using Raw₀.Const.get?_emptyWithCapacity
 
 @[simp]
-theorem get?_emptyc {a : α} : get? (∅ : Raw α (fun _ => β)) a = none :=
-  get?_empty
+theorem get?_empty {a : α} : get? (∅ : Raw α (fun _ => β)) a = none :=
+  get?_emptyWithCapacity
+
+set_option linter.missingDocs false in
+@[deprecated get?_empty (since := "2025-03-11")]
+abbrev get?_emptyc := @get?_empty
 
 theorem get?_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
     m.isEmpty = true → get? m a = none := by
@@ -399,14 +427,18 @@ theorem get_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} (hab :
 end Const
 
 @[simp]
-theorem get!_empty [LawfulBEq α] {a : α} [Inhabited (β a)] {c} :
-    (empty c : Raw α β).get! a = default := by
-  simp_to_raw using Raw₀.get!_empty
+theorem get!_emptyWithCapacity [LawfulBEq α] {a : α} [Inhabited (β a)] {c} :
+    (emptyWithCapacity c : Raw α β).get! a = default := by
+  simp_to_raw using Raw₀.get!_emptyWithCapacity
 
 @[simp]
-theorem get!_emptyc [LawfulBEq α] {a : α} [Inhabited (β a)] :
+theorem get!_empty [LawfulBEq α] {a : α} [Inhabited (β a)] :
     (∅ : Raw α β).get! a = default :=
-  get!_empty
+  get!_emptyWithCapacity
+
+set_option linter.missingDocs false in
+@[deprecated get!_empty (since := "2025-03-11")]
+abbrev get!_emptyc := @get!_empty
 
 theorem get!_of_isEmpty [LawfulBEq α] (h : m.WF) {a : α} [Inhabited (β a)] :
     m.isEmpty = true → m.get! a = default := by
@@ -459,12 +491,16 @@ namespace Const
 variable {β : Type v} {m : DHashMap.Raw α (fun _ => β)} (h : m.WF)
 
 @[simp]
-theorem get!_empty [Inhabited β] {a : α} {c} : get! (empty c : Raw α (fun _ => β)) a = default := by
-  simp_to_raw using Raw₀.Const.get!_empty
+theorem get!_emptyWithCapacity [Inhabited β] {a : α} {c} : get! (emptyWithCapacity c : Raw α (fun _ => β)) a = default := by
+  simp_to_raw using Raw₀.Const.get!_emptyWithCapacity
 
 @[simp]
-theorem get!_emptyc [Inhabited β] {a : α} : get! (∅ : Raw α (fun _ => β)) a = default :=
-  get!_empty
+theorem get!_empty [Inhabited β] {a : α} : get! (∅ : Raw α (fun _ => β)) a = default :=
+  get!_emptyWithCapacity
+
+set_option linter.missingDocs false in
+@[deprecated get!_empty (since := "2025-03-11")]
+abbrev get!_emptyc := @get!_empty
 
 theorem get!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {a : α} :
     m.isEmpty = true → get! m a = default := by
@@ -524,14 +560,18 @@ theorem get!_congr [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {
 end Const
 
 @[simp]
-theorem getD_empty [LawfulBEq α] {a : α} {fallback : β a} {c} :
-    (empty c : Raw α β).getD a fallback = fallback := by
-  simp_to_raw using Raw₀.getD_empty
+theorem getD_emptyWithCapacity [LawfulBEq α] {a : α} {fallback : β a} {c} :
+    (emptyWithCapacity c : Raw α β).getD a fallback = fallback := by
+  simp_to_raw using Raw₀.getD_emptyWithCapacity
 
 @[simp]
-theorem getD_emptyc [LawfulBEq α] {a : α} {fallback : β a} :
+theorem getD_empty [LawfulBEq α] {a : α} {fallback : β a} :
     (∅ : Raw α β).getD a fallback = fallback :=
-  getD_empty
+  getD_emptyWithCapacity
+
+set_option linter.missingDocs false in
+@[deprecated getD_empty (since := "2025-03-11")]
+abbrev getD_emptyc := @getD_empty
 
 theorem getD_of_isEmpty [LawfulBEq α] (h : m.WF) {a : α} {fallback : β a} :
     m.isEmpty = true → m.getD a fallback = fallback := by
@@ -589,13 +629,17 @@ namespace Const
 variable {β : Type v} {m : DHashMap.Raw α (fun _ => β)} (h : m.WF)
 
 @[simp]
-theorem getD_empty {a : α} {fallback : β} {c} :
-    getD (empty c : Raw α (fun _ => β)) a fallback = fallback := by
-  simp_to_raw using Raw₀.Const.getD_empty
+theorem getD_emptyWithCapacity {a : α} {fallback : β} {c} :
+    getD (emptyWithCapacity c : Raw α (fun _ => β)) a fallback = fallback := by
+  simp_to_raw using Raw₀.Const.getD_emptyWithCapacity
 
 @[simp]
-theorem getD_emptyc {a : α} {fallback : β} : getD (∅ : Raw α (fun _ => β)) a fallback = fallback :=
-  getD_empty
+theorem getD_empty {a : α} {fallback : β} : getD (∅ : Raw α (fun _ => β)) a fallback = fallback :=
+  getD_emptyWithCapacity
+
+set_option linter.missingDocs false in
+@[deprecated getD_empty (since := "2025-03-11")]
+abbrev getD_emptyc := @getD_empty
 
 theorem getD_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {fallback : β} :
     m.isEmpty = true → getD m a fallback = fallback := by
@@ -658,13 +702,17 @@ theorem getD_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} {fall
 end Const
 
 @[simp]
-theorem getKey?_empty {a : α} {c} :
-    (empty c : Raw α β).getKey? a = none := by
-  simp_to_raw using Raw₀.getKey?_empty
+theorem getKey?_emptyWithCapacity {a : α} {c} :
+    (emptyWithCapacity c : Raw α β).getKey? a = none := by
+  simp_to_raw using Raw₀.getKey?_emptyWithCapacity
 
 @[simp]
-theorem getKey?_emptyc {a : α} : (∅ : Raw α β).getKey? a = none :=
-  getKey?_empty
+theorem getKey?_empty {a : α} : (∅ : Raw α β).getKey? a = none :=
+  getKey?_emptyWithCapacity
+
+set_option linter.missingDocs false in
+@[deprecated getKey?_empty (since := "2025-03-11")]
+abbrev getKey?_emptyc := @getKey?_empty
 
 theorem getKey?_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
     m.isEmpty = true → m.getKey? a = none := by
@@ -752,14 +800,18 @@ theorem getKey_eq [LawfulBEq α] (h : m.WF) {k : α} (h') :
   simp_to_raw using Raw₀.getKey_eq
 
 @[simp]
-theorem getKey!_empty [Inhabited α] {a : α} {c} :
-    (empty c : Raw α β).getKey! a = default := by
-  simp_to_raw using Raw₀.getKey!_empty
+theorem getKey!_emptyWithCapacity [Inhabited α] {a : α} {c} :
+    (emptyWithCapacity c : Raw α β).getKey! a = default := by
+  simp_to_raw using Raw₀.getKey!_emptyWithCapacity
 
 @[simp]
-theorem getKey!_emptyc [Inhabited α] {a : α} :
+theorem getKey!_empty [Inhabited α] {a : α} :
     (∅ : Raw α β).getKey! a = default :=
-  getKey!_empty
+  getKey!_emptyWithCapacity
+
+set_option linter.missingDocs false in
+@[deprecated getKey!_empty (since := "2025-03-11")]
+abbrev getKey!_emptyc := @getKey!_empty
 
 theorem getKey!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {a : α} :
     m.isEmpty = true → m.getKey! a = default := by
@@ -823,14 +875,18 @@ theorem getKey!_eq_of_mem [LawfulBEq α] [Inhabited α] (h : m.WF) {k : α} :
   simpa only [mem_iff_contains] using getKey!_eq_of_contains h
 
 @[simp]
-theorem getKeyD_empty {a fallback : α} {c} :
-    (empty c : Raw α β).getKeyD a fallback = fallback := by
-  simp_to_raw using Raw₀.getKeyD_empty
+theorem getKeyD_emptyWithCapacity {a fallback : α} {c} :
+    (emptyWithCapacity c : Raw α β).getKeyD a fallback = fallback := by
+  simp_to_raw using Raw₀.getKeyD_emptyWithCapacity
 
 @[simp]
-theorem getKeyD_emptyc {a fallback : α} :
+theorem getKeyD_empty {a fallback : α} :
     (∅ : Raw α β).getKeyD a fallback = fallback :=
-  getKeyD_empty
+  getKeyD_emptyWithCapacity
+
+set_option linter.missingDocs false in
+@[deprecated getKeyD_empty (since := "2025-03-11")]
+abbrev getKeyD_emptyc := @getKeyD_empty
 
 theorem getKeyD_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a fallback : α} :
     m.isEmpty = true → m.getKeyD a fallback = fallback := by
@@ -1855,24 +1911,24 @@ open Internal.Raw Internal.Raw₀
 theorem ofList_nil :
     ofList ([] : List ((a : α) × (β a))) = ∅ := by
   simp_to_raw
-  rw [Raw₀.insertMany_empty_list_nil]
+  rw [Raw₀.insertMany_emptyWithCapacity_list_nil]
 
 @[simp]
 theorem ofList_singleton {k : α} {v : β k} :
     ofList [⟨k, v⟩] = (∅ : Raw α β).insert k v := by
   simp_to_raw
-  rw [Raw₀.insertMany_empty_list_singleton]
+  rw [Raw₀.insertMany_emptyWithCapacity_list_singleton]
 
 theorem ofList_cons [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} {tl : List ((a : α) × (β a))} :
     ofList (⟨k, v⟩ :: tl) = ((∅ : Raw α β).insert k v).insertMany tl := by
   simp_to_raw
-  rw [Raw₀.insertMany_empty_list_cons]
+  rw [Raw₀.insertMany_emptyWithCapacity_list_cons]
 
 @[simp]
 theorem contains_ofList [EquivBEq α] [LawfulHashable α]
     {l : List ((a : α) × β a)} {k : α} :
     (ofList l).contains k = (l.map Sigma.fst).contains k := by
-  simp_to_raw using Raw₀.contains_insertMany_empty_list
+  simp_to_raw using Raw₀.contains_insertMany_emptyWithCapacity_list
 
 @[simp]
 theorem mem_ofList [EquivBEq α] [LawfulHashable α]
@@ -1884,14 +1940,14 @@ theorem get?_ofList_of_contains_eq_false [LawfulBEq α]
     {l : List ((a : α) × β a)} {k : α}
     (contains_eq_false : (l.map Sigma.fst).contains k = false) :
     (ofList l).get? k = none := by
-  simp_to_raw using Raw₀.get?_insertMany_empty_list_of_contains_eq_false
+  simp_to_raw using Raw₀.get?_insertMany_emptyWithCapacity_list_of_contains_eq_false
 
 theorem get?_ofList_of_mem [LawfulBEq α]
     {l : List ((a : α) × β a)} {k k' : α} (k_beq : k == k') {v : β k}
     (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
     (mem : ⟨k, v⟩ ∈ l) :
     (ofList l).get? k' = some (cast (by congr; apply LawfulBEq.eq_of_beq k_beq) v) := by
-  simp_to_raw using Raw₀.get?_insertMany_empty_list_of_mem
+  simp_to_raw using Raw₀.get?_insertMany_emptyWithCapacity_list_of_mem
 
 theorem get_ofList_of_mem [LawfulBEq α]
     {l : List ((a : α) × β a)} {k k' : α} (k_beq : k == k') {v : β k}
@@ -1899,39 +1955,39 @@ theorem get_ofList_of_mem [LawfulBEq α]
     (mem : ⟨k, v⟩ ∈ l)
     {h} :
     (ofList l).get k' h = cast (by congr; apply LawfulBEq.eq_of_beq k_beq) v := by
-  simp_to_raw using Raw₀.get_insertMany_empty_list_of_mem
+  simp_to_raw using Raw₀.get_insertMany_emptyWithCapacity_list_of_mem
 
 theorem get!_ofList_of_contains_eq_false [LawfulBEq α]
     {l : List ((a : α) × β a)} {k : α} [Inhabited (β k)]
     (contains_eq_false : (l.map Sigma.fst).contains k = false) :
     (ofList l).get! k = default := by
-  simp_to_raw using get!_insertMany_empty_list_of_contains_eq_false
+  simp_to_raw using Raw₀.get!_insertMany_emptyWithCapacity_list_of_contains_eq_false
 
 theorem get!_ofList_of_mem [LawfulBEq α]
     {l : List ((a : α) × β a)} {k k' : α} (k_beq : k == k') {v : β k} [Inhabited (β k')]
     (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
     (mem : ⟨k, v⟩ ∈ l) :
     (ofList l).get! k' = cast (by congr; apply LawfulBEq.eq_of_beq k_beq) v := by
-  simp_to_raw using Raw₀.get!_insertMany_empty_list_of_mem
+  simp_to_raw using Raw₀.get!_insertMany_emptyWithCapacity_list_of_mem
 
 theorem getD_ofList_of_contains_eq_false [LawfulBEq α]
     {l : List ((a : α) × β a)} {k : α} {fallback : β k}
     (contains_eq_false : (l.map Sigma.fst).contains k = false) :
     (ofList l).getD k fallback = fallback := by
-  simp_to_raw using Raw₀.getD_insertMany_empty_list_of_contains_eq_false
+  simp_to_raw using Raw₀.getD_insertMany_emptyWithCapacity_list_of_contains_eq_false
 
 theorem getD_ofList_of_mem [LawfulBEq α]
     {l : List ((a : α) × β a)} {k k' : α} (k_beq : k == k') {v : β k} {fallback : β k'}
     (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
     (mem : ⟨k, v⟩ ∈ l) :
     (ofList l).getD k' fallback = cast (by congr; apply LawfulBEq.eq_of_beq k_beq) v := by
-  simp_to_raw using Raw₀.getD_insertMany_empty_list_of_mem
+  simp_to_raw using Raw₀.getD_insertMany_emptyWithCapacity_list_of_mem
 
 theorem getKey?_ofList_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
     {l : List ((a : α) × β a)} {k : α}
     (contains_eq_false : (l.map Sigma.fst).contains k = false) :
     (ofList l).getKey? k = none := by
-  simp_to_raw using Raw₀.getKey?_insertMany_empty_list_of_contains_eq_false
+  simp_to_raw using Raw₀.getKey?_insertMany_emptyWithCapacity_list_of_contains_eq_false
 
 theorem getKey?_ofList_of_mem [EquivBEq α] [LawfulHashable α]
     {l : List ((a : α) × β a)}
@@ -1939,7 +1995,7 @@ theorem getKey?_ofList_of_mem [EquivBEq α] [LawfulHashable α]
     (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
     (mem : k ∈ l.map Sigma.fst) :
     (ofList l).getKey? k' = some k := by
-  simp_to_raw using Raw₀.getKey?_insertMany_empty_list_of_mem
+  simp_to_raw using Raw₀.getKey?_insertMany_emptyWithCapacity_list_of_mem
 
 theorem getKey_ofList_of_mem [EquivBEq α] [LawfulHashable α]
     {l : List ((a : α) × β a)}
@@ -1948,13 +2004,13 @@ theorem getKey_ofList_of_mem [EquivBEq α] [LawfulHashable α]
     (mem : k ∈ l.map Sigma.fst)
     {h'} :
     (ofList l).getKey k' h' = k := by
-  simp_to_raw using Raw₀.getKey_insertMany_empty_list_of_mem
+  simp_to_raw using Raw₀.getKey_insertMany_emptyWithCapacity_list_of_mem
 
 theorem getKey!_ofList_of_contains_eq_false [EquivBEq α] [LawfulHashable α] [Inhabited α]
     {l : List ((a : α) × β a)} {k : α}
     (contains_eq_false : (l.map Sigma.fst).contains k = false) :
     (ofList l).getKey! k = default := by
-  simp_to_raw using Raw₀.getKey!_insertMany_empty_list_of_contains_eq_false
+  simp_to_raw using Raw₀.getKey!_insertMany_emptyWithCapacity_list_of_contains_eq_false
 
 theorem getKey!_ofList_of_mem [EquivBEq α] [LawfulHashable α] [Inhabited α]
     {l : List ((a : α) × β a)}
@@ -1962,13 +2018,13 @@ theorem getKey!_ofList_of_mem [EquivBEq α] [LawfulHashable α] [Inhabited α]
     (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
     (mem : k ∈ l.map Sigma.fst) :
     (ofList l).getKey! k' = k := by
-  simp_to_raw using Raw₀.getKey!_insertMany_empty_list_of_mem
+  simp_to_raw using Raw₀.getKey!_insertMany_emptyWithCapacity_list_of_mem
 
 theorem getKeyD_ofList_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
     {l : List ((a : α) × β a)} {k fallback : α}
     (contains_eq_false : (l.map Sigma.fst).contains k = false) :
     (ofList l).getKeyD k fallback = fallback := by
-  simp_to_raw using Raw₀.getKeyD_insertMany_empty_list_of_contains_eq_false
+  simp_to_raw using Raw₀.getKeyD_insertMany_emptyWithCapacity_list_of_contains_eq_false
 
 theorem getKeyD_ofList_of_mem [EquivBEq α] [LawfulHashable α]
     {l : List ((a : α) × β a)}
@@ -1976,23 +2032,23 @@ theorem getKeyD_ofList_of_mem [EquivBEq α] [LawfulHashable α]
     (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
     (mem : k ∈ l.map Sigma.fst) :
     (ofList l).getKeyD k' fallback = k := by
-  simp_to_raw using Raw₀.getKeyD_insertMany_empty_list_of_mem
+  simp_to_raw using Raw₀.getKeyD_insertMany_emptyWithCapacity_list_of_mem
 
 theorem size_ofList [EquivBEq α] [LawfulHashable α]
     {l : List ((a : α) × β a)} (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) :
     (ofList l).size = l.length := by
-  simp_to_raw using Raw₀.size_insertMany_empty_list
+  simp_to_raw using Raw₀.size_insertMany_emptyWithCapacity_list
 
 theorem size_ofList_le [EquivBEq α] [LawfulHashable α]
     {l : List ((a : α) × β a)} :
     (ofList l).size ≤ l.length := by
-  simp_to_raw using Raw₀.size_insertMany_empty_list_le
+  simp_to_raw using Raw₀.size_insertMany_emptyWithCapacity_list_le
 
 @[simp]
 theorem isEmpty_ofList [EquivBEq α] [LawfulHashable α]
     {l : List ((a : α) × β a)} :
     (ofList l).isEmpty = l.isEmpty := by
-  simp_to_raw using Raw₀.isEmpty_insertMany_empty_list
+  simp_to_raw using Raw₀.isEmpty_insertMany_emptyWithCapacity_list
 
 namespace Const
 
@@ -2013,13 +2069,13 @@ theorem ofList_singleton {k : α} {v : β} :
 theorem ofList_cons {k : α} {v : β} {tl : List (α × β)} :
     ofList (⟨k, v⟩ :: tl) = insertMany ((∅ : Raw α (fun _ => β)).insert k v) tl := by
   simp_to_raw
-  rw [Raw₀.Const.insertMany_empty_list_cons]
+  rw [Raw₀.Const.insertMany_emptyWithCapacity_list_cons]
 
 @[simp]
 theorem contains_ofList [EquivBEq α] [LawfulHashable α]
     {l : List (α × β)} {k : α} :
     (ofList l).contains k = (l.map Prod.fst).contains k := by
-  simp_to_raw using Raw₀.Const.contains_insertMany_empty_list
+  simp_to_raw using Raw₀.Const.contains_insertMany_emptyWithCapacity_list
 
 @[simp]
 theorem mem_ofList [EquivBEq α] [LawfulHashable α]
@@ -2031,14 +2087,14 @@ theorem get?_ofList_of_contains_eq_false [LawfulBEq α]
     {l : List (α × β)} {k : α}
     (contains_eq_false : (l.map Prod.fst).contains k = false) :
     get? (ofList l) k = none := by
-  simp_to_raw using Raw₀.Const.get?_insertMany_empty_list_of_contains_eq_false
+  simp_to_raw using Raw₀.Const.get?_insertMany_emptyWithCapacity_list_of_contains_eq_false
 
 theorem get?_ofList_of_mem [LawfulBEq α]
     {l : List (α × β)} {k k' : α} (k_beq : k == k') {v : β}
     (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
     (mem : ⟨k, v⟩ ∈ l) :
     get? (ofList l) k' = some v := by
-  simp_to_raw using Raw₀.Const.get?_insertMany_empty_list_of_mem
+  simp_to_raw using Raw₀.Const.get?_insertMany_emptyWithCapacity_list_of_mem
 
 theorem get_ofList_of_mem [LawfulBEq α]
     {l : List (α × β)} {k k' : α} (k_beq : k == k') {v : β}
@@ -2046,39 +2102,39 @@ theorem get_ofList_of_mem [LawfulBEq α]
     (mem : ⟨k, v⟩ ∈ l)
     {h} :
     get (ofList l) k' h = v := by
-  simp_to_raw using Raw₀.Const.get_insertMany_empty_list_of_mem
+  simp_to_raw using Raw₀.Const.get_insertMany_emptyWithCapacity_list_of_mem
 
 theorem get!_ofList_of_contains_eq_false [LawfulBEq α]
     {l : List (α × β)} {k : α} [Inhabited β]
     (contains_eq_false : (l.map Prod.fst).contains k = false) :
     get! (ofList l) k = default := by
-  simp_to_raw using Raw₀.Const.get!_insertMany_empty_list_of_contains_eq_false
+  simp_to_raw using Raw₀.Const.get!_insertMany_emptyWithCapacity_list_of_contains_eq_false
 
 theorem get!_ofList_of_mem [LawfulBEq α]
     {l : List (α × β)} {k k' : α} (k_beq : k == k') {v : β} [Inhabited β]
     (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
     (mem : ⟨k, v⟩ ∈ l) :
     get! (ofList l) k' = v := by
-  simp_to_raw using Raw₀.Const.get!_insertMany_empty_list_of_mem
+  simp_to_raw using Raw₀.Const.get!_insertMany_emptyWithCapacity_list_of_mem
 
 theorem getD_ofList_of_contains_eq_false [LawfulBEq α]
     {l : List (α × β)} {k : α} {fallback : β}
     (contains_eq_false : (l.map Prod.fst).contains k = false) :
     getD (ofList l) k fallback = fallback := by
-  simp_to_raw using Raw₀.Const.getD_insertMany_empty_list_of_contains_eq_false
+  simp_to_raw using Raw₀.Const.getD_insertMany_emptyWithCapacity_list_of_contains_eq_false
 
 theorem getD_ofList_of_mem [LawfulBEq α]
     {l : List (α × β)} {k k' : α} (k_beq : k == k') {v : β} {fallback : β}
     (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
     (mem : ⟨k, v⟩ ∈ l) :
     getD (ofList l) k' fallback = v := by
-  simp_to_raw using Raw₀.Const.getD_insertMany_empty_list_of_mem
+  simp_to_raw using Raw₀.Const.getD_insertMany_emptyWithCapacity_list_of_mem
 
 theorem getKey?_ofList_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
     {l : List (α × β)} {k : α}
     (contains_eq_false : (l.map Prod.fst).contains k = false) :
     (ofList l).getKey? k = none := by
-  simp_to_raw using Raw₀.Const.getKey?_insertMany_empty_list_of_contains_eq_false
+  simp_to_raw using Raw₀.Const.getKey?_insertMany_emptyWithCapacity_list_of_contains_eq_false
 
 theorem getKey?_ofList_of_mem [EquivBEq α] [LawfulHashable α]
     {l : List (α × β)}
@@ -2086,7 +2142,7 @@ theorem getKey?_ofList_of_mem [EquivBEq α] [LawfulHashable α]
     (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
     (mem : k ∈ l.map Prod.fst) :
     (ofList l).getKey? k' = some k := by
-  simp_to_raw using Raw₀.Const.getKey?_insertMany_empty_list_of_mem
+  simp_to_raw using Raw₀.Const.getKey?_insertMany_emptyWithCapacity_list_of_mem
 
 theorem getKey_ofList_of_mem [EquivBEq α] [LawfulHashable α]
     {l : List (α × β)}
@@ -2095,13 +2151,13 @@ theorem getKey_ofList_of_mem [EquivBEq α] [LawfulHashable α]
     (mem : k ∈ l.map Prod.fst)
     {h'} :
     (ofList l).getKey k' h' = k := by
-  simp_to_raw using Raw₀.Const.getKey_insertMany_empty_list_of_mem
+  simp_to_raw using Raw₀.Const.getKey_insertMany_emptyWithCapacity_list_of_mem
 
 theorem getKey!_ofList_of_contains_eq_false [EquivBEq α] [LawfulHashable α] [Inhabited α]
     {l : List (α × β)} {k : α}
     (contains_eq_false : (l.map Prod.fst).contains k = false) :
     (ofList l).getKey! k = default := by
-  simp_to_raw using Raw₀.Const.getKey!_insertMany_empty_list_of_contains_eq_false
+  simp_to_raw using Raw₀.Const.getKey!_insertMany_emptyWithCapacity_list_of_contains_eq_false
 
 theorem getKey!_ofList_of_mem [EquivBEq α] [LawfulHashable α] [Inhabited α]
     {l : List (α × β)}
@@ -2109,13 +2165,13 @@ theorem getKey!_ofList_of_mem [EquivBEq α] [LawfulHashable α] [Inhabited α]
     (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
     (mem : k ∈ l.map Prod.fst) :
     (ofList l).getKey! k' = k := by
-  simp_to_raw using Raw₀.Const.getKey!_insertMany_empty_list_of_mem
+  simp_to_raw using Raw₀.Const.getKey!_insertMany_emptyWithCapacity_list_of_mem
 
 theorem getKeyD_ofList_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
     {l : List (α × β)} {k fallback : α}
     (contains_eq_false : (l.map Prod.fst).contains k = false) :
     (ofList l).getKeyD k fallback = fallback := by
-  simp_to_raw using Raw₀.Const.getKeyD_insertMany_empty_list_of_contains_eq_false
+  simp_to_raw using Raw₀.Const.getKeyD_insertMany_emptyWithCapacity_list_of_contains_eq_false
 
 theorem getKeyD_ofList_of_mem [EquivBEq α] [LawfulHashable α]
     {l : List (α × β)}
@@ -2123,23 +2179,23 @@ theorem getKeyD_ofList_of_mem [EquivBEq α] [LawfulHashable α]
     (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
     (mem : k ∈ l.map Prod.fst) :
     (ofList l).getKeyD k' fallback = k := by
-  simp_to_raw using Raw₀.Const.getKeyD_insertMany_empty_list_of_mem
+  simp_to_raw using Raw₀.Const.getKeyD_insertMany_emptyWithCapacity_list_of_mem
 
 theorem size_ofList [EquivBEq α] [LawfulHashable α]
     {l : List (α × β)} (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) :
     (ofList l).size = l.length := by
-  simp_to_raw using Raw₀.Const.size_insertMany_empty_list
+  simp_to_raw using Raw₀.Const.size_insertMany_emptyWithCapacity_list
 
 theorem size_ofList_le [EquivBEq α] [LawfulHashable α]
     {l : List (α × β)} :
     (ofList l).size ≤ l.length := by
-  simp_to_raw using Raw₀.Const.size_insertMany_empty_list_le
+  simp_to_raw using Raw₀.Const.size_insertMany_emptyWithCapacity_list_le
 
 @[simp]
 theorem isEmpty_ofList [EquivBEq α] [LawfulHashable α]
     {l : List (α × β)} :
     (ofList l).isEmpty = l.isEmpty := by
-  simp_to_raw using Raw₀.Const.isEmpty_insertMany_empty_list
+  simp_to_raw using Raw₀.Const.isEmpty_insertMany_emptyWithCapacity_list
 
 @[simp]
 theorem unitOfList_nil :
@@ -2156,13 +2212,13 @@ theorem unitOfList_singleton {k : α} :
 theorem unitOfList_cons {hd : α} {tl : List α} :
     unitOfList (hd :: tl) = insertManyIfNewUnit ((∅ : Raw α (fun _ => Unit)).insertIfNew hd ()) tl := by
   simp_to_raw
-  rw [Raw₀.Const.insertManyIfNewUnit_empty_list_cons]
+  rw [Raw₀.Const.insertManyIfNewUnit_emptyWithCapacity_list_cons]
 
 @[simp]
 theorem contains_unitOfList [EquivBEq α] [LawfulHashable α]
     {l : List α} {k : α} :
     (unitOfList l).contains k = l.contains k := by
-  simp_to_raw using Raw₀.Const.contains_insertManyIfNewUnit_empty_list
+  simp_to_raw using Raw₀.Const.contains_insertManyIfNewUnit_emptyWithCapacity_list
 
 @[simp]
 theorem mem_unitOfList [EquivBEq α] [LawfulHashable α]
@@ -2173,13 +2229,13 @@ theorem mem_unitOfList [EquivBEq α] [LawfulHashable α]
 theorem getKey?_unitOfList_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
     {l : List α} {k : α} (contains_eq_false : l.contains k = false) :
     getKey? (unitOfList l) k = none := by
-  simp_to_raw using Raw₀.Const.getKey?_insertManyIfNewUnit_empty_list_of_contains_eq_false
+  simp_to_raw using Raw₀.Const.getKey?_insertManyIfNewUnit_emptyWithCapacity_list_of_contains_eq_false
 
 theorem getKey?_unitOfList_of_mem [EquivBEq α] [LawfulHashable α]
     {l : List α} {k k' : α} (k_beq : k == k')
     (distinct : l.Pairwise (fun a b => (a == b) = false)) (mem : k ∈ l) :
     getKey? (unitOfList l) k' = some k := by
-  simp_to_raw using Raw₀.Const.getKey?_insertManyIfNewUnit_empty_list_of_mem
+  simp_to_raw using Raw₀.Const.getKey?_insertManyIfNewUnit_emptyWithCapacity_list_of_mem
 
 theorem getKey_unitOfList_of_mem [EquivBEq α] [LawfulHashable α]
     {l : List α}
@@ -2187,56 +2243,56 @@ theorem getKey_unitOfList_of_mem [EquivBEq α] [LawfulHashable α]
     (distinct : l.Pairwise (fun a b => (a == b) = false))
     (mem : k ∈ l) {h'} :
     getKey (unitOfList l) k' h' = k := by
-  simp_to_raw using Raw₀.Const.getKey_insertManyIfNewUnit_empty_list_of_mem
+  simp_to_raw using Raw₀.Const.getKey_insertManyIfNewUnit_emptyWithCapacity_list_of_mem
 
 theorem getKey!_unitOfList_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
     [Inhabited α] {l : List α} {k : α}
     (contains_eq_false : l.contains k = false) :
     getKey! (unitOfList l) k = default := by
-  simp_to_raw using Raw₀.Const.getKey!_insertManyIfNewUnit_empty_list_of_contains_eq_false
+  simp_to_raw using Raw₀.Const.getKey!_insertManyIfNewUnit_emptyWithCapacity_list_of_contains_eq_false
 
 theorem getKey!_unitOfList_of_mem [EquivBEq α] [LawfulHashable α]
     [Inhabited α] {l : List α} {k k' : α} (k_beq : k == k')
     (distinct : l.Pairwise (fun a b => (a == b) = false))
     (mem : k ∈ l) :
     getKey! (unitOfList l) k' = k := by
-  simp_to_raw using Raw₀.Const.getKey!_insertManyIfNewUnit_empty_list_of_mem
+  simp_to_raw using Raw₀.Const.getKey!_insertManyIfNewUnit_emptyWithCapacity_list_of_mem
 
 theorem getKeyD_unitOfList_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
     {l : List α} {k fallback : α}
     (contains_eq_false : l.contains k = false) :
     getKeyD (unitOfList l) k fallback = fallback := by
-  simp_to_raw using Raw₀.Const.getKeyD_insertManyIfNewUnit_empty_list_of_contains_eq_false
+  simp_to_raw using Raw₀.Const.getKeyD_insertManyIfNewUnit_emptyWithCapacity_list_of_contains_eq_false
 
 theorem getKeyD_unitOfList_of_mem [EquivBEq α] [LawfulHashable α]
     {l : List α} {k k' fallback : α} (k_beq : k == k')
     (distinct : l.Pairwise (fun a b => (a == b) = false))
     (mem : k ∈ l ) :
     getKeyD (unitOfList l) k' fallback = k := by
-  simp_to_raw using Raw₀.Const.getKeyD_insertManyIfNewUnit_empty_list_of_mem
+  simp_to_raw using Raw₀.Const.getKeyD_insertManyIfNewUnit_emptyWithCapacity_list_of_mem
 
 theorem size_unitOfList [EquivBEq α] [LawfulHashable α]
     {l : List α}
     (distinct : l.Pairwise (fun a b => (a == b) = false)) :
     (unitOfList l).size = l.length := by
-  simp_to_raw using Raw₀.Const.size_insertManyIfNewUnit_empty_list
+  simp_to_raw using Raw₀.Const.size_insertManyIfNewUnit_emptyWithCapacity_list
 
 theorem size_unitOfList_le [EquivBEq α] [LawfulHashable α]
     {l : List α} :
     (unitOfList l).size ≤ l.length := by
-  simp_to_raw using Raw₀.Const.size_insertManyIfNewUnit_empty_list_le
+  simp_to_raw using Raw₀.Const.size_insertManyIfNewUnit_emptyWithCapacity_list_le
 
 @[simp]
 theorem isEmpty_unitOfList [EquivBEq α] [LawfulHashable α]
     {l : List α} :
     (unitOfList l).isEmpty = l.isEmpty := by
-  simp_to_raw using Raw₀.Const.isEmpty_insertManyIfNewUnit_empty_list
+  simp_to_raw using Raw₀.Const.isEmpty_insertManyIfNewUnit_emptyWithCapacity_list
 
 @[simp]
 theorem get?_unitOfList [EquivBEq α] [LawfulHashable α]
     {l : List α} {k : α} :
     get? (unitOfList l) k = if l.contains k then some () else none := by
-  simp_to_raw using Raw₀.Const.get?_insertManyIfNewUnit_empty_list
+  simp_to_raw using Raw₀.Const.get?_insertManyIfNewUnit_emptyWithCapacity_list
 
 @[simp]
 theorem get_unitOfList
@@ -3186,14 +3242,18 @@ end Const
 
 end Equiv
 
-theorem equiv_empty_iff_isEmpty [EquivBEq α] [LawfulHashable α] {c : Nat} (h : m.WF) :
-    m ~m empty c ↔ m.isEmpty :=
-  ⟨fun h' => (Raw₀.equiv_empty_iff_isEmpty ⟨m, h.size_buckets_pos⟩ h).mp h',
-    fun h' => (Raw₀.equiv_empty_iff_isEmpty ⟨m, h.size_buckets_pos⟩ h).mpr h'⟩
+theorem equiv_emptyWithCapacity_iff_isEmpty [EquivBEq α] [LawfulHashable α] {c : Nat} (h : m.WF) :
+    m ~m emptyWithCapacity c ↔ m.isEmpty :=
+  ⟨fun h' => (Raw₀.equiv_emptyWithCapacity_iff_isEmpty ⟨m, h.size_buckets_pos⟩ h).mp h',
+    fun h' => (Raw₀.equiv_emptyWithCapacity_iff_isEmpty ⟨m, h.size_buckets_pos⟩ h).mpr h'⟩
 
-theorem equiv_emptyc_iff_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) :
+theorem equiv_empty_iff_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) :
     m ~m ∅ ↔ m.isEmpty :=
-  equiv_empty_iff_isEmpty h
+  equiv_emptyWithCapacity_iff_isEmpty h
+
+set_option linter.missingDocs false in
+@[deprecated equiv_empty_iff_isEmpty (since := "2025-03-12")]
+abbrev equiv_emptyc_iff_isEmpty := @equiv_empty_iff_isEmpty
 
 theorem equiv_iff_toList_perm {m₁ m₂ : DHashMap.Raw α β} [EquivBEq α] [LawfulHashable α] :
     m₁ ~m m₂ ↔ m₁.toList.Perm m₂.toList :=

src/Std/Data/HashMap/Basic.lean

@@ -62,12 +62,15 @@ structure HashMap (α : Type u) (β : Type v) [BEq α] [Hashable α] where
 
 namespace HashMap
 
-@[inline, inherit_doc DHashMap.empty] def empty [BEq α] [Hashable α] (capacity := 8) :
+@[inline, inherit_doc DHashMap.empty] def emptyWithCapacity [BEq α] [Hashable α] (capacity := 8) :
     HashMap α β :=
-  ⟨DHashMap.empty capacity⟩
+  ⟨DHashMap.emptyWithCapacity capacity⟩
+
+@[deprecated emptyWithCapacity (since := "2025-03-12"), inherit_doc emptyWithCapacity]
+abbrev empty := @emptyWithCapacity
 
 instance [BEq α] [Hashable α] : EmptyCollection (HashMap α β) where
-  emptyCollection := empty
+  emptyCollection := emptyWithCapacity
 
 instance [BEq α] [Hashable α] : Inhabited (HashMap α β) where
   default := ∅
@@ -83,7 +86,7 @@ structure Equiv (m₁ m₂ : HashMap α β) where
     (b : β) : HashMap α β :=
   ⟨m.inner.insert a b⟩
 
-instance : Singleton (α × β) (HashMap α β) := ⟨fun ⟨a, b⟩ => HashMap.empty.insert a b⟩
+instance : Singleton (α × β) (HashMap α β) := ⟨fun ⟨a, b⟩ => (∅ : HashMap α β).insert a b⟩
 
 instance : Insert (α × β) (HashMap α β) := ⟨fun ⟨a, b⟩ s => s.insert a b⟩
 

src/Std/Data/HashMap/Lemmas.lean

@@ -33,12 +33,16 @@ private theorem ext {m m' : HashMap α β} : m.inner = m'.inner → m = m' := by
   cases m; cases m'; rintro rfl; rfl
 
 @[simp]
-theorem isEmpty_empty {c} : (empty c : HashMap α β).isEmpty :=
-  DHashMap.isEmpty_empty
+theorem isEmpty_emptyWithCapacity {c} : (emptyWithCapacity c : HashMap α β).isEmpty :=
+  DHashMap.isEmpty_emptyWithCapacity
 
 @[simp]
-theorem isEmpty_emptyc : (∅ : HashMap α β).isEmpty :=
-  DHashMap.isEmpty_emptyc
+theorem isEmpty_empty : (∅ : HashMap α β).isEmpty :=
+  DHashMap.isEmpty_empty
+
+set_option linter.missingDocs false in
+@[deprecated isEmpty_empty (since := "2025-03-12")]
+abbrev isEmpty_emptyc := @isEmpty_empty
 
 @[simp]
 theorem isEmpty_insert [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
@@ -56,17 +60,26 @@ theorem mem_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) :
     a ∈ m ↔ b ∈ m :=
   DHashMap.mem_congr hab
 
-@[simp] theorem contains_empty {a : α} {c} : (empty c : HashMap α β).contains a = false :=
+@[simp]
+theorem contains_emptyWithCapacity {a : α} {c} : (emptyWithCapacity c : HashMap α β).contains a = false :=
+  DHashMap.contains_emptyWithCapacity
+
+@[simp] theorem not_mem_emptyWithCapacity {a : α} {c} : ¬a ∈ (emptyWithCapacity c : HashMap α β) :=
+  DHashMap.not_mem_emptyWithCapacity
+
+@[simp] theorem contains_empty {a : α} : (∅ : HashMap α β).contains a = false :=
   DHashMap.contains_empty
 
-@[simp] theorem not_mem_empty {a : α} {c} : ¬a ∈ (empty c : HashMap α β) :=
+set_option linter.missingDocs false in
+@[deprecated contains_empty (since := "2025-03-12")]
+abbrev contains_emptyc := @contains_empty
+
+@[simp] theorem not_mem_empty {a : α} : ¬a ∈ (∅ : HashMap α β) :=
   DHashMap.not_mem_empty
 
-@[simp] theorem contains_emptyc {a : α} : (∅ : HashMap α β).contains a = false :=
-  DHashMap.contains_emptyc
-
-@[simp] theorem not_mem_emptyc {a : α} : ¬a ∈ (∅ : HashMap α β) :=
-  DHashMap.not_mem_emptyc
+set_option linter.missingDocs false in
+@[deprecated not_mem_empty (since := "2025-03-12")]
+abbrev not_mem_emptyc := @not_mem_empty
 
 theorem contains_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
     m.isEmpty → m.contains a = false :=
@@ -123,12 +136,16 @@ theorem mem_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β} : k
   simp
 
 @[simp]
-theorem size_empty {c} : (empty c : HashMap α β).size = 0 :=
-  DHashMap.size_empty
+theorem size_emptyWithCapacity {c} : (emptyWithCapacity c : HashMap α β).size = 0 :=
+  DHashMap.size_emptyWithCapacity
 
 @[simp]
-theorem size_emptyc : (∅ : HashMap α β).size = 0 :=
-  DHashMap.size_emptyc
+theorem size_empty : (∅ : HashMap α β).size = 0 :=
+  DHashMap.size_empty
+
+set_option linter.missingDocs false in
+@[deprecated size_empty (since := "2025-03-12")]
+abbrev size_emptyc := @size_empty
 
 theorem isEmpty_eq_size_eq_zero : m.isEmpty = (m.size == 0) :=
   DHashMap.isEmpty_eq_size_eq_zero
@@ -146,12 +163,16 @@ theorem size_insert_le [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
   DHashMap.size_insert_le
 
 @[simp]
-theorem erase_empty {a : α} {c : Nat} : (empty c : HashMap α β).erase a = empty c :=
-  ext DHashMap.erase_empty
+theorem erase_emptyWithCapacity {a : α} {c : Nat} : (emptyWithCapacity c : HashMap α β).erase a = emptyWithCapacity c :=
+  ext DHashMap.erase_emptyWithCapacity
 
 @[simp]
-theorem erase_emptyc {a : α} : (∅ : HashMap α β).erase a = ∅ :=
-  ext DHashMap.erase_emptyc
+theorem erase_empty {a : α} : (∅ : HashMap α β).erase a = ∅ :=
+  ext DHashMap.erase_empty
+
+set_option linter.missingDocs false in
+@[deprecated erase_empty (since := "2025-03-12")]
+abbrev erase_emptyc := @erase_empty
 
 @[simp]
 theorem isEmpty_erase [EquivBEq α] [LawfulHashable α] {k : α} :
@@ -209,12 +230,16 @@ theorem containsThenInsertIfNew_snd {k : α} {v : β} :
 @[simp] theorem get!_eq_getElem! [Inhabited β] {a : α} : get! m a = m[a]! := rfl
 
 @[simp]
-theorem getElem?_empty {a : α} {c} : (empty c : HashMap α β)[a]? = none :=
-  DHashMap.Const.get?_empty
+theorem getElem?_emptyWithCapacity {a : α} {c} : (emptyWithCapacity c : HashMap α β)[a]? = none :=
+  DHashMap.Const.get?_emptyWithCapacity
 
 @[simp]
-theorem getElem?_emptyc {a : α} : (∅ : HashMap α β)[a]? = none :=
-  DHashMap.Const.get?_emptyc
+theorem getElem?_empty {a : α} : (∅ : HashMap α β)[a]? = none :=
+  DHashMap.Const.get?_empty
+
+set_option linter.missingDocs false in
+@[deprecated getElem?_empty (since := "2025-03-12")]
+abbrev getElem?_emptyc := @getElem?_empty
 
 theorem getElem?_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
     m.isEmpty = true → m[a]? = none :=
@@ -275,12 +300,16 @@ theorem getElem_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b
   DHashMap.Const.get_congr hab (h' := h')
 
 @[simp]
-theorem getElem!_empty [Inhabited β] {a : α} {c} : (empty c : HashMap α β)[a]! = default :=
-  DHashMap.Const.get!_empty
+theorem getElem!_emptyWithCapacity [Inhabited β] {a : α} {c} : (emptyWithCapacity c : HashMap α β)[a]! = default :=
+  DHashMap.Const.get!_emptyWithCapacity
 
 @[simp]
-theorem getElem!_emptyc [Inhabited β] {a : α} : (∅ : HashMap α β)[a]! = default :=
-  DHashMap.Const.get!_emptyc
+theorem getElem!_empty [Inhabited β] {a : α} : (∅ : HashMap α β)[a]! = default :=
+  DHashMap.Const.get!_empty
+
+set_option linter.missingDocs false in
+@[deprecated getElem!_empty (since := "2025-03-12")]
+abbrev getElem!_emptyc := @getElem!_empty
 
 theorem getElem!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
     m.isEmpty = true → m[a]! = default :=
@@ -333,14 +362,18 @@ theorem getElem!_congr [EquivBEq α] [LawfulHashable α] [Inhabited β] {a b :
   DHashMap.Const.get!_congr hab
 
 @[simp]
-theorem getD_empty {a : α} {fallback : β} {c} :
-    (empty c : HashMap α β).getD a fallback = fallback :=
-  DHashMap.Const.getD_empty
+theorem getD_emptyWithCapacity {a : α} {fallback : β} {c} :
+    (emptyWithCapacity c : HashMap α β).getD a fallback = fallback :=
+  DHashMap.Const.getD_emptyWithCapacity
 
 @[simp]
-theorem getD_emptyc {a : α} {fallback : β} : (∅ : HashMap α β).getD a fallback = fallback :=
+theorem getD_empty {a : α} {fallback : β} : (∅ : HashMap α β).getD a fallback = fallback :=
   DHashMap.Const.getD_empty
 
+set_option linter.missingDocs false in
+@[deprecated getD_empty (since := "2025-03-12")]
+abbrev getD_emptyc := @getD_empty
+
 theorem getD_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} :
     m.isEmpty = true → m.getD a fallback = fallback :=
   DHashMap.Const.getD_of_isEmpty
@@ -396,12 +429,16 @@ theorem getD_congr [EquivBEq α] [LawfulHashable α] {a b : α} {fallback : β}
   DHashMap.Const.getD_congr hab
 
 @[simp]
-theorem getKey?_empty {a : α} {c} : (empty c : HashMap α β).getKey? a = none :=
-  DHashMap.getKey?_empty
+theorem getKey?_emptyWithCapacity {a : α} {c} : (emptyWithCapacity c : HashMap α β).getKey? a = none :=
+  DHashMap.getKey?_emptyWithCapacity
 
 @[simp]
-theorem getKey?_emptyc {a : α} : (∅ : HashMap α β).getKey? a = none :=
-  DHashMap.getKey?_emptyc
+theorem getKey?_empty {a : α} : (∅ : HashMap α β).getKey? a = none :=
+  DHashMap.getKey?_empty
+
+set_option linter.missingDocs false in
+@[deprecated getKey?_empty (since := "2025-03-12")]
+abbrev getKey?_emptyc := @getKey?_empty
 
 theorem getKey?_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
     m.isEmpty = true → m.getKey? a = none :=
@@ -479,12 +516,16 @@ theorem getKey_eq [LawfulBEq α] {k : α} (h : k ∈ m) : m.getKey k h = k :=
   DHashMap.getKey_eq h
 
 @[simp]
-theorem getKey!_empty [Inhabited α] {a : α} {c} : (empty c : HashMap α β).getKey! a = default :=
-  DHashMap.getKey!_empty
+theorem getKey!_emptyWithCapacity [Inhabited α] {a : α} {c} : (emptyWithCapacity c : HashMap α β).getKey! a = default :=
+  DHashMap.getKey!_emptyWithCapacity
 
 @[simp]
-theorem getKey!_emptyc [Inhabited α] {a : α} : (∅ : HashMap α β).getKey! a = default :=
-  DHashMap.getKey!_emptyc
+theorem getKey!_empty [Inhabited α] {a : α} : (∅ : HashMap α β).getKey! a = default :=
+  DHashMap.getKey!_empty
+
+set_option linter.missingDocs false in
+@[deprecated getKey!_empty (since := "2025-03-12")]
+abbrev getKey!_emptyc := @getKey!_empty
 
 theorem getKey!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
     m.isEmpty = true → m.getKey! a = default :=
@@ -544,14 +585,18 @@ theorem getKey!_eq_of_mem [LawfulBEq α] [Inhabited α] {k : α} (h : k ∈ m) :
   DHashMap.getKey!_eq_of_mem h
 
 @[simp]
-theorem getKeyD_empty {a : α} {fallback : α} {c} :
-    (empty c : HashMap α β).getKeyD a fallback = fallback :=
-  DHashMap.getKeyD_empty
+theorem getKeyD_emptyWithCapacity {a : α} {fallback : α} {c} :
+    (emptyWithCapacity c : HashMap α β).getKeyD a fallback = fallback :=
+  DHashMap.getKeyD_emptyWithCapacity
 
 @[simp]
-theorem getKeyD_emptyc {a : α} {fallback : α} : (∅ : HashMap α β).getKeyD a fallback = fallback :=
+theorem getKeyD_empty {a : α} {fallback : α} : (∅ : HashMap α β).getKeyD a fallback = fallback :=
   DHashMap.getKeyD_empty
 
+set_option linter.missingDocs false in
+@[deprecated getKeyD_empty (since := "2025-03-12")]
+abbrev getKeyD_emptyc := @getKeyD_empty
+
 theorem getKeyD_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} {fallback : α} :
     m.isEmpty = true → m.getKeyD a fallback = fallback :=
   DHashMap.getKeyD_of_isEmpty
@@ -1992,23 +2037,31 @@ section Equiv
 variable {m m₁ m₂ : HashMap α β}
 
 @[simp]
-theorem equiv_empty_iff_isEmpty [EquivBEq α] [LawfulHashable α] {c : Nat} :
-    m ~m empty c ↔ m.isEmpty :=
-  ⟨fun ⟨h⟩ => DHashMap.equiv_empty_iff_isEmpty.mp h,
-    fun h => ⟨DHashMap.equiv_empty_iff_isEmpty.mpr h⟩⟩
+theorem equiv_emptyWithCapacity_iff_isEmpty [EquivBEq α] [LawfulHashable α] {c : Nat} :
+    m ~m emptyWithCapacity c ↔ m.isEmpty :=
+  ⟨fun ⟨h⟩ => DHashMap.equiv_emptyWithCapacity_iff_isEmpty.mp h,
+    fun h => ⟨DHashMap.equiv_emptyWithCapacity_iff_isEmpty.mpr h⟩⟩
 
 @[simp]
-theorem equiv_emptyc_iff_isEmpty [EquivBEq α] [LawfulHashable α] : m ~m ∅ ↔ m.isEmpty :=
-  equiv_empty_iff_isEmpty
+theorem equiv_empty_iff_isEmpty [EquivBEq α] [LawfulHashable α] : m ~m ∅ ↔ m.isEmpty :=
+  equiv_emptyWithCapacity_iff_isEmpty
+
+set_option linter.missingDocs false in
+@[deprecated equiv_empty_iff_isEmpty (since := "2025-03-12")]
+abbrev equiv_emptyc_iff_isEmpty := @equiv_empty_iff_isEmpty
 
 @[simp]
-theorem empty_equiv_iff_isEmpty [EquivBEq α] [LawfulHashable α] {c : Nat} :
-    empty c ~m m ↔ m.isEmpty :=
-  Equiv.comm.trans equiv_empty_iff_isEmpty
+theorem emptyWithCapacity_equiv_iff_isEmpty [EquivBEq α] [LawfulHashable α] {c : Nat} :
+    emptyWithCapacity c ~m m ↔ m.isEmpty :=
+  Equiv.comm.trans equiv_emptyWithCapacity_iff_isEmpty
 
 @[simp]
-theorem emptyc_equiv_iff_isEmpty [EquivBEq α] [LawfulHashable α] : ∅ ~m m ↔ m.isEmpty :=
-  empty_equiv_iff_isEmpty
+theorem empty_equiv_iff_isEmpty [EquivBEq α] [LawfulHashable α] : ∅ ~m m ↔ m.isEmpty :=
+  emptyWithCapacity_equiv_iff_isEmpty
+
+set_option linter.missingDocs false in
+@[deprecated empty_equiv_iff_isEmpty (since := "2025-03-12")]
+abbrev emptyc_equiv_iff_isEmpty := @empty_equiv_iff_isEmpty
 
 theorem equiv_iff_toList_perm [EquivBEq α] [LawfulHashable α] :
     m₁ ~m m₂ ↔ m₁.toList.Perm m₂.toList :=

src/Std/Data/HashMap/Raw.lean

@@ -60,11 +60,14 @@ structure Raw (α : Type u) (β : Type v) where
 
 namespace Raw
 
-@[inline, inherit_doc DHashMap.Raw.empty] def empty (capacity := 8) : Raw α β :=
-  ⟨DHashMap.Raw.empty capacity⟩
+@[inline, inherit_doc DHashMap.Raw.empty] def emptyWithCapacity (capacity := 8) : Raw α β :=
+  ⟨DHashMap.Raw.emptyWithCapacity capacity⟩
+
+@[deprecated emptyWithCapacity (since := "2025-03-12"), inherit_doc emptyWithCapacity]
+abbrev empty := @emptyWithCapacity
 
 instance : EmptyCollection (Raw α β) where
-  emptyCollection := empty
+  emptyCollection := emptyWithCapacity
 
 instance : Inhabited (Raw α β) where
   default := ∅
@@ -81,7 +84,7 @@ set_option linter.unusedVariables false in
     (a : α) (b : β) : Raw α β :=
   ⟨m.inner.insert a b⟩
 
-instance [BEq α] [Hashable α] : Singleton (α × β) (Raw α β) := ⟨fun ⟨a, b⟩ => Raw.empty.insert a b⟩
+instance [BEq α] [Hashable α] : Singleton (α × β) (Raw α β) := ⟨fun ⟨a, b⟩ => (∅ : Raw α β).insert a b⟩
 
 instance [BEq α] [Hashable α] : Insert (α × β) (Raw α β) := ⟨fun ⟨a, b⟩ s => s.insert a b⟩
 
@@ -284,11 +287,15 @@ structure WF [BEq α] [Hashable α] (m : Raw α β) : Prop where
   /-- Internal implementation detail of the hash map -/
   out : m.inner.WF
 
-theorem WF.empty [BEq α] [Hashable α] {c} : (empty c : Raw α β).WF :=
-  ⟨DHashMap.Raw.WF.empty⟩
+theorem WF.emptyWithCapacity [BEq α] [Hashable α] {c} : (emptyWithCapacity c : Raw α β).WF :=
+  ⟨DHashMap.Raw.WF.emptyWithCapacity⟩
 
-theorem WF.emptyc [BEq α] [Hashable α] : (∅ : Raw α β).WF :=
-  WF.empty
+theorem WF.empty [BEq α] [Hashable α] : (∅ : Raw α β).WF :=
+  WF.emptyWithCapacity
+
+set_option linter.missingDocs false in
+@[deprecated WF.empty (since := "2025-03-12")]
+abbrev WF.emptyc := @WF.empty
 
 theorem WF.insert [BEq α] [Hashable α] {m : Raw α β} {a : α} {b : β} (h : m.WF) :
     (m.insert a b).WF :=

src/Std/Data/HashMap/RawLemmas.lean

@@ -29,12 +29,16 @@ namespace Raw
 variable {m : Raw α β}
 
 @[simp]
-theorem size_empty {c} : (empty c : Raw α β).size = 0 :=
-  DHashMap.Raw.size_empty
+theorem size_emptyWithCapacity {c} : (emptyWithCapacity c : Raw α β).size = 0 :=
+  DHashMap.Raw.size_emptyWithCapacity
 
 @[simp]
-theorem size_emptyc : (∅ : Raw α β).size = 0 :=
-  DHashMap.Raw.size_emptyc
+theorem size_empty : (∅ : Raw α β).size = 0 :=
+  DHashMap.Raw.size_empty
+
+set_option linter.missingDocs false in
+@[deprecated size_empty (since := "2025-03-12")]
+abbrev size_emptyc := @size_empty
 
 theorem isEmpty_eq_size_eq_zero : m.isEmpty = (m.size == 0) :=
   DHashMap.Raw.isEmpty_eq_size_eq_zero
@@ -45,12 +49,16 @@ private theorem ext {m m' : Raw α β} : m.inner = m'.inner → m = m' := by
 variable [BEq α] [Hashable α]
 
 @[simp]
-theorem isEmpty_empty {c} : (empty c : Raw α β).isEmpty :=
-  DHashMap.Raw.isEmpty_empty
+theorem isEmpty_emptyWithCapacity {c} : (emptyWithCapacity c : Raw α β).isEmpty :=
+  DHashMap.Raw.isEmpty_emptyWithCapacity
 
 @[simp]
-theorem isEmpty_emptyc : (∅ : Raw α β).isEmpty :=
-  DHashMap.Raw.isEmpty_emptyc
+theorem isEmpty_empty : (∅ : Raw α β).isEmpty :=
+  DHashMap.Raw.isEmpty_empty
+
+set_option linter.missingDocs false in
+@[deprecated isEmpty_empty (since := "2025-03-12")]
+abbrev isEmpty_emptyc := @isEmpty_empty
 
 @[simp]
 theorem isEmpty_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β} :
@@ -68,17 +76,25 @@ theorem mem_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} (hab :
     a ∈ m ↔ b ∈ m :=
   DHashMap.Raw.mem_congr h.out hab
 
-@[simp] theorem contains_empty {a : α} {c} : (empty c : Raw α β).contains a = false :=
+@[simp] theorem contains_emptyWithCapacity {a : α} {c} : (emptyWithCapacity c : Raw α β).contains a = false :=
+  DHashMap.Raw.contains_emptyWithCapacity
+
+@[simp] theorem not_mem_emptyWithCapacity {a : α} {c} : ¬a ∈ (emptyWithCapacity c : Raw α β) :=
+  DHashMap.Raw.not_mem_emptyWithCapacity
+
+@[simp] theorem contains_empty {a : α} : (∅ : Raw α β).contains a = false :=
   DHashMap.Raw.contains_empty
 
-@[simp] theorem not_mem_empty {a : α} {c} : ¬a ∈ (empty c : Raw α β) :=
+set_option linter.missingDocs false in
+@[deprecated contains_empty (since := "2025-03-12")]
+abbrev contains_emptyc := @contains_empty
+
+@[simp] theorem not_mem_empty {a : α} : ¬a ∈ (∅ : Raw α β) :=
   DHashMap.Raw.not_mem_empty
 
-@[simp] theorem contains_emptyc {a : α} : (∅ : Raw α β).contains a = false :=
-  DHashMap.Raw.contains_emptyc
-
-@[simp] theorem not_mem_emptyc {a : α} : ¬a ∈ (∅ : Raw α β) :=
-  DHashMap.Raw.not_mem_emptyc
+set_option linter.missingDocs false in
+@[deprecated not_mem_empty (since := "2025-03-12")]
+abbrev not_mem_emptyc := @not_mem_empty
 
 theorem contains_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
     m.isEmpty → m.contains a = false :=
@@ -151,12 +167,16 @@ theorem size_insert_le [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v
   DHashMap.Raw.size_insert_le h.out
 
 @[simp]
-theorem erase_empty {k : α} {c : Nat} : (empty c : Raw α β).erase k = empty c :=
-  ext DHashMap.Raw.erase_empty
+theorem erase_emptyWithCapacity {k : α} {c : Nat} : (emptyWithCapacity c : Raw α β).erase k = emptyWithCapacity c :=
+  ext DHashMap.Raw.erase_emptyWithCapacity
 
 @[simp]
-theorem erase_emptyc {k : α} : (∅ : Raw α β).erase k = ∅ :=
-  ext DHashMap.Raw.erase_emptyc
+theorem erase_empty {k : α} : (∅ : Raw α β).erase k = ∅ :=
+  ext DHashMap.Raw.erase_empty
+
+set_option linter.missingDocs false in
+@[deprecated erase_empty (since := "2025-03-12")]
+abbrev erase_emptyc := @erase_empty
 
 @[simp]
 theorem isEmpty_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
@@ -218,12 +238,16 @@ theorem containsThenInsertIfNew_snd (h : m.WF) {k : α} {v : β} :
 @[simp] theorem get!_eq_getElem! [Inhabited β] {a : α} : get! m a = m[a]! := rfl
 
 @[simp]
-theorem getElem?_empty {a : α} {c} : (empty c : Raw α β)[a]? = none :=
-  DHashMap.Raw.Const.get?_empty
+theorem get?_emptyWithCapacity {a : α} {c} : (emptyWithCapacity c : Raw α β)[a]? = none :=
+  DHashMap.Raw.Const.get?_emptyWithCapacity
 
 @[simp]
-theorem getElem?_emptyc {a : α} : (∅ : Raw α β)[a]? = none :=
-  DHashMap.Raw.Const.get?_emptyc
+theorem get?_empty {a : α} : (∅ : Raw α β)[a]? = none :=
+  DHashMap.Raw.Const.get?_empty
+
+set_option linter.missingDocs false in
+@[deprecated get?_empty (since := "2025-03-12")]
+abbrev get?_emptyc := @get?_empty
 
 theorem getElem?_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
     m.isEmpty = true → m[a]? = none :=
@@ -287,12 +311,16 @@ theorem getElem_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} (h
   DHashMap.Raw.Const.get_congr h.out hab (h' := h')
 
 @[simp]
-theorem getElem!_empty [Inhabited β] {a : α} {c} : (empty c : Raw α β)[a]! = default :=
-  DHashMap.Raw.Const.get!_empty
+theorem getElem!_emptyWithCapacity [Inhabited β] {a : α} {c} : (emptyWithCapacity c : Raw α β)[a]! = default :=
+  DHashMap.Raw.Const.get!_emptyWithCapacity
 
 @[simp]
-theorem getElem!_emptyc [Inhabited β] {a : α} : (∅ : Raw α β)[a]! = default :=
-  DHashMap.Raw.Const.get!_emptyc
+theorem getElem!_empty [Inhabited β] {a : α} : (∅ : Raw α β)[a]! = default :=
+  DHashMap.Raw.Const.get!_empty
+
+set_option linter.missingDocs false in
+@[deprecated getElem!_empty (since := "2025-03-12")]
+abbrev getElem!_emptyc := @getElem!_empty
 
 theorem getElem!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {a : α} :
     m.isEmpty = true → m[a]! = default :=
@@ -345,13 +373,17 @@ theorem getElem!_congr [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.W
   DHashMap.Raw.Const.get!_congr h.out hab
 
 @[simp]
-theorem getD_empty {a : α} {fallback : β} {c} : (empty c : Raw α β).getD a fallback = fallback :=
-  DHashMap.Raw.Const.getD_empty
+theorem getD_emptyWithCapacity {a : α} {fallback : β} {c} : (emptyWithCapacity c : Raw α β).getD a fallback = fallback :=
+  DHashMap.Raw.Const.getD_emptyWithCapacity
 
 @[simp]
-theorem getD_emptyc {a : α} {fallback : β} : (∅ : Raw α β).getD a fallback = fallback :=
+theorem getD_empty {a : α} {fallback : β} : (∅ : Raw α β).getD a fallback = fallback :=
   DHashMap.Raw.Const.getD_empty
 
+set_option linter.missingDocs false in
+@[deprecated getD_empty (since := "2025-03-12")]
+abbrev getD_emptyc := @getD_empty
+
 theorem getD_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {fallback : β} :
     m.isEmpty = true → m.getD a fallback = fallback :=
   DHashMap.Raw.Const.getD_of_isEmpty h.out
@@ -407,12 +439,16 @@ theorem getD_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} {fall
   DHashMap.Raw.Const.getD_congr h.out hab
 
 @[simp]
-theorem getKey?_empty {a : α} {c} : (empty c : Raw α β).getKey? a = none :=
-  DHashMap.Raw.getKey?_empty
+theorem getKey?_emptyWithCapacity {a : α} {c} : (emptyWithCapacity c : Raw α β).getKey? a = none :=
+  DHashMap.Raw.getKey?_emptyWithCapacity
 
 @[simp]
-theorem getKey?_emptyc {a : α} : (∅ : Raw α β).getKey? a = none :=
-  DHashMap.Raw.getKey?_emptyc
+theorem getKey?_empty {a : α} : (∅ : Raw α β).getKey? a = none :=
+  DHashMap.Raw.getKey?_empty
+
+set_option linter.missingDocs false in
+@[deprecated getKey?_empty (since := "2025-03-12")]
+abbrev getKey?_emptyc := @getKey?_empty
 
 theorem getKey?_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
     m.isEmpty = true → m.getKey? a = none :=
@@ -496,12 +532,16 @@ theorem getKey_eq [LawfulBEq α] (h : m.WF) {k : α} (h' : k ∈ m) :
   DHashMap.Raw.getKey_eq h.out h'
 
 @[simp]
-theorem getKey!_empty [Inhabited α] {a : α} {c} : (empty c : Raw α β).getKey! a = default :=
-  DHashMap.Raw.getKey!_empty
+theorem getKey!_emptyWithCapacity [Inhabited α] {a : α} {c} : (emptyWithCapacity c : Raw α β).getKey! a = default :=
+  DHashMap.Raw.getKey!_emptyWithCapacity
 
 @[simp]
-theorem getKey!_emptyc [Inhabited α] {a : α} : (∅ : Raw α β).getKey! a = default :=
-  DHashMap.Raw.getKey!_emptyc
+theorem getKey!_empty [Inhabited α] {a : α} : (∅ : Raw α β).getKey! a = default :=
+  DHashMap.Raw.getKey!_empty
+
+set_option linter.missingDocs false in
+@[deprecated getKey!_empty (since := "2025-03-12")]
+abbrev getKey!_emptyc := @getKey!_empty
 
 theorem getKey!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {a : α} :
     m.isEmpty = true → m.getKey! a = default :=
@@ -562,14 +602,18 @@ theorem getKey!_eq_of_mem [LawfulBEq α] [Inhabited α] (h : m.WF) {k : α} (h'
   DHashMap.Raw.getKey!_eq_of_mem h.out h'
 
 @[simp]
-theorem getKeyD_empty {a fallback : α} {c} :
-    (empty c : Raw α β).getKeyD a fallback = fallback :=
-  DHashMap.Raw.getKeyD_empty
+theorem getKeyD_emptyWithCapacity {a fallback : α} {c} :
+    (emptyWithCapacity c : Raw α β).getKeyD a fallback = fallback :=
+  DHashMap.Raw.getKeyD_emptyWithCapacity
 
 @[simp]
-theorem getKeyD_emptyc {a fallback : α} : (∅ : Raw α β).getKeyD a fallback = fallback :=
+theorem getKeyD_empty {a fallback : α} : (∅ : Raw α β).getKeyD a fallback = fallback :=
   DHashMap.Raw.getKeyD_empty
 
+set_option linter.missingDocs false in
+@[deprecated getKeyD_empty (since := "2025-03-12")]
+abbrev getKeyD_emptyc := @getKeyD_empty
+
 theorem getKeyD_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a fallback : α} :
     m.isEmpty = true → m.getKeyD a fallback = fallback :=
   DHashMap.Raw.getKeyD_of_isEmpty h.out
@@ -2025,14 +2069,18 @@ theorem of_forall_mem_unit_iff [LawfulBEq α]
 
 end Equiv
 
-theorem equiv_empty_iff_isEmpty [EquivBEq α] [LawfulHashable α] {c : Nat} (h : m.WF) :
-    m ~m empty c ↔ m.isEmpty :=
-  ⟨fun ⟨h'⟩ => (DHashMap.Raw.equiv_empty_iff_isEmpty h.1).mp h',
-    fun h' => ⟨(DHashMap.Raw.equiv_empty_iff_isEmpty h.1).mpr h'⟩⟩
+theorem equiv_emptyWithCapacity_iff_isEmpty [EquivBEq α] [LawfulHashable α] {c : Nat} (h : m.WF) :
+    m ~m emptyWithCapacity c ↔ m.isEmpty :=
+  ⟨fun ⟨h'⟩ => (DHashMap.Raw.equiv_emptyWithCapacity_iff_isEmpty h.1).mp h',
+    fun h' => ⟨(DHashMap.Raw.equiv_emptyWithCapacity_iff_isEmpty h.1).mpr h'⟩⟩
 
-theorem equiv_emptyc_iff_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) :
+theorem equiv_empty_iff_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) :
     m ~m ∅ ↔ m.isEmpty :=
-  equiv_empty_iff_isEmpty h
+  equiv_emptyWithCapacity_iff_isEmpty h
+
+set_option linter.missingDocs false in
+@[deprecated equiv_empty_iff_isEmpty (since := "2025-03-12")]
+abbrev equiv_emptyc_iff_isEmpty := @equiv_empty_iff_isEmpty
 
 theorem equiv_iff_toList_perm {m₁ m₂ : Raw α β} [EquivBEq α] [LawfulHashable α] :
     m₁ ~m m₂ ↔ m₁.toList.Perm m₂.toList :=

src/Std/Data/HashSet/Basic.lean

@@ -61,11 +61,14 @@ set so that it can hold the given number of elements without reallocating. It is
 use the empty collection notations `∅` and `{}` to create an empty hash set with the default
 capacity.
 -/
-@[inline] def empty [BEq α] [Hashable α] (capacity := 8) : HashSet α :=
-  ⟨HashMap.empty capacity⟩
+@[inline] def emptyWithCapacity [BEq α] [Hashable α] (capacity := 8) : HashSet α :=
+  ⟨HashMap.emptyWithCapacity capacity⟩
+
+@[deprecated emptyWithCapacity (since := "2025-03-12"), inherit_doc emptyWithCapacity]
+abbrev empty := @emptyWithCapacity
 
 instance [BEq α] [Hashable α] : EmptyCollection (HashSet α) where
-  emptyCollection := empty
+  emptyCollection := emptyWithCapacity
 
 instance [BEq α] [Hashable α] : Inhabited (HashSet α) where
   default := ∅
@@ -90,7 +93,7 @@ differently: it will overwrite an existing mapping.
 @[inline] def insert (m : HashSet α) (a : α) : HashSet α :=
   ⟨m.inner.insertIfNew a ()⟩
 
-instance : Singleton α (HashSet α) := ⟨fun a => HashSet.empty.insert a⟩
+instance : Singleton α (HashSet α) := ⟨fun a => (∅ : HashSet α).insert a⟩
 
 instance : Insert α (HashSet α) := ⟨fun a s => s.insert a⟩
 

src/Std/Data/HashSet/Lemmas.lean

@@ -32,12 +32,16 @@ private theorem ext {m m' : HashSet α} : m.inner = m'.inner → m = m' := by
   cases m; cases m'; rintro rfl; rfl
 
 @[simp]
-theorem isEmpty_empty {c} : (empty c : HashSet α).isEmpty :=
-  HashMap.isEmpty_empty
+theorem isEmpty_emptyWithCapacity {c} : (emptyWithCapacity c : HashSet α).isEmpty :=
+  HashMap.isEmpty_emptyWithCapacity
 
 @[simp]
-theorem isEmpty_emptyc : (∅ : HashSet α).isEmpty :=
-  HashMap.isEmpty_emptyc
+theorem isEmpty_empty : (∅ : HashSet α).isEmpty :=
+  HashMap.isEmpty_empty
+
+set_option linter.missingDocs false in
+@[deprecated isEmpty_empty (since := "2025-03-12")]
+abbrev isEmpty_emptyc := @isEmpty_empty
 
 @[simp]
 theorem isEmpty_insert [EquivBEq α] [LawfulHashable α] {a : α} : (m.insert a).isEmpty = false :=
@@ -53,17 +57,26 @@ theorem contains_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a ==
 theorem mem_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) : a ∈ m ↔ b ∈ m :=
   HashMap.mem_congr hab
 
-@[simp] theorem contains_empty {a : α} {c} : (empty c : HashSet α).contains a = false :=
+@[simp]
+theorem contains_emptyWithCapacity {a : α} {c} : (emptyWithCapacity c : HashSet α).contains a = false :=
+  HashMap.contains_emptyWithCapacity
+
+@[simp] theorem not_mem_emptyWithCapacity {a : α} {c} : ¬a ∈ (emptyWithCapacity c : HashSet α) :=
+  HashMap.not_mem_emptyWithCapacity
+
+@[simp] theorem contains_empty {a : α} : (∅ : HashSet α).contains a = false :=
   HashMap.contains_empty
 
-@[simp] theorem not_mem_empty {a : α} {c} : ¬a ∈ (empty c : HashSet α) :=
+set_option linter.missingDocs false in
+@[deprecated contains_empty (since := "2025-03-12")]
+abbrev contains_emptyc := @contains_empty
+
+@[simp] theorem not_mem_empty {a : α} : ¬a ∈ (∅ : HashSet α) :=
   HashMap.not_mem_empty
 
-@[simp] theorem contains_emptyc {a : α} : (∅ : HashSet α).contains a = false :=
-  HashMap.contains_emptyc
-
-@[simp] theorem not_mem_emptyc {a : α} : ¬a ∈ (∅ : HashSet α) :=
-  HashMap.not_mem_emptyc
+set_option linter.missingDocs false in
+@[deprecated not_mem_empty (since := "2025-03-12")]
+abbrev not_mem_emptyc := @not_mem_empty
 
 theorem contains_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
     m.isEmpty → m.contains a = false :=
@@ -128,12 +141,16 @@ theorem contains_insert_self [EquivBEq α] [LawfulHashable α] {k : α} : (m.ins
 theorem mem_insert_self [EquivBEq α] [LawfulHashable α] {k : α} : k ∈ m.insert k := by simp
 
 @[simp]
-theorem size_empty {c} : (empty c : HashSet α).size = 0 :=
-  HashMap.size_empty
+theorem size_emptyWithCapacity {c} : (emptyWithCapacity c : HashSet α).size = 0 :=
+  HashMap.size_emptyWithCapacity
 
 @[simp]
-theorem size_emptyc : (∅ : HashSet α).size = 0 :=
-  HashMap.size_emptyc
+theorem size_empty : (∅ : HashSet α).size = 0 :=
+  HashMap.size_empty
+
+set_option linter.missingDocs false in
+@[deprecated size_empty (since := "2025-03-12")]
+abbrev size_emptyc := @size_empty
 
 theorem isEmpty_eq_size_eq_zero : m.isEmpty = (m.size == 0) :=
   HashMap.isEmpty_eq_size_eq_zero
@@ -150,12 +167,16 @@ theorem size_insert_le [EquivBEq α] [LawfulHashable α] {k : α} :
   HashMap.size_insertIfNew_le
 
 @[simp]
-theorem erase_empty {a : α} {c : Nat} : (empty c : HashSet α).erase a = empty c :=
-  ext HashMap.erase_empty
+theorem erase_emptyWithCapacity {a : α} {c : Nat} : (emptyWithCapacity c : HashSet α).erase a = emptyWithCapacity c :=
+  ext HashMap.erase_emptyWithCapacity
 
 @[simp]
-theorem erase_emptyc {a : α} : (∅ : HashSet α).erase a = ∅ :=
-  ext HashMap.erase_emptyc
+theorem erase_empty {a : α} : (∅ : HashSet α).erase a = ∅ :=
+  ext HashMap.erase_empty
+
+set_option linter.missingDocs false in
+@[deprecated erase_empty (since := "2025-03-12")]
+abbrev erase_emptyc := @erase_empty
 
 @[simp]
 theorem isEmpty_erase [EquivBEq α] [LawfulHashable α] {k : α} :
@@ -191,12 +212,16 @@ theorem size_le_size_erase [EquivBEq α] [LawfulHashable α] {k : α} :
   HashMap.size_le_size_erase
 
 @[simp]
-theorem get?_empty {a : α} {c} : (empty c : HashSet α).get? a = none :=
-  HashMap.getKey?_empty
+theorem get?_emptyWithCapacity {a : α} {c} : (emptyWithCapacity c : HashSet α).get? a = none :=
+  HashMap.getKey?_emptyWithCapacity
 
 @[simp]
-theorem get?_emptyc {a : α} : (∅ : HashSet α).get? a = none :=
-  HashMap.getKey?_emptyc
+theorem get?_empty {a : α} : (∅ : HashSet α).get? a = none :=
+  HashMap.getKey?_empty
+
+set_option linter.missingDocs false in
+@[deprecated get?_empty (since := "2025-03-12")]
+abbrev get?_emptyc := @get?_empty
 
 theorem get?_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
     m.isEmpty = true → m.get? a = none :=
@@ -263,12 +288,16 @@ theorem get_eq [LawfulBEq α] {k : α} (h : k ∈ m) : m.get k h = k :=
   HashMap.getKey_eq h
 
 @[simp]
-theorem get!_empty [Inhabited α] {a : α} {c} : (empty c : HashSet α).get! a = default :=
-  HashMap.getKey!_empty
+theorem get!_emptyWithCapacity [Inhabited α] {a : α} {c} : (emptyWithCapacity c : HashSet α).get! a = default :=
+  HashMap.getKey!_emptyWithCapacity
 
 @[simp]
-theorem get!_emptyc [Inhabited α] {a : α} : (∅ : HashSet α).get! a = default :=
-  HashMap.getKey!_emptyc
+theorem get!_empty [Inhabited α] {a : α} : (∅ : HashSet α).get! a = default :=
+  HashMap.getKey!_empty
+
+set_option linter.missingDocs false in
+@[deprecated get!_empty (since := "2025-03-12")]
+abbrev get!_emptyc := @get!_empty
 
 theorem get!_of_isEmpty [Inhabited α] [EquivBEq α] [LawfulHashable α] {a : α} :
     m.isEmpty = true → m.get! a = default :=
@@ -322,12 +351,16 @@ theorem get!_eq_of_mem [LawfulBEq α] [Inhabited α] {k : α} (h : k ∈ m) : m.
   HashMap.getKey!_eq_of_mem h
 
 @[simp]
-theorem getD_empty {a fallback : α} {c} : (empty c : HashSet α).getD a fallback = fallback :=
-  HashMap.getKeyD_empty
+theorem getD_emptyWithCapacity {a fallback : α} {c} : (emptyWithCapacity c : HashSet α).getD a fallback = fallback :=
+  HashMap.getKeyD_emptyWithCapacity
 
 @[simp]
-theorem getD_emptyc {a fallback : α} : (∅ : HashSet α).getD a fallback = fallback :=
-  HashMap.getKeyD_emptyc
+theorem getD_empty {a fallback : α} : (∅ : HashSet α).getD a fallback = fallback :=
+  HashMap.getKeyD_empty
+
+set_option linter.missingDocs false in
+@[deprecated getD_empty (since := "2025-03-12")]
+abbrev getD_emptyc := @getD_empty
 
 theorem getD_of_isEmpty [EquivBEq α] [LawfulHashable α] {a fallback : α} :
     m.isEmpty = true → m.getD a fallback = fallback :=
@@ -750,23 +783,31 @@ section Equiv
 variable {m m₁ m₂ : HashSet α}
 
 @[simp]
-theorem equiv_empty_iff_isEmpty [EquivBEq α] [LawfulHashable α] {c : Nat} :
-    m ~m empty c ↔ m.isEmpty :=
-  ⟨fun ⟨h⟩ => HashMap.equiv_empty_iff_isEmpty.mp h,
-    fun h => ⟨HashMap.equiv_empty_iff_isEmpty.mpr h⟩⟩
+theorem equiv_emptyWithCapacity_iff_isEmpty [EquivBEq α] [LawfulHashable α] {c : Nat} :
+    m ~m emptyWithCapacity c ↔ m.isEmpty :=
+  ⟨fun ⟨h⟩ => HashMap.equiv_emptyWithCapacity_iff_isEmpty.mp h,
+    fun h => ⟨HashMap.equiv_emptyWithCapacity_iff_isEmpty.mpr h⟩⟩
 
 @[simp]
-theorem equiv_emptyc_iff_isEmpty [EquivBEq α] [LawfulHashable α] : m ~m ∅ ↔ m.isEmpty :=
-  equiv_empty_iff_isEmpty
+theorem equiv_empty_iff_isEmpty [EquivBEq α] [LawfulHashable α] : m ~m ∅ ↔ m.isEmpty :=
+  equiv_emptyWithCapacity_iff_isEmpty
+
+set_option linter.missingDocs false in
+@[deprecated equiv_empty_iff_isEmpty (since := "2025-03-12")]
+abbrev equiv_emptyc_iff_isEmpty := @equiv_empty_iff_isEmpty
 
 @[simp]
-theorem empty_equiv_iff_isEmpty [EquivBEq α] [LawfulHashable α] {c : Nat} :
-    empty c ~m m ↔ m.isEmpty :=
-  Equiv.comm.trans equiv_empty_iff_isEmpty
+theorem emptyWithCapacity_equiv_iff_isEmpty [EquivBEq α] [LawfulHashable α] {c : Nat} :
+    emptyWithCapacity c ~m m ↔ m.isEmpty :=
+  Equiv.comm.trans equiv_emptyWithCapacity_iff_isEmpty
 
 @[simp]
-theorem emptyc_equiv_iff_isEmpty [EquivBEq α] [LawfulHashable α] : ∅ ~m m ↔ m.isEmpty :=
-  empty_equiv_iff_isEmpty
+theorem empty_equiv_iff_isEmpty [EquivBEq α] [LawfulHashable α] : ∅ ~m m ↔ m.isEmpty :=
+  emptyWithCapacity_equiv_iff_isEmpty
+
+set_option linter.missingDocs false in
+@[deprecated empty_equiv_iff_isEmpty (since := "2025-03-12")]
+abbrev emptyc_equiv_iff_isEmpty := @empty_equiv_iff_isEmpty
 
 theorem equiv_iff_toList_perm [EquivBEq α] [LawfulHashable α] :
     m₁ ~m m₂ ↔ m₁.toList.Perm m₂.toList :=

src/Std/Data/HashSet/Raw.lean

@@ -62,11 +62,14 @@ Creates a new empty hash set. The optional parameter `capacity` can be supplied
 so that it can hold the given number of elements without reallocating. It is also possible to use
 the empty collection notations `∅` and `{}` to create an empty hash set with the default capacity.
 -/
-@[inline] def empty (capacity := 8) : Raw α :=
-  ⟨HashMap.Raw.empty capacity⟩
+@[inline] def emptyWithCapacity (capacity := 8) : Raw α :=
+  ⟨HashMap.Raw.emptyWithCapacity capacity⟩
+
+@[deprecated emptyWithCapacity (since := "2025-03-12"), inherit_doc emptyWithCapacity]
+abbrev empty := @emptyWithCapacity
 
 instance : EmptyCollection (Raw α) where
-  emptyCollection := empty
+  emptyCollection := emptyWithCapacity
 
 instance : Inhabited (Raw α) where
   default := ∅
@@ -91,7 +94,7 @@ differently: it will overwrite an existing mapping.
 @[inline] def insert [BEq α] [Hashable α] (m : Raw α) (a : α) : Raw α :=
   ⟨m.inner.insertIfNew a ()⟩
 
-instance [BEq α] [Hashable α] : Singleton α (Raw α) := ⟨fun a => Raw.empty.insert a⟩
+instance [BEq α] [Hashable α] : Singleton α (Raw α) := ⟨fun a => (∅ : Raw α).insert a⟩
 
 instance [BEq α] [Hashable α] : Insert α (Raw α) := ⟨fun a s => s.insert a⟩
 
@@ -283,11 +286,15 @@ structure WF [BEq α] [Hashable α] (m : Raw α) : Prop where
   /-- Internal implementation detail of the hash set -/
   out : m.inner.WF
 
-theorem WF.empty [BEq α] [Hashable α] {c} : (empty c : Raw α).WF :=
-  ⟨HashMap.Raw.WF.empty⟩
+theorem WF.emptyWithCapacity [BEq α] [Hashable α] {c} : (emptyWithCapacity c : Raw α).WF :=
+  ⟨HashMap.Raw.WF.emptyWithCapacity⟩
 
-theorem WF.emptyc [BEq α] [Hashable α] : (∅ : Raw α).WF :=
-  ⟨HashMap.Raw.WF.empty⟩
+theorem WF.empty [BEq α] [Hashable α] : (∅ : Raw α).WF :=
+  WF.emptyWithCapacity
+
+set_option linter.missingDocs false in
+@[deprecated WF.empty (since := "2025-03-12")]
+abbrev WF.emptyc := @WF.empty
 
 theorem WF.insert [BEq α] [Hashable α] {m : Raw α} {a : α} (h : m.WF) : (m.insert a).WF :=
   ⟨HashMap.Raw.WF.insertIfNew h.out⟩

src/Std/Data/HashSet/RawLemmas.lean

@@ -32,12 +32,16 @@ private theorem ext {m m' : Raw α} : m.inner = m'.inner → m = m' := by
   cases m; cases m'; rintro rfl; rfl
 
 @[simp]
-theorem size_empty {c} : (empty c : Raw α).size = 0 :=
-  HashMap.Raw.size_empty
+theorem size_emptyWithCapacity {c} : (emptyWithCapacity c : Raw α).size = 0 :=
+  HashMap.Raw.size_emptyWithCapacity
 
 @[simp]
-theorem size_emptyc : (∅ : Raw α).size = 0 :=
-  HashMap.Raw.size_emptyc
+theorem size_empty : (∅ : Raw α).size = 0 :=
+  HashMap.Raw.size_empty
+
+set_option linter.missingDocs false in
+@[deprecated size_empty (since := "2025-03-12")]
+abbrev size_emptyc := @size_empty
 
 theorem isEmpty_eq_size_eq_zero : m.isEmpty = (m.size == 0) :=
   HashMap.Raw.isEmpty_eq_size_eq_zero
@@ -45,12 +49,16 @@ theorem isEmpty_eq_size_eq_zero : m.isEmpty = (m.size == 0) :=
 variable [BEq α] [Hashable α]
 
 @[simp]
-theorem isEmpty_empty {c} : (empty c : Raw α).isEmpty :=
-  HashMap.Raw.isEmpty_empty
+theorem isEmpty_emptyWithCapacity {c} : (emptyWithCapacity c : Raw α).isEmpty :=
+  HashMap.Raw.isEmpty_emptyWithCapacity
 
 @[simp]
-theorem isEmpty_emptyc : (∅ : Raw α).isEmpty :=
-  HashMap.Raw.isEmpty_emptyc
+theorem isEmpty_empty : (∅ : Raw α).isEmpty :=
+  HashMap.Raw.isEmpty_empty
+
+set_option linter.missingDocs false in
+@[deprecated isEmpty_empty (since := "2025-03-12")]
+abbrev isEmpty_emptyc := @isEmpty_empty
 
 @[simp]
 theorem isEmpty_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
@@ -68,17 +76,25 @@ theorem mem_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} (hab :
     a ∈ m ↔ b ∈ m :=
   HashMap.Raw.mem_congr h.out hab
 
-@[simp] theorem contains_empty {a : α} {c} : (empty c : Raw α).contains a = false :=
+@[simp] theorem contains_emptyWithCapacity {a : α} {c} : (emptyWithCapacity c : Raw α).contains a = false :=
+  HashMap.Raw.contains_emptyWithCapacity
+
+@[simp] theorem not_mem_emptyWithCapacity {a : α} {c} : ¬a ∈ (emptyWithCapacity c : Raw α) :=
+  HashMap.Raw.not_mem_emptyWithCapacity
+
+@[simp] theorem contains_empty {a : α} : (∅ : Raw α).contains a = false :=
   HashMap.Raw.contains_empty
 
-@[simp] theorem not_mem_empty {a : α} {c} : ¬a ∈ (empty c : Raw α) :=
+set_option linter.missingDocs false in
+@[deprecated contains_empty (since := "2025-03-12")]
+abbrev contains_emptyc := @contains_empty
+
+@[simp] theorem not_mem_empty {a : α} : ¬a ∈ (∅ : Raw α) :=
   HashMap.Raw.not_mem_empty
 
-@[simp] theorem contains_emptyc {a : α} : (∅ : Raw α).contains a = false :=
-  HashMap.Raw.contains_emptyc
-
-@[simp] theorem not_mem_emptyc {a : α} : ¬a ∈ (∅ : Raw α) :=
-  HashMap.Raw.not_mem_emptyc
+set_option linter.missingDocs false in
+@[deprecated not_mem_empty (since := "2025-03-12")]
+abbrev not_mem_emptyc := @not_mem_empty
 
 theorem contains_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
     m.isEmpty → m.contains a = false :=
@@ -160,12 +176,16 @@ theorem size_insert_le [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
   HashMap.Raw.size_insertIfNew_le h.out
 
 @[simp]
-theorem erase_empty {k : α} {c : Nat} : (empty c : Raw α).erase k = empty c :=
-  ext HashMap.Raw.erase_empty
+theorem erase_emptyWithCapacity {k : α} {c : Nat} : (emptyWithCapacity c : Raw α).erase k = emptyWithCapacity c :=
+  ext HashMap.Raw.erase_emptyWithCapacity
 
 @[simp]
-theorem erase_emptyc {k : α} : (∅ : Raw α).erase k = ∅ :=
-  ext HashMap.Raw.erase_emptyc
+theorem erase_empty {k : α} : (∅ : Raw α).erase k = ∅ :=
+  ext HashMap.Raw.erase_empty
+
+set_option linter.missingDocs false in
+@[deprecated erase_empty (since := "2025-03-12")]
+abbrev erase_emptyc := @erase_empty
 
 @[simp]
 theorem isEmpty_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
@@ -203,12 +223,16 @@ theorem size_le_size_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α}
   HashMap.Raw.size_le_size_erase h.out
 
 @[simp]
-theorem get?_empty {a : α} {c} : (empty c : Raw α).get? a = none :=
-  HashMap.Raw.getKey?_empty
+theorem get?_emptyWithCapacity {a : α} {c} : (emptyWithCapacity c : Raw α).get? a = none :=
+  HashMap.Raw.getKey?_emptyWithCapacity
 
 @[simp]
-theorem get?_emptyc {a : α} : (∅ : Raw α).get? a = none :=
-  HashMap.Raw.getKey?_emptyc
+theorem get?_empty {a : α} : (∅ : Raw α).get? a = none :=
+  HashMap.Raw.getKey?_empty
+
+set_option linter.missingDocs false in
+@[deprecated get?_empty (since := "2025-03-12")]
+abbrev get?_emptyc := @get?_empty
 
 theorem get?_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
     m.isEmpty = true → m.get? a = none :=
@@ -283,12 +307,16 @@ theorem get_eq [LawfulBEq α] (h : m.WF) {k : α} (h' : m.contains k) :
   HashMap.Raw.getKey_eq h.out h'
 
 @[simp]
-theorem get!_empty [Inhabited α] {a : α} {c} : (empty c : Raw α).get! a = default :=
-  HashMap.Raw.getKey!_empty
+theorem get!_emptyWithCapacity [Inhabited α] {a : α} {c} : (emptyWithCapacity c : Raw α).get! a = default :=
+  HashMap.Raw.getKey!_emptyWithCapacity
 
 @[simp]
-theorem get!_emptyc [Inhabited α] {a : α} : (∅ : Raw α).get! a = default :=
-  HashMap.Raw.getKey!_emptyc
+theorem get!_empty [Inhabited α] {a : α} : (∅ : Raw α).get! a = default :=
+  HashMap.Raw.getKey!_empty
+
+set_option linter.missingDocs false in
+@[deprecated get!_empty (since := "2025-03-12")]
+abbrev get!_emptyc := @get!_empty
 
 theorem get!_of_isEmpty [Inhabited α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
     m.isEmpty = true → m.get! a = default :=
@@ -344,12 +372,16 @@ theorem get!_eq_of_mem [LawfulBEq α] [Inhabited α] (h : m.WF) {k : α} (h' : k
   HashMap.Raw.getKey!_eq_of_mem h.out h'
 
 @[simp]
-theorem getD_empty {a fallback : α} {c} : (empty c : Raw α).getD a fallback = fallback :=
-  HashMap.Raw.getKeyD_empty
+theorem getD_emptyWithCapacity {a fallback : α} {c} : (emptyWithCapacity c : Raw α).getD a fallback = fallback :=
+  HashMap.Raw.getKeyD_emptyWithCapacity
 
 @[simp]
-theorem getD_emptyc {a fallback : α} : (∅ : Raw α).getD a fallback = fallback :=
-  HashMap.Raw.getKeyD_emptyc
+theorem getD_empty {a fallback : α} : (∅ : Raw α).getD a fallback = fallback :=
+  HashMap.Raw.getKeyD_empty
+
+set_option linter.missingDocs false in
+@[deprecated getD_empty (since := "2025-03-12")]
+abbrev getD_emptyc := @getD_empty
 
 theorem getD_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a fallback : α} :
     m.isEmpty = true → m.getD a fallback = fallback :=
@@ -783,14 +815,18 @@ theorem of_forall_mem_iff [LawfulBEq α] (h₁ : m₁.WF) (h₂ : m₂.WF)
 
 end Equiv
 
-theorem equiv_empty_iff_isEmpty [EquivBEq α] [LawfulHashable α] {c : Nat} (h : m.WF) :
-    m ~m empty c ↔ m.isEmpty :=
-  ⟨fun ⟨h'⟩ => (HashMap.Raw.equiv_empty_iff_isEmpty h.1).mp h',
-    fun h' => ⟨(HashMap.Raw.equiv_empty_iff_isEmpty h.1).mpr h'⟩⟩
+theorem equiv_emptyWithCapacity_iff_isEmpty [EquivBEq α] [LawfulHashable α] {c : Nat} (h : m.WF) :
+    m ~m emptyWithCapacity c ↔ m.isEmpty :=
+  ⟨fun ⟨h'⟩ => (HashMap.Raw.equiv_emptyWithCapacity_iff_isEmpty h.1).mp h',
+    fun h' => ⟨(HashMap.Raw.equiv_emptyWithCapacity_iff_isEmpty h.1).mpr h'⟩⟩
 
-theorem equiv_emptyc_iff_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) :
+theorem equiv_empty_iff_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) :
     m ~m ∅ ↔ m.isEmpty :=
-  equiv_empty_iff_isEmpty h
+  equiv_emptyWithCapacity_iff_isEmpty h
+
+set_option linter.missingDocs false in
+@[deprecated equiv_empty_iff_isEmpty (since := "2025-03-12")]
+abbrev equiv_emptyc_iff_isEmpty := @equiv_empty_iff_isEmpty
 
 theorem equiv_iff_toList_perm {m₁ m₂ : Raw α} [EquivBEq α] [LawfulHashable α] :
     m₁ ~m m₂ ↔ m₁.toList.Perm m₂.toList :=

src/Std/Sat/AIG/Basic.lean

@@ -293,7 +293,7 @@ Transform an `Entrypoint` into a graphviz string. Useful for debugging purposes.
 def toGraphviz {α : Type} [DecidableEq α] [ToString α] [Hashable α] (entry : Entrypoint α) :
     String :=
   let ⟨⟨decls, _, hinv⟩, ⟨idx, h⟩⟩ := entry
-  let (dag, s) := go "" decls hinv idx h |>.run .empty
+  let (dag, s) := go "" decls hinv idx h |>.run ∅
   let nodes := s.fold (fun x y ↦ x ++ toGraphvizString decls y) ""
   "Digraph AIG {" ++ nodes ++ dag ++ "}"
 where

src/lake/Lake/Config/Module.lean

@@ -30,7 +30,7 @@ instance : Hashable Module where hash m := hash m.keyName
 instance : BEq Module where beq m n := m.keyName == n.keyName
 
 abbrev ModuleSet := Std.HashSet Module
-@[inline] def ModuleSet.empty : ModuleSet := Std.HashSet.empty
+@[inline] def ModuleSet.empty : ModuleSet := ∅
 
 abbrev OrdModuleSet := OrdHashSet Module
 @[inline] def OrdModuleSet.empty : OrdModuleSet := OrdHashSet.empty

src/lake/Lake/Config/Package.lean

@@ -422,7 +422,7 @@ instance : Hashable Package where hash pkg := hash pkg.config.name
 instance : BEq Package where beq p1 p2 := p1.config.name == p2.config.name
 
 abbrev PackageSet := Std.HashSet Package
-@[inline] def PackageSet.empty : PackageSet := Std.HashSet.empty
+@[inline] def PackageSet.empty : PackageSet := ∅
 
 abbrev OrdPackageSet := OrdHashSet Package
 @[inline] def OrdPackageSet.empty : OrdPackageSet := OrdHashSet.empty

src/lake/Lake/Util/OrdHashSet.lean

@@ -22,12 +22,12 @@ variable [Hashable α] [BEq α]
 instance : Coe (OrdHashSet α) (Std.HashSet α) := ⟨toHashSet⟩
 
 def empty : OrdHashSet α :=
-  ⟨.empty, .empty⟩
+  ⟨∅, .empty⟩
 
 instance : EmptyCollection (OrdHashSet α) := ⟨empty⟩
 
 def mkEmpty (size : Nat) : OrdHashSet α :=
-  ⟨.empty, .mkEmpty size⟩
+  ⟨∅, .mkEmpty size⟩
 
 def insert (self : OrdHashSet α) (a : α) : OrdHashSet α :=
   if self.toHashSet.contains a then

src/stdlib_flags.h

@@ -11,12 +11,12 @@ options get_default_options() {
     opts = opts.update({"debug", "proofAsSorry"}, false);
     // switch to `true` for ABI-breaking changes affecting meta code;
     // see also next option!
-    opts = opts.update({"interpreter", "prefer_native"}, false);
+    opts = opts.update({"interpreter", "prefer_native"}, true);
     // switch to `false` when enabling `prefer_native` should also affect use
     // of built-in parsers in quotations; this is usually the case, but setting
     // both to `true` may be necessary for handling non-builtin parsers with
     // builtin elaborators
-    opts = opts.update({"internal", "parseQuotWithCurrentStage"}, true);
+    opts = opts.update({"internal", "parseQuotWithCurrentStage"}, false);
     // changes to builtin parsers may also require toggling the following option if macros/syntax
     // with custom precheck hooks were affected
     opts = opts.update({"quotPrecheck"}, true);

tests/lean/run/hashmap-implicits.lean

@@ -15,14 +15,14 @@ structure A (α) extends BEq α, Hashable α where
 def A.add (xs : A α) (x : α) : A α :=
   {xs with foo := xs.foo.insert x 5}
 
-example (xs : A α) (x : α) : ¬x ∈ @DHashMap.empty _ (fun _ => Nat) xs.toBEq xs.toHashable 5 :=
-  DHashMap.not_mem_empty
+example (xs : A α) (x : α) : ¬x ∈ @DHashMap.emptyWithCapacity _ (fun _ => Nat) xs.toBEq xs.toHashable 5 :=
+  DHashMap.not_mem_emptyWithCapacity
 
-example (xs : A α) (x : α) : (@DHashMap.empty _ (fun _ => Nat) xs.toBEq xs.toHashable 5).contains x = false := by
-  rw [DHashMap.contains_empty]
+example (xs : A α) (x : α) : (@DHashMap.emptyWithCapacity _ (fun _ => Nat) xs.toBEq xs.toHashable 5).contains x = false := by
+  rw [DHashMap.contains_emptyWithCapacity]
 
-example (xs : A α) (x : α) : DHashMap.Const.get? (@DHashMap.empty _ (fun _ => Nat) xs.toBEq xs.toHashable 5) x = none := by
-  rw [DHashMap.Const.get?_empty]
+example (xs : A α) (x : α) : DHashMap.Const.get? (@DHashMap.emptyWithCapacity _ (fun _ => Nat) xs.toBEq xs.toHashable 5) x = none := by
+  rw [DHashMap.Const.get?_emptyWithCapacity]
 
 example (xs : A α) (x : α) [@LawfulBEq α xs.toBEq] : xs.foo.size ≤ (xs.foo.insert x 5).size :=
   DHashMap.size_le_size_insert
@@ -37,14 +37,14 @@ structure A (α) extends BEq α, Hashable α where
 def A.add (xs : A α) (x : α) : A α :=
   {xs with foo := xs.foo.insert x 5}
 
-example (xs : A α) (x : α) : ¬x ∈ @HashMap.empty _ Nat xs.toBEq xs.toHashable 5 :=
-  HashMap.not_mem_empty
+example (xs : A α) (x : α) : ¬x ∈ @HashMap.emptyWithCapacity _ Nat xs.toBEq xs.toHashable 5 :=
+  HashMap.not_mem_emptyWithCapacity
 
-example (xs : A α) (x : α) : (@HashMap.empty _ Nat xs.toBEq xs.toHashable 5).contains x = false := by
-  rw [HashMap.contains_empty]
+example (xs : A α) (x : α) : (@HashMap.emptyWithCapacity _ Nat xs.toBEq xs.toHashable 5).contains x = false := by
+  rw [HashMap.contains_emptyWithCapacity]
 
-example (xs : A α) (x : α) : (@HashMap.empty _ Nat xs.toBEq xs.toHashable 5)[x]? = none := by
-  rw [HashMap.getElem?_empty]
+example (xs : A α) (x : α) : (@HashMap.emptyWithCapacity _ Nat xs.toBEq xs.toHashable 5)[x]? = none := by
+  rw [HashMap.getElem?_emptyWithCapacity]
 
 example (xs : A α) (x : α) [@LawfulBEq α xs.toBEq] : xs.foo.size ≤ (xs.foo.insert x 5).size :=
   HashMap.size_le_size_insert
@@ -59,11 +59,11 @@ structure A (α) extends BEq α, Hashable α where
 def A.add (xs : A α) (x : α) : A α :=
   {xs with foo := xs.foo.insert x}
 
-example (xs : A α) (x : α) : ¬x ∈ @HashSet.empty _ xs.toBEq xs.toHashable 5 :=
-  DHashMap.not_mem_empty
+example (xs : A α) (x : α) : ¬x ∈ @HashSet.emptyWithCapacity _ xs.toBEq xs.toHashable 5 :=
+  HashSet.not_mem_emptyWithCapacity
 
-example (xs : A α) (x : α) : (@HashSet.empty _ xs.toBEq xs.toHashable 5).contains x = false := by
-  rw [HashSet.contains_empty]
+example (xs : A α) (x : α) : (@HashSet.emptyWithCapacity _ xs.toBEq xs.toHashable 5).contains x = false := by
+  rw [HashSet.contains_emptyWithCapacity]
 
 example (xs : A α) (x : α) [@LawfulBEq α xs.toBEq] : xs.foo.size ≤ (xs.foo.insert x).size :=
   HashSet.size_le_size_insert