feat: add isExclusiveUnsafe

Avoid potentially expensive `e.replace` if it is not applicable.

src/Init/Core.lean

@@ -1089,15 +1089,18 @@ def InvImage {α : Sort u} {β : Sort v} (r : β → β → Prop) (f : α → β
   fun a₁ a₂ => r (f a₁) (f a₂)
 
 /--
-The transitive closure `r⁺` of a relation `r` is the smallest relation which is
-transitive and contains `r`. `r⁺ a z` if and only if there exists a sequence
+The transitive closure `TransGen r` of a relation `r` is the smallest relation which is
+transitive and contains `r`. `TransGen r a z` if and only if there exists a sequence
 `a r b r ... r z` of length at least 1 connecting `a` to `z`.
 -/
-inductive TC {α : Sort u} (r : α → α → Prop) : α → α → Prop where
-  /-- If `r a b` then `r⁺ a b`. This is the base case of the transitive closure. -/
-  | base  : ∀ a b, r a b → TC r a b
+inductive Relation.TransGen {α : Sort u} (r : α → α → Prop) : α → α → Prop
+  /-- If `r a b` then `TransGen r a b`. This is the base case of the transitive closure. -/
+  | single {a b} : r a b → TransGen r a b
   /-- The transitive closure is transitive. -/
-  | trans : ∀ a b c, TC r a b → TC r b c → TC r a c
+  | tail {a b c} : TransGen r a b → r b c → TransGen r a c
+
+/-- Deprecated synonym for `Relation.TransGen`. -/
+@[deprecated Relation.TransGen (since := "2024-07-16")] abbrev TC := @Relation.TransGen
 
 /-! # Subtype -/
 

src/Init/Notation.lean

@@ -267,8 +267,7 @@ syntax (name := rawNatLit) "nat_lit " num : term
 
 @[inherit_doc] infixr:90 " ∘ "  => Function.comp
 @[inherit_doc] infixr:35 " × "  => Prod
-@[inherit_doc] infixr:35 " ×ₚ "  => PProd
-@[inherit_doc] infixr:35 " ×ₘ "  => MProd
+@[inherit_doc] infixr:35 " ×' " => PProd
 
 @[inherit_doc] infix:50  " ∣ " => Dvd.dvd
 @[inherit_doc] infixl:55 " ||| " => HOr.hOr

src/Init/NotationExtra.lean

@@ -163,16 +163,6 @@ end Lean
   | `($(_) $x $y)          => `(($x, $y))
   | _                      => throw ()
 
-@[app_unexpander PProd.mk] def unexpandPProdMk : Lean.PrettyPrinter.Unexpander
-  | `($(_) $x ($y, $ys,*)ₚ) => `(($x, $y, $ys,*)ₚ)
-  | `($(_) $x $y)           => `(($x, $y)ₚ)
-  | _                       => throw ()
-
-@[app_unexpander MProd.mk] def unexpandMProdMk : Lean.PrettyPrinter.Unexpander
-  | `($(_) $x ($y, $ys,*)ₘ) => `(($x, $y, $ys,*)ₘ)
-  | `($(_) $x $y)           => `(($x, $y)ₘ)
-  | _                       => throw ()
-
 @[app_unexpander ite] def unexpandIte : Lean.PrettyPrinter.Unexpander
   | `($(_) $c $t $e) => `(if $c then $t else $e)
   | _                => throw ()

src/Init/Prelude.lean

@@ -488,9 +488,9 @@ attribute [unbox] Prod
 
 /--
 Similar to `Prod`, but `α` and `β` can be propositions.
+You can use `α ×' β` as notation for `PProd α β`.
 We use this type internally to automatically generate the `brecOn` recursor.
 -/
-@[pp_using_anonymous_constructor]
 structure PProd (α : Sort u) (β : Sort v) where
   /-- The first projection out of a pair. if `p : PProd α β` then `p.1 : α`. -/
   fst : α

src/Init/ShareCommon.lean

@@ -102,3 +102,11 @@ instance ShareCommonT.monadShareCommon [Monad m] : MonadShareCommon (ShareCommon
 
 @[inline] def ShareCommonT.run [Monad m] (x : ShareCommonT σ m α) : m α := x.run' default
 @[inline] def ShareCommonM.run (x : ShareCommonM σ α) : α := ShareCommonT.run x
+
+/--
+A more restrictive but efficient max sharing primitive.
+
+Remark: it optimizes the number of RC operations, and the strategy for caching results.
+-/
+@[extern "lean_sharecommon_quick"]
+def ShareCommon.shareCommon' (a : α) : α := a

src/Init/Util.lean

@@ -45,6 +45,13 @@ def dbgSleep {α : Type u} (ms : UInt32) (f : Unit → α) : α := f ()
 @[extern "lean_ptr_addr"]
 unsafe opaque ptrAddrUnsafe {α : Type u} (a : @& α) : USize
 
+/--
+Returns `true` if `a` is an exclusive object.
+We say an object is exclusive if it is single-threaded and its reference counter is 1.
+-/
+@[extern "lean_is_exclusive_obj"]
+unsafe opaque isExclusiveUnsafe {α : Type u} (a : @& α) : Bool
+
 set_option linter.unusedVariables.funArgs false in
 @[inline] unsafe def withPtrAddrUnsafe {α : Type u} {β : Type v} (a : α) (k : USize → β) (h : ∀ u₁ u₂, k u₁ = k u₂) : β :=
   k (ptrAddrUnsafe a)

src/Init/WF.lean

@@ -148,22 +148,26 @@ end InvImage
   wf  := InvImage.wf f h.wf
 
 -- The transitive closure of a well-founded relation is well-founded
-namespace TC
-variable {α : Sort u} {r : α → α → Prop}
+open Relation
 
-theorem accessible {z : α} (ac : Acc r z) : Acc (TC r) z := by
-  induction ac with
-  | intro x acx ih =>
-    apply Acc.intro x
-    intro y rel
-    induction rel with
-    | base a b rab => exact ih a rab
-    | trans a b c rab _ _ ih₂ => apply Acc.inv (ih₂ acx ih) rab
+theorem Acc.transGen (h : Acc r a) : Acc (TransGen r) a := by
+  induction h with
+  | intro x _ H =>
+    refine Acc.intro x fun y hy ↦ ?_
+    cases hy with
+    | single hyx =>
+      exact H y hyx
+    | tail hyz hzx =>
+      exact (H _ hzx).inv hyz
 
-theorem wf (h : WellFounded r) : WellFounded (TC r) :=
-  ⟨fun a => accessible (apply h a)⟩
-end TC
+theorem acc_transGen_iff : Acc (TransGen r) a ↔ Acc r a :=
+  ⟨Subrelation.accessible TransGen.single, Acc.transGen⟩
 
+theorem WellFounded.transGen (h : WellFounded r) : WellFounded (TransGen r) :=
+  ⟨fun a ↦ (h.apply a).transGen⟩
+
+@[deprecated Acc.transGen (since := "2024-07-16")] abbrev TC.accessible := @Acc.transGen
+@[deprecated WellFounded.transGen (since := "2024-07-16")] abbrev TC.wf := @WellFounded.transGen
 namespace Nat
 
 -- less-than is well-founded

src/Lean/Compiler/LCNF/Main.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Compiler.Options
+import Lean.Compiler.ExternAttr
 import Lean.Compiler.LCNF.PassManager
 import Lean.Compiler.LCNF.Passes
 import Lean.Compiler.LCNF.PrettyPrinter

src/Lean/Compiler/LCNF/PrettyPrinter.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Lean.PrettyPrinter
+import Lean.PrettyPrinter.Delaborator.Options
 import Lean.Compiler.LCNF.CompilerM
 import Lean.Compiler.LCNF.Internalize
 

src/Lean/Data/RBMap.lean

@@ -80,6 +80,10 @@ protected def max : RBNode α β → Option (Sigma (fun k => β k))
 def singleton (k : α) (v : β k) : RBNode α β :=
   node red leaf k v leaf
 
+def isSingleton : RBNode α β → Bool
+  | node _ leaf _ _ leaf => true
+  | _ => false
+
 -- the first half of Okasaki's `balance`, concerning red-red sequences in the left child
 @[inline] def balance1 : RBNode α β → (a : α) → β a → RBNode α β → RBNode α β
   | node red (node red a kx vx b) ky vy c, kz, vz, d
@@ -269,6 +273,9 @@ variable {α : Type u} {β : Type v} {σ : Type w} {cmp : α → α → Ordering
 def depth (f : Nat → Nat → Nat) (t : RBMap α β cmp) : Nat :=
   t.val.depth f
 
+def isSingleton (t : RBMap α β cmp) : Bool :=
+  t.val.isSingleton
+
 @[inline] def fold (f : σ → α → β → σ) : (init : σ) → RBMap α β cmp → σ
   | b, ⟨t, _⟩ => t.fold f b
 

src/Lean/Elab/BuiltinCommand.lean

@@ -11,7 +11,6 @@ import Lean.Elab.Eval
 import Lean.Elab.Command
 import Lean.Elab.Open
 import Lean.Elab.SetOption
-import Lean.PrettyPrinter
 
 namespace Lean.Elab.Command
 

src/Lean/Elab/BuiltinNotation.lean

@@ -330,15 +330,6 @@ where
     return (← expandCDot? pairs).getD pairs
   | _ => Macro.throwUnsupported
 
-@[builtin_macro Lean.Parser.Term.ptuple] def expandPTuple : Macro
-  | `(()ₚ) => ``(PUnit.unit)
-  | `(($e, $es,*)ₚ) => mkPPairs (#[e] ++ es)
-  | _ => Macro.throwUnsupported
-
-@[builtin_macro Lean.Parser.Term.mtuple] def expandMTuple : Macro
-  | `(($e, $es,*)ₘ) => mkMPairs (#[e] ++ es)
-  | _ => Macro.throwUnsupported
-
 @[builtin_macro Lean.Parser.Term.typeAscription] def expandTypeAscription : Macro
   | `(($e : $(type)?)) => do
     match (← expandCDot? e) with

src/Lean/Elab/MutualDef.lean

@@ -728,12 +728,26 @@ def insertReplacementForLetRecs (r : Replacement) (letRecClosures : List LetRecC
   letRecClosures.foldl (init := r) fun r c =>
     r.insert c.toLift.fvarId c.closed
 
+def isApplicable (r : Replacement) (e : Expr) : Bool :=
+  Option.isSome <| e.findExt? fun e =>
+    if e.hasFVar then
+      match e with
+      | .fvar fvarId => if r.contains fvarId then .found else .done
+      | _ => .visit
+    else
+      .done
+
 def Replacement.apply (r : Replacement) (e : Expr) : Expr :=
-  e.replace fun e => match e with
-    | .fvar fvarId => match r.find? fvarId with
-      | some c => some c
-      | _      => none
-    | _ => none
+  -- Remark: if `r` is not a singlenton, then declaration is using `mutual` or `let rec`,
+  -- and there is a big chance `isApplicable r e` is true.
+  if r.isSingleton && !isApplicable r e then
+    e
+  else
+    e.replace fun e => match e with
+      | .fvar fvarId => match r.find? fvarId with
+        | some c => some c
+        | _      => none
+      | _ => none
 
 def pushMain (preDefs : Array PreDefinition) (sectionVars : Array Expr) (mainHeaders : Array DefViewElabHeader) (mainVals : Array Expr)
     : TermElabM (Array PreDefinition) :=
@@ -923,6 +937,7 @@ where
             trace[Elab.definition] "{preDef.declName} : {preDef.type} :=\n{preDef.value}"
           let preDefs ← withLevelNames allUserLevelNames <| levelMVarToParamPreDecls preDefs
           let preDefs ← instantiateMVarsAtPreDecls preDefs
+          let preDefs ← shareCommonPreDefs preDefs
           let preDefs ← fixLevelParams preDefs scopeLevelNames allUserLevelNames
           for preDef in preDefs do
             trace[Elab.definition] "after eraseAuxDiscr, {preDef.declName} : {preDef.type} :=\n{preDef.value}"

src/Lean/Elab/PreDefinition/Basic.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Init.ShareCommon
 import Lean.Compiler.NoncomputableAttr
 import Lean.Util.CollectLevelParams
 import Lean.Meta.AbstractNestedProofs
@@ -52,20 +53,21 @@ private def getLevelParamsPreDecls (preDefs : Array PreDefinition) (scopeLevelNa
   | Except.error msg      => throwError msg
   | Except.ok levelParams => pure levelParams
 
-def fixLevelParams (preDefs : Array PreDefinition) (scopeLevelNames allUserLevelNames : List Name) : TermElabM (Array PreDefinition) :=
-do profileitM Exception s!"fix level params" (← getOptions) do
-  -- We used to use `shareCommon` here, but is was a bottleneck
-  let levelParams ← getLevelParamsPreDecls preDefs scopeLevelNames allUserLevelNames
-  let us := levelParams.map mkLevelParam
-  let fixExpr (e : Expr) : Expr :=
-    e.replace fun c => match c with
-      | Expr.const declName _ => if preDefs.any fun preDef => preDef.declName == declName then some $ Lean.mkConst declName us else none
-      | _ => none
-  return preDefs.map fun preDef =>
-    { preDef with
-      type        := fixExpr preDef.type,
-      value       := fixExpr preDef.value,
-      levelParams := levelParams }
+def fixLevelParams (preDefs : Array PreDefinition) (scopeLevelNames allUserLevelNames : List Name) : TermElabM (Array PreDefinition) := do
+  profileitM Exception s!"fix level params" (← getOptions) do
+    withTraceNode `Elab.def.fixLevelParams (fun _ => return m!"fix level params") do
+      -- We used to use `shareCommon` here, but is was a bottleneck
+      let levelParams ← getLevelParamsPreDecls preDefs scopeLevelNames allUserLevelNames
+      let us := levelParams.map mkLevelParam
+      let fixExpr (e : Expr) : Expr :=
+        e.replace fun c => match c with
+          | Expr.const declName _ => if preDefs.any fun preDef => preDef.declName == declName then some $ Lean.mkConst declName us else none
+          | _ => none
+      return preDefs.map fun preDef =>
+        { preDef with
+          type        := fixExpr preDef.type,
+          value       := fixExpr preDef.value,
+          levelParams := levelParams }
 
 def applyAttributesOf (preDefs : Array PreDefinition) (applicationTime : AttributeApplicationTime) : TermElabM Unit := do
   for preDef in preDefs do
@@ -211,4 +213,17 @@ def checkCodomainsLevel (preDefs : Array PreDefinition) : MetaM Unit := do
             m!"for `{preDefs[0]!.declName}` is{indentExpr type₀} : {← inferType type₀}\n" ++
             m!"and for `{preDefs[i]!.declName}` is{indentExpr typeᵢ} : {← inferType typeᵢ}"
 
+def shareCommonPreDefs (preDefs : Array PreDefinition) : CoreM (Array PreDefinition) := do
+  profileitM Exception "share common exprs" (← getOptions) do
+    withTraceNode `Elab.def.maxSharing (fun _ => return m!"share common exprs") do
+      let mut es := #[]
+      for preDef in preDefs do
+        es := es.push preDef.type |>.push preDef.value
+      es := ShareCommon.shareCommon' es
+      let mut result := #[]
+      for h : i in [:preDefs.size] do
+        let preDef := preDefs[i]
+        result := result.push { preDef with type := es[2*i]!, value := es[2*i+1]! }
+      return result
+
 end Lean.Elab

src/Lean/Elab/PreDefinition/Main.lean

@@ -152,69 +152,71 @@ def shouldUseWF (preDefs : Array PreDefinition) : Bool :=
     preDef.termination.decreasingBy?.isSome
 
 
-def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := withLCtx {} {} do profileitM Exception "add pre-definitions" (← getOptions) do
-  for preDef in preDefs do
-    trace[Elab.definition.body] "{preDef.declName} : {preDef.type} :=\n{preDef.value}"
-  let preDefs ← preDefs.mapM ensureNoUnassignedMVarsAtPreDef
-  let preDefs ← betaReduceLetRecApps preDefs
-  let cliques := partitionPreDefs preDefs
-  for preDefs in cliques do
-    trace[Elab.definition.scc] "{preDefs.map (·.declName)}"
-    if preDefs.size == 1 && isNonRecursive preDefs[0]! then
-      /-
-      We must erase `recApp` annotations even when `preDef` is not recursive
-      because it may use another recursive declaration in the same mutual block.
-      See issue #2321
-      -/
-      let preDef ← eraseRecAppSyntax preDefs[0]!
-      ensureEqnReservedNamesAvailable preDef.declName
-      if preDef.modifiers.isNoncomputable then
-        addNonRec preDef
-      else
-        addAndCompileNonRec preDef
-      preDef.termination.ensureNone "not recursive"
-    else if preDefs.any (·.modifiers.isUnsafe) then
-      addAndCompileUnsafe preDefs
-      preDefs.forM (·.termination.ensureNone "unsafe")
-    else if preDefs.any (·.modifiers.isPartial) then
+def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := withLCtx {} {} do
+  profileitM Exception "process pre-definitions" (← getOptions) do
+    withTraceNode `Elab.def.processPreDef (fun _ => return m!"process pre-definitions") do
       for preDef in preDefs do
-        if preDef.modifiers.isPartial && !(← whnfD preDef.type).isForall then
-          withRef preDef.ref <| throwError "invalid use of 'partial', '{preDef.declName}' is not a function{indentExpr preDef.type}"
-      addAndCompilePartial preDefs
-      preDefs.forM (·.termination.ensureNone "partial")
-    else
-      ensureFunIndReservedNamesAvailable preDefs
-      try
-        checkCodomainsLevel preDefs
-        checkTerminationByHints preDefs
-        let termArg?s ← elabTerminationByHints preDefs
-        if shouldUseStructural preDefs then
-          structuralRecursion preDefs termArg?s
-        else if shouldUseWF preDefs then
-          wfRecursion preDefs termArg?s
+        trace[Elab.definition.body] "{preDef.declName} : {preDef.type} :=\n{preDef.value}"
+      let preDefs ← preDefs.mapM ensureNoUnassignedMVarsAtPreDef
+      let preDefs ← betaReduceLetRecApps preDefs
+      let cliques := partitionPreDefs preDefs
+      for preDefs in cliques do
+        trace[Elab.definition.scc] "{preDefs.map (·.declName)}"
+        if preDefs.size == 1 && isNonRecursive preDefs[0]! then
+          /-
+          We must erase `recApp` annotations even when `preDef` is not recursive
+          because it may use another recursive declaration in the same mutual block.
+          See issue #2321
+          -/
+          let preDef ← eraseRecAppSyntax preDefs[0]!
+          ensureEqnReservedNamesAvailable preDef.declName
+          if preDef.modifiers.isNoncomputable then
+            addNonRec preDef
+          else
+            addAndCompileNonRec preDef
+          preDef.termination.ensureNone "not recursive"
+        else if preDefs.any (·.modifiers.isUnsafe) then
+          addAndCompileUnsafe preDefs
+          preDefs.forM (·.termination.ensureNone "unsafe")
+        else if preDefs.any (·.modifiers.isPartial) then
+          for preDef in preDefs do
+            if preDef.modifiers.isPartial && !(← whnfD preDef.type).isForall then
+              withRef preDef.ref <| throwError "invalid use of 'partial', '{preDef.declName}' is not a function{indentExpr preDef.type}"
+          addAndCompilePartial preDefs
+          preDefs.forM (·.termination.ensureNone "partial")
         else
-          withRef (preDefs[0]!.ref) <| mapError
-            (orelseMergeErrors
-              (structuralRecursion preDefs termArg?s)
-              (wfRecursion preDefs termArg?s))
-            (fun msg =>
-              let preDefMsgs := preDefs.toList.map (MessageData.ofExpr $ mkConst ·.declName)
-              m!"fail to show termination for{indentD (MessageData.joinSep preDefMsgs Format.line)}\nwith errors\n{msg}")
-      catch ex =>
-        logException ex
-        let s ← saveState
-        try
-          if preDefs.all fun preDef => preDef.kind == DefKind.def || preDefs.all fun preDef => preDef.kind == DefKind.abbrev then
-            -- try to add as partial definition
+          ensureFunIndReservedNamesAvailable preDefs
+          try
+            checkCodomainsLevel preDefs
+            checkTerminationByHints preDefs
+            let termArg?s ← elabTerminationByHints preDefs
+            if shouldUseStructural preDefs then
+              structuralRecursion preDefs termArg?s
+            else if shouldUseWF preDefs then
+              wfRecursion preDefs termArg?s
+            else
+              withRef (preDefs[0]!.ref) <| mapError
+                (orelseMergeErrors
+                  (structuralRecursion preDefs termArg?s)
+                  (wfRecursion preDefs termArg?s))
+                (fun msg =>
+                  let preDefMsgs := preDefs.toList.map (MessageData.ofExpr $ mkConst ·.declName)
+                  m!"fail to show termination for{indentD (MessageData.joinSep preDefMsgs Format.line)}\nwith errors\n{msg}")
+          catch ex =>
+            logException ex
+            let s ← saveState
             try
-              addAndCompilePartial preDefs (useSorry := true)
-            catch _ =>
-              -- Compilation failed try again just as axiom
-              s.restore
-              addAsAxioms preDefs
-          else if preDefs.all fun preDef => preDef.kind == DefKind.theorem then
-            addAsAxioms preDefs
-        catch _ => s.restore
+              if preDefs.all fun preDef => preDef.kind == DefKind.def || preDefs.all fun preDef => preDef.kind == DefKind.abbrev then
+                -- try to add as partial definition
+                try
+                  addAndCompilePartial preDefs (useSorry := true)
+                catch _ =>
+                  -- Compilation failed try again just as axiom
+                  s.restore
+                  addAsAxioms preDefs
+              else if preDefs.all fun preDef => preDef.kind == DefKind.theorem then
+                addAsAxioms preDefs
+            catch _ => s.restore
 
 builtin_initialize
   registerTraceClass `Elab.definition.body

src/Lean/Elab/PreDefinition/TerminationArgument.lean

@@ -10,7 +10,7 @@ import Lean.Elab.Term
 import Lean.Elab.Binders
 import Lean.Elab.SyntheticMVars
 import Lean.Elab.PreDefinition.TerminationHint
-import Lean.PrettyPrinter.Delaborator
+import Lean.PrettyPrinter.Delaborator.Basic
 
 /-!
 This module contains
@@ -115,7 +115,7 @@ def TerminationArgument.delab (arity : Nat) (extraParams : Nat) (termArg : Termi
       -- any variable not mentioned syntatically (it may appear in the `Expr`, so do not just use
       -- `e.bindingBody!.hasLooseBVar`) should be delaborated as a hole.
       let vars  : TSyntaxArray [`ident, `Lean.Parser.Term.hole] :=
-        Array.map (fun (i : Ident) => if hasIdent i.getId stxBody then i else hole) vars
+        Array.map (fun (i : Ident) => if stxBody.raw.hasIdent i.getId then i else hole) vars
       -- drop trailing underscores
       let mut vars := vars
       while ! vars.isEmpty && vars.back.raw.isOfKind ``hole do vars := vars.pop

src/Lean/Meta/AppBuilder.lean

@@ -504,6 +504,14 @@ def mkArrayLit (type : Expr) (xs : List Expr) : MetaM Expr := do
   let listLit ← mkListLit type xs
   return mkApp (mkApp (mkConst ``List.toArray [u]) type) listLit
 
+def mkNone (type : Expr) : MetaM Expr := do
+  let u ← getDecLevel type
+  return mkApp (mkConst ``Option.none [u]) type
+
+def mkSome (type value : Expr) : MetaM Expr := do
+  let u ← getDecLevel type
+  return mkApp2 (mkConst ``Option.some [u]) type value
+
 def mkSorry (type : Expr) (synthetic : Bool) : MetaM Expr := do
   let u ← getLevel type
   return mkApp2 (mkConst ``sorryAx [u]) type (toExpr synthetic)

src/Lean/Meta/LitValues.lean

@@ -176,4 +176,48 @@ def litToCtor (e : Expr) : MetaM Expr := do
     return mkApp3 (mkConst ``Fin.mk) n i h
   return e
 
+/--
+Check if an expression is a list literal (i.e. a nested chain of `List.cons`, ending at a `List.nil`),
+where each element is "recognised" by a given function `f : Expr → MetaM (Option α)`,
+and return the array of recognised values.
+-/
+partial def getListLitOf? (e : Expr) (f : Expr → MetaM (Option α)) : MetaM (Option (Array α)) := do
+  let mut e ← instantiateMVars e.consumeMData
+  let mut r := #[]
+  while true do
+    match_expr e with
+    | List.nil _ => break
+    | List.cons _ a as => do
+      let some a ← f a | return none
+      r := r.push a
+      e := as
+    | _ => return none
+  return some r
+
+/--
+Check if an expression is a list literal (i.e. a nested chain of `List.cons`, ending at a `List.nil`),
+returning the array of `Expr` values.
+-/
+def getListLit? (e : Expr) : MetaM (Option (Array Expr)) := getListLitOf? e fun s => return some s
+
+/--
+Check if an expression is an array literal
+(i.e. `List.toArray` applied to a nested chain of `List.cons`, ending at a `List.nil`),
+where each element is "recognised" by a given function `f : Expr → MetaM (Option α)`,
+and return the array of recognised values.
+-/
+def getArrayLitOf? (e : Expr) (f : Expr → MetaM (Option α)) : MetaM (Option (Array α)) := do
+  let e ← instantiateMVars e.consumeMData
+  match_expr e with
+  | List.toArray _ as => getListLitOf? as f
+  | _ => return none
+
+/--
+Check if an expression is an array literal
+(i.e. `List.toArray` applied to a nested chain of `List.cons`, ending at a `List.nil`),
+returning the array of `Expr` values.
+-/
+def getArrayLit? (e : Expr) : MetaM (Option (Array Expr)) := getArrayLitOf? e fun s => return some s
+
+
 end Lean.Meta

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs.lean

@@ -13,3 +13,4 @@ import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Char
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.String
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.List
+import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Array

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Array.lean

@@ -0,0 +1,36 @@
+/-
+Copyright (c) 2024 Lean FRO. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Lean.Meta.LitValues
+import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
+
+namespace Array
+open Lean Meta Simp
+
+/-- Simplification procedure for `#[...][n]` for `n` a `Nat` literal. -/
+builtin_dsimproc [simp, seval] reduceGetElem (@GetElem.getElem (Array _) Nat _ _ _ _ _ _) := fun e => do
+  let_expr GetElem.getElem _ _ _ _ _ xs n _ ← e | return .continue
+  let some n ← Nat.fromExpr? n | return .continue
+  let some xs ← getArrayLit? xs | return .continue
+  return .done <| xs[n]!
+
+/-- Simplification procedure for `#[...][n]?` for `n` a `Nat` literal. -/
+builtin_dsimproc [simp, seval] reduceGetElem? (@GetElem?.getElem? (Array _) Nat _ _ _ _ _) := fun e => do
+  let_expr GetElem?.getElem? _ _ α _ _ xs n ← e | return .continue
+  let some n ← Nat.fromExpr? n | return .continue
+  let some xs ← getArrayLit? xs | return .continue
+  let r ← if h : n < xs.size then mkSome α xs[n] else mkNone α
+  return .done r
+
+/-- Simplification procedure for `#[...][n]!` for `n` a `Nat` literal. -/
+builtin_dsimproc [simp, seval] reduceGetElem! (@GetElem?.getElem! (Array _) Nat _ _ _ _ _ _) := fun e => do
+  let_expr GetElem?.getElem! _ _ α _ _ I xs n ← e | return .continue
+  let some n ← Nat.fromExpr? n | return .continue
+  let some xs ← getArrayLit? xs | return .continue
+  let r ← if h : n < xs.size then pure xs[n] else mkDefault α
+  return .done r
+
+end Array

src/Lean/Parser/Term.lean

@@ -179,14 +179,6 @@ do not yield the right result.
 @[builtin_term_parser] def tuple := leading_parser
   "(" >> optional (withoutPosition (withoutForbidden (termParser >> ", " >> sepBy1 termParser ", " (allowTrailingSep := true)))) >> ")"
 
-/-- Universe polymorphic tuple notation; `()ₚ` is short for `PUnit.unit`, `(a, b, c)ₚ` for `PProd.mk a (PProd.mk b c)`, etc. -/
-@[builtin_term_parser] def ptuple := leading_parser
-  "(" >> optional (withoutPosition (withoutForbidden (termParser >> ", " >> sepBy1 termParser ", " (allowTrailingSep := true)))) >> ")ₚ"
-
-/-- Universe monomorphic tuple notation; `(a, b, c)ₘ` for `MProd.mk a (MProd.mk b c)`, etc. -/
-@[builtin_term_parser] def mtuple := leading_parser
-  "(" >> withoutPosition (withoutForbidden (termParser >> ", " >> sepBy1 termParser ", " (allowTrailingSep := true))) >> ")ₘ"
-
 /--
 Parentheses, used for grouping expressions (e.g., `a * (b + c)`).
 Can also be used for creating simple functions when combined with `·`. Here are some examples:

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -199,6 +199,10 @@ def unexpandStructureInstance (stx : Syntax) : Delab := whenPPOption getPPStruct
   let mut fields := #[]
   guard $ fieldNames.size == stx[1].getNumArgs
   if hasPPUsingAnonymousConstructorAttribute env s.induct then
+    /- Note that we don't flatten anonymous constructor notation. Only a complete such notation receives TermInfo,
+       and flattening would cause the flattened-in notation to lose its TermInfo.
+       Potentially it would be justified to flatten anonymous constructor notation when the terms are
+       from the same type family (think `Sigma`), but for now users can write a custom delaborator in such instances. -/
     return ← withTypeAscription (cond := (← withType <| getPPOption getPPStructureInstanceType)) do
       `(⟨$[$(stx[1].getArgs)],*⟩)
   let args := e.getAppArgs
@@ -769,16 +773,6 @@ def delabMData : Delab := do
   else
     withMDataOptions delab
 
-/--
-Check for a `Syntax.ident` of the given name anywhere in the tree.
-This is usually a bad idea since it does not check for shadowing bindings,
-but in the delaborator we assume that bindings are never shadowed.
--/
-partial def hasIdent (id : Name) : Syntax → Bool
-  | Syntax.ident _ _ id' _ => id == id'
-  | Syntax.node _ _ args   => args.any (hasIdent id)
-  | _                      => false
-
 /--
 Return `true` iff current binder should be merged with the nested
 binder, if any, into a single binder group:
@@ -824,7 +818,7 @@ def delabLam : Delab :=
     let e ← getExpr
     let stxT ← withBindingDomain delab
     let ppTypes ← getPPOption getPPFunBinderTypes
-    let usedDownstream := curNames.any (fun n => hasIdent n.getId stxBody)
+    let usedDownstream := curNames.any (fun n => stxBody.hasIdent n.getId)
 
     -- leave lambda implicit if possible
     -- TODO: for now we just always block implicit lambdas when delaborating. We can revisit.
@@ -1135,6 +1129,24 @@ def delabSigma : Delab := delabSigmaCore (sigma := true)
 @[builtin_delab app.PSigma]
 def delabPSigma : Delab := delabSigmaCore (sigma := false)
 
+-- PProd and MProd value delaborator
+-- (like pp_using_anonymous_constructor but flattening nested tuples)
+
+def delabPProdMkCore (mkName : Name) : Delab := whenNotPPOption getPPExplicit <| whenPPOption getPPNotation do
+  guard <| (← getExpr).getAppNumArgs == 4
+  let a ← withAppFn <| withAppArg delab
+  let b ← withAppArg <| delab
+  if (← getExpr).appArg!.isAppOfArity mkName 4 then
+    if let `(⟨$xs,*⟩) := b then
+      return ← `(⟨$a, $xs,*⟩)
+  `(⟨$a, $b⟩)
+
+@[builtin_delab app.PProd.mk]
+def delabPProdMk : Delab := delabPProdMkCore ``PProd.mk
+
+@[builtin_delab app.MProd.mk]
+def delabMProdMk : Delab := delabPProdMkCore ``MProd.mk
+
 partial def delabDoElems : DelabM (List Syntax) := do
   let e ← getExpr
   if e.isAppOfArity ``Bind.bind 6 then

src/Lean/Syntax.lean

@@ -164,6 +164,16 @@ def asNode : Syntax → SyntaxNode
 def getIdAt (stx : Syntax) (i : Nat) : Name :=
   (stx.getArg i).getId
 
+/--
+Check for a `Syntax.ident` of the given name anywhere in the tree.
+This is usually a bad idea since it does not check for shadowing bindings,
+but in the delaborator we assume that bindings are never shadowed.
+-/
+partial def hasIdent (id : Name) : Syntax → Bool
+  | ident _ _ id' _ => id == id'
+  | node _ _ args   => args.any (hasIdent id)
+  | _               => false
+
 @[inline] def modifyArgs (stx : Syntax) (fn : Array Syntax → Array Syntax) : Syntax :=
   match stx with
   | node i k args => node i k (fn args)

src/Lean/Util.lean

@@ -31,3 +31,4 @@ import Lean.Util.FileSetupInfo
 import Lean.Util.Heartbeats
 import Lean.Util.SearchPath
 import Lean.Util.SafeExponentiation
+import Lean.Util.NumObjs

src/Lean/Util/NumObjs.lean

@@ -0,0 +1,47 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Expr
+import Lean.Util.PtrSet
+
+namespace Lean.Expr
+namespace NumObjs
+
+unsafe structure State where
+ visited : PtrSet Expr := mkPtrSet
+ counter : Nat := 0
+
+unsafe abbrev M := StateM State
+
+unsafe def visit (e : Expr) : M Unit :=
+  unless (← get).visited.contains e do
+    modify fun { visited, counter } => { visited := visited.insert e, counter := counter + 1 }
+    match e with
+      | .forallE _ d b _ => visit d; visit b
+      | .lam _ d b _     => visit d; visit b
+      | .mdata _ b       => visit b
+      | .letE _ t v b _  => visit t; visit v; visit b
+      | .app f a         => visit f; visit a
+      | .proj _ _ b      => visit b
+      | _                => return ()
+
+unsafe def main (e : Expr) : Nat :=
+  let (_, s) := NumObjs.visit e |>.run {}
+  s.counter
+
+end NumObjs
+
+/--
+Returns the number of allocated `Expr` objects in the given expression `e`.
+
+This operation is performed in `IO` because the result depends on the memory representation of the object.
+
+Note: Use this function primarily for diagnosing performance issues.
+-/
+def numObjs (e : Expr) : IO Nat :=
+  return unsafe NumObjs.main e
+
+end Lean.Expr

src/Lean/Widget/InteractiveCode.lean

@@ -5,7 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Wojciech Nawrocki
 -/
 prelude
-import Lean.PrettyPrinter
 import Lean.Server.Rpc.Basic
 import Lean.Server.InfoUtils
 import Lean.Widget.TaggedText

src/Std/Data/DHashMap/Basic.lean

@@ -30,6 +30,8 @@ universe u v w
 
 variable {α : Type u} {β : α → Type v} {δ : Type w} {m : Type w → Type w} [Monad m]
 
+variable {_ : BEq α} {_ : Hashable α}
+
 namespace Std
 
 open DHashMap.Internal DHashMap.Internal.List
@@ -42,6 +44,9 @@ and an array of buckets, where each bucket is a linked list of key-value pais. T
 is always a power of two. The hash map doubles its size upon inserting an element such that the
 number of elements is more than 75% of the number of buckets.
 
+The hash table is backed by an `Array`. Users should make sure that the hash map is used linearly to
+avoid expensive copies.
+
 The hash map uses `==` (provided by the `BEq` typeclass) to compare keys and `hash` (provided by
 the `Hashable` typeclass) to hash them. To ensure that the operations behave as expected, `==`
 should be an equivalence relation and `a == b` should imply `hash a = hash b` (see also the
@@ -66,34 +71,34 @@ instance [BEq α] [Hashable α] : EmptyCollection (DHashMap α β) where
 instance [BEq α] [Hashable α] : Inhabited (DHashMap α β) where
   default := ∅
 
-@[inline, inherit_doc Raw.insert] def insert [BEq α] [Hashable α] (m : DHashMap α β) (a : α)
+@[inline, inherit_doc Raw.insert] def insert (m : DHashMap α β) (a : α)
     (b : β a) : DHashMap α β :=
   ⟨Raw₀.insert ⟨m.1, m.2.size_buckets_pos⟩ a b, .insert₀ m.2⟩
 
-@[inline, inherit_doc Raw.insertIfNew] def insertIfNew [BEq α] [Hashable α] (m : DHashMap α β)
+@[inline, inherit_doc Raw.insertIfNew] def insertIfNew (m : DHashMap α β)
     (a : α) (b : β a) : DHashMap α β :=
   ⟨Raw₀.insertIfNew ⟨m.1, m.2.size_buckets_pos⟩ a b, .insertIfNew₀ m.2⟩
 
-@[inline, inherit_doc Raw.containsThenInsert] def containsThenInsert [BEq α] [Hashable α]
+@[inline, inherit_doc Raw.containsThenInsert] def containsThenInsert
     (m : DHashMap α β) (a : α) (b : β a) : Bool × DHashMap α β :=
   let m' := Raw₀.containsThenInsert ⟨m.1, m.2.size_buckets_pos⟩ a b
   ⟨m'.1, ⟨m'.2.1, .containsThenInsert₀ m.2⟩⟩
 
-@[inline, inherit_doc Raw.containsThenInsertIfNew] def containsThenInsertIfNew [BEq α] [Hashable α]
+@[inline, inherit_doc Raw.containsThenInsertIfNew] def containsThenInsertIfNew
     (m : DHashMap α β) (a : α) (b : β a) : Bool × DHashMap α β :=
   let m' := Raw₀.containsThenInsertIfNew ⟨m.1, m.2.size_buckets_pos⟩ a b
   ⟨m'.1, ⟨m'.2.1, .containsThenInsertIfNew₀ m.2⟩⟩
 
-@[inline, inherit_doc Raw.getThenInsertIfNew?] def getThenInsertIfNew? [BEq α] [Hashable α]
+@[inline, inherit_doc Raw.getThenInsertIfNew?] def getThenInsertIfNew?
     [LawfulBEq α] (m : DHashMap α β) (a : α) (b : β a) : Option (β a) × DHashMap α β :=
   let m' := Raw₀.getThenInsertIfNew? ⟨m.1, m.2.size_buckets_pos⟩ a b
   ⟨m'.1, ⟨m'.2.1, .getThenInsertIfNew?₀ m.2⟩⟩
 
-@[inline, inherit_doc Raw.get?] def get? [BEq α] [LawfulBEq α] [Hashable α] (m : DHashMap α β)
+@[inline, inherit_doc Raw.get?] def get? [LawfulBEq α] (m : DHashMap α β)
     (a : α) : Option (β a) :=
   Raw₀.get? ⟨m.1, m.2.size_buckets_pos⟩ a
 
-@[inline, inherit_doc Raw.contains] def contains [BEq α] [Hashable α] (m : DHashMap α β) (a : α) :
+@[inline, inherit_doc Raw.contains] def contains (m : DHashMap α β) (a : α) :
     Bool :=
   Raw₀.contains ⟨m.1, m.2.size_buckets_pos⟩ a
 
@@ -103,19 +108,19 @@ instance [BEq α] [Hashable α] : Membership α (DHashMap α β) where
 instance [BEq α] [Hashable α] {m : DHashMap α β} {a : α} : Decidable (a ∈ m) :=
   show Decidable (m.contains a) from inferInstance
 
-@[inline, inherit_doc Raw.get] def get [BEq α] [Hashable α] [LawfulBEq α] (m : DHashMap α β) (a : α)
+@[inline, inherit_doc Raw.get] def get [LawfulBEq α] (m : DHashMap α β) (a : α)
     (h : a ∈ m) : β a :=
   Raw₀.get ⟨m.1, m.2.size_buckets_pos⟩ a h
 
-@[inline, inherit_doc Raw.get!] def get! [BEq α] [Hashable α] [LawfulBEq α] (m : DHashMap α β)
+@[inline, inherit_doc Raw.get!] def get! [LawfulBEq α] (m : DHashMap α β)
     (a : α) [Inhabited (β a)] : β a :=
   Raw₀.get! ⟨m.1, m.2.size_buckets_pos⟩ a
 
-@[inline, inherit_doc Raw.getD] def getD [BEq α] [Hashable α] [LawfulBEq α] (m : DHashMap α β)
+@[inline, inherit_doc Raw.getD] def getD [LawfulBEq α] (m : DHashMap α β)
     (a : α) (fallback : β a) : β a :=
   Raw₀.getD ⟨m.1, m.2.size_buckets_pos⟩ a fallback
 
-@[inline, inherit_doc Raw.erase] def erase [BEq α] [Hashable α] (m : DHashMap α β) (a : α) :
+@[inline, inherit_doc Raw.erase] def erase (m : DHashMap α β) (a : α) :
     DHashMap α β :=
   ⟨Raw₀.erase ⟨m.1, m.2.size_buckets_pos⟩ a, .erase₀ m.2⟩
 
@@ -123,57 +128,57 @@ section
 
 variable {β : Type v}
 
-@[inline, inherit_doc Raw.Const.get?] def Const.get? [BEq α] [Hashable α]
+@[inline, inherit_doc Raw.Const.get?] def Const.get?
     (m : DHashMap α (fun _ => β)) (a : α) : Option β :=
   Raw₀.Const.get? ⟨m.1, m.2.size_buckets_pos⟩ a
 
-@[inline, inherit_doc Raw.Const.get] def Const.get [BEq α] [Hashable α]
+@[inline, inherit_doc Raw.Const.get] def Const.get
     (m : DHashMap α (fun _ => β)) (a : α) (h : a ∈ m) : β :=
   Raw₀.Const.get ⟨m.1, m.2.size_buckets_pos⟩ a h
 
-@[inline, inherit_doc Raw.Const.getD] def Const.getD [BEq α] [Hashable α]
+@[inline, inherit_doc Raw.Const.getD] def Const.getD
     (m : DHashMap α (fun _ => β)) (a : α) (fallback : β) : β :=
   Raw₀.Const.getD ⟨m.1, m.2.size_buckets_pos⟩ a fallback
 
-@[inline, inherit_doc Raw.Const.get!] def Const.get! [BEq α] [Hashable α] [Inhabited β]
+@[inline, inherit_doc Raw.Const.get!] def Const.get! [Inhabited β]
     (m : DHashMap α (fun _ => β)) (a : α) : β :=
   Raw₀.Const.get! ⟨m.1, m.2.size_buckets_pos⟩ a
 
-@[inline, inherit_doc Raw.Const.getThenInsertIfNew?] def Const.getThenInsertIfNew? [BEq α]
-    [Hashable α] (m : DHashMap α (fun _ => β)) (a : α) (b : β) :
+@[inline, inherit_doc Raw.Const.getThenInsertIfNew?] def Const.getThenInsertIfNew?
+    (m : DHashMap α (fun _ => β)) (a : α) (b : β) :
     Option β × DHashMap α (fun _ => β) :=
   let m' := Raw₀.Const.getThenInsertIfNew? ⟨m.1, m.2.size_buckets_pos⟩ a b
   ⟨m'.1, ⟨m'.2.1, .constGetThenInsertIfNew?₀ m.2⟩⟩
 
 end
 
-@[inline, inherit_doc Raw.size] def size [BEq α] [Hashable α] (m : DHashMap α β) : Nat :=
+@[inline, inherit_doc Raw.size] def size (m : DHashMap α β) : Nat :=
   m.1.size
 
-@[inline, inherit_doc Raw.isEmpty] def isEmpty [BEq α] [Hashable α] (m : DHashMap α β) : Bool :=
+@[inline, inherit_doc Raw.isEmpty] def isEmpty (m : DHashMap α β) : Bool :=
   m.1.isEmpty
 
 section Unverified
 
 /-! We currently do not provide lemmas for the functions below. -/
 
-@[inline, inherit_doc Raw.filter] def filter [BEq α] [Hashable α] (f : (a : α) → β a → Bool)
+@[inline, inherit_doc Raw.filter] def filter (f : (a : α) → β a → Bool)
     (m : DHashMap α β) : DHashMap α β :=
   ⟨Raw₀.filter f ⟨m.1, m.2.size_buckets_pos⟩, .filter₀ m.2⟩
 
-@[inline, inherit_doc Raw.foldM] def foldM [BEq α] [Hashable α] (f : δ → (a : α) → β a → m δ)
+@[inline, inherit_doc Raw.foldM] def foldM (f : δ → (a : α) → β a → m δ)
     (init : δ) (b : DHashMap α β) : m δ :=
   b.1.foldM f init
 
-@[inline, inherit_doc Raw.fold] def fold [BEq α] [Hashable α] (f : δ → (a : α) → β a → δ)
+@[inline, inherit_doc Raw.fold] def fold (f : δ → (a : α) → β a → δ)
     (init : δ) (b : DHashMap α β) : δ :=
   b.1.fold f init
 
-@[inline, inherit_doc Raw.forM] def forM [BEq α] [Hashable α] (f : (a : α) → β a → m PUnit)
+@[inline, inherit_doc Raw.forM] def forM (f : (a : α) → β a → m PUnit)
     (b : DHashMap α β) : m PUnit :=
   b.1.forM f
 
-@[inline, inherit_doc Raw.forIn] def forIn [BEq α] [Hashable α]
+@[inline, inherit_doc Raw.forIn] def forIn
     (f : (a : α) → β a → δ → m (ForInStep δ)) (init : δ) (b : DHashMap α β) : m δ :=
   b.1.forIn f init
 
@@ -183,49 +188,49 @@ instance [BEq α] [Hashable α] : ForM m (DHashMap α β) ((a : α) × β a) whe
 instance [BEq α] [Hashable α] : ForIn m (DHashMap α β) ((a : α) × β a) where
   forIn m init f := m.forIn (fun a b acc => f ⟨a, b⟩ acc) init
 
-@[inline, inherit_doc Raw.toList] def toList [BEq α] [Hashable α] (m : DHashMap α β) :
+@[inline, inherit_doc Raw.toList] def toList (m : DHashMap α β) :
     List ((a : α) × β a) :=
   m.1.toList
 
-@[inline, inherit_doc Raw.toArray] def toArray [BEq α] [Hashable α] (m : DHashMap α β) :
+@[inline, inherit_doc Raw.toArray] def toArray (m : DHashMap α β) :
     Array ((a : α) × β a) :=
   m.1.toArray
 
-@[inline, inherit_doc Raw.Const.toList] def Const.toList {β : Type v} [BEq α] [Hashable α]
+@[inline, inherit_doc Raw.Const.toList] def Const.toList {β : Type v}
     (m : DHashMap α (fun _ => β)) : List (α × β) :=
   Raw.Const.toList m.1
 
-@[inline, inherit_doc Raw.Const.toArray] def Const.toArray {β : Type v} [BEq α] [Hashable α]
+@[inline, inherit_doc Raw.Const.toArray] def Const.toArray {β : Type v}
     (m : DHashMap α (fun _ => β)) : Array (α × β) :=
   Raw.Const.toArray m.1
 
-@[inline, inherit_doc Raw.keys] def keys [BEq α] [Hashable α] (m : DHashMap α β) : List α :=
+@[inline, inherit_doc Raw.keys] def keys (m : DHashMap α β) : List α :=
   m.1.keys
 
-@[inline, inherit_doc Raw.keysArray] def keysArray [BEq α] [Hashable α] (m : DHashMap α β) :
+@[inline, inherit_doc Raw.keysArray] def keysArray (m : DHashMap α β) :
     Array α :=
   m.1.keysArray
 
-@[inline, inherit_doc Raw.values] def values {β : Type v} [BEq α] [Hashable α]
+@[inline, inherit_doc Raw.values] def values {β : Type v}
     (m : DHashMap α (fun _ => β)) : List β :=
   m.1.values
 
-@[inline, inherit_doc Raw.valuesArray] def valuesArray {β : Type v} [BEq α] [Hashable α]
+@[inline, inherit_doc Raw.valuesArray] def valuesArray {β : Type v}
     (m : DHashMap α (fun _ => β)) : Array β :=
   m.1.valuesArray
 
-@[inline, inherit_doc Raw.insertMany] def insertMany [BEq α] [Hashable α] {ρ : Type w}
+@[inline, inherit_doc Raw.insertMany] def insertMany {ρ : Type w}
     [ForIn Id ρ ((a : α) × β a)] (m : DHashMap α β) (l : ρ) : DHashMap α β :=
   ⟨(Raw₀.insertMany ⟨m.1, m.2.size_buckets_pos⟩ l).1,
    (Raw₀.insertMany ⟨m.1, m.2.size_buckets_pos⟩ l).2 _ Raw.WF.insert₀ m.2⟩
 
-@[inline, inherit_doc Raw.Const.insertMany] def Const.insertMany {β : Type v} [BEq α] [Hashable α]
+@[inline, inherit_doc Raw.Const.insertMany] def Const.insertMany {β : Type v}
     {ρ : Type w} [ForIn Id ρ (α × β)] (m : DHashMap α (fun _ => β)) (l : ρ) :
     DHashMap α (fun _ => β) :=
   ⟨(Raw₀.Const.insertMany ⟨m.1, m.2.size_buckets_pos⟩ l).1,
    (Raw₀.Const.insertMany ⟨m.1, m.2.size_buckets_pos⟩ l).2 _ Raw.WF.insert₀ m.2⟩
 
-@[inline, inherit_doc Raw.Const.insertManyUnit] def Const.insertManyUnit [BEq α] [Hashable α]
+@[inline, inherit_doc Raw.Const.insertManyUnit] def Const.insertManyUnit
     {ρ : Type w} [ForIn Id ρ α] (m : DHashMap α (fun _ => Unit)) (l : ρ) :
     DHashMap α (fun _ => Unit) :=
   ⟨(Raw₀.Const.insertManyUnit ⟨m.1, m.2.size_buckets_pos⟩ l).1,
@@ -243,7 +248,7 @@ instance [BEq α] [Hashable α] : ForIn m (DHashMap α β) ((a : α) × β a) wh
     DHashMap α (fun _ => Unit) :=
   Const.insertManyUnit ∅ l
 
-@[inherit_doc Raw.Internal.numBuckets] def Internal.numBuckets [BEq α] [Hashable α]
+@[inherit_doc Raw.Internal.numBuckets] def Internal.numBuckets
     (m : DHashMap α β) : Nat :=
   Raw.Internal.numBuckets m.1
 

src/Std/Data/DHashMap/Internal/AssocList/Basic.lean

@@ -77,61 +77,61 @@ variable {β : Type v}
 /-- Internal implementation detail of the hash map -/
 def get? [BEq α] (a : α) : AssocList α (fun _ => β) → Option β
   | nil => none
-  | cons k v es => bif a == k then some v else get? a es
+  | cons k v es => bif k == a then some v else get? a es
 
 end
 
 /-- Internal implementation detail of the hash map -/
 def getCast? [BEq α] [LawfulBEq α] (a : α) : AssocList α β → Option (β a)
   | nil => none
-  | cons k v es => if h : a == k then some (cast (congrArg β (eq_of_beq h).symm) v)
+  | cons k v es => if h : k == a then some (cast (congrArg β (eq_of_beq h)) v)
       else es.getCast? a
 
 /-- Internal implementation detail of the hash map -/
 def contains [BEq α] (a : α) : AssocList α β → Bool
   | nil => false
-  | cons k _ l => a == k || l.contains a
+  | cons k _ l => k == a || l.contains a
 
 /-- Internal implementation detail of the hash map -/
 def get {β : Type v} [BEq α] (a : α) : (l : AssocList α (fun _ => β)) → l.contains a → β
-  | cons k v es, h => if hka : a == k then v else get a es
+  | cons k v es, h => if hka : k == a then v else get a es
       (by rw [← h, contains, Bool.of_not_eq_true hka, Bool.false_or])
 
 /-- Internal implementation detail of the hash map -/
 def getCast [BEq α] [LawfulBEq α] (a : α) : (l : AssocList α β) → l.contains a → β a
-  | cons k v es, h => if hka : a == k then cast (congrArg β (eq_of_beq hka).symm) v
+  | cons k v es, h => if hka : k == a then cast (congrArg β (eq_of_beq hka)) v
       else es.getCast a (by rw [← h, contains, Bool.of_not_eq_true hka, Bool.false_or])
 
 /-- Internal implementation detail of the hash map -/
 def getCast! [BEq α] [LawfulBEq α] (a : α) [Inhabited (β a)] : AssocList α β → β a
   | nil => panic! "key is not present in hash table"
-  | cons k v es => if h : a == k then cast (congrArg β (eq_of_beq h).symm) v else es.getCast! a
+  | cons k v es => if h : k == a then cast (congrArg β (eq_of_beq h)) v else es.getCast! a
 
 /-- Internal implementation detail of the hash map -/
 def get! {β : Type v} [BEq α] [Inhabited β] (a : α) : AssocList α (fun _ => β) → β
   | nil => panic! "key is not present in hash table"
-  | cons k v es => bif a == k then v else es.get! a
+  | cons k v es => bif k == a then v else es.get! a
 
 /-- Internal implementation detail of the hash map -/
 def getCastD [BEq α] [LawfulBEq α] (a : α) (fallback : β a) : AssocList α β → β a
   | nil => fallback
-  | cons k v es => if h : a == k then cast (congrArg β (eq_of_beq h).symm) v
+  | cons k v es => if h : k == a then cast (congrArg β (eq_of_beq h)) v
       else es.getCastD a fallback
 
 /-- Internal implementation detail of the hash map -/
 def getD {β : Type v} [BEq α] (a : α) (fallback : β) : AssocList α (fun _ => β) → β
   | nil => fallback
-  | cons k v es => bif a == k then v else es.getD a fallback
+  | cons k v es => bif k == a then v else es.getD a fallback
 
 /-- Internal implementation detail of the hash map -/
 def replace [BEq α] (a : α) (b : β a) : AssocList α β → AssocList α β
   | nil => nil
-  | cons k v l => bif a == k then cons a b l else cons k v (replace a b l)
+  | cons k v l => bif k == a then cons a b l else cons k v (replace a b l)
 
 /-- Internal implementation detail of the hash map -/
 def erase [BEq α] (a : α) : AssocList α β → AssocList α β
   | nil => nil
-  | cons k v l => bif a == k then l else cons k v (l.erase a)
+  | cons k v l => bif k == a then l else cons k v (l.erase a)
 
 /-- Internal implementation detail of the hash map -/
 @[inline] def filterMap (f : (a : α) → β a → Option (γ a)) :

src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean

@@ -116,14 +116,14 @@ theorem toList_replace [BEq α] {l : AssocList α β} {a : α} {b : β a} :
     (l.replace a b).toList = replaceEntry a b l.toList := by
   induction l
   · simp [replace]
-  · next k v t ih => cases h : a == k <;> simp_all [replace, List.replaceEntry_cons]
+  · next k v t ih => cases h : k == a <;> simp_all [replace, List.replaceEntry_cons]
 
 @[simp]
 theorem toList_erase [BEq α] {l : AssocList α β} {a : α} :
     (l.erase a).toList = eraseKey a l.toList := by
   induction l
   · simp [erase]
-  · next k v t ih => cases h : a == k <;> simp_all [erase, List.eraseKey_cons]
+  · next k v t ih => cases h : k == a <;> simp_all [erase, List.eraseKey_cons]
 
 theorem toList_filterMap {f : (a : α) → β a → Option (γ a)} {l : AssocList α β} :
     Perm (l.filterMap f).toList (l.toList.filterMap fun p => (f p.1 p.2).map (⟨p.1, ·⟩)) := by

src/Std/Data/DHashMap/Internal/List/Associative.lean

@@ -35,19 +35,19 @@ theorem assoc_induction {motive : List ((a : α) × β a) → Prop} (nil : motiv
 /-- Internal implementation detail of the hash map -/
 def getEntry? [BEq α] (a : α) : List ((a : α) × β a) → Option ((a : α) × β a)
   | [] => none
-  | ⟨k, v⟩ :: l => bif a == k then some ⟨k, v⟩ else getEntry? a l
+  | ⟨k, v⟩ :: l => bif k == a then some ⟨k, v⟩ else getEntry? a l
 
 @[simp] theorem getEntry?_nil [BEq α] {a : α} :
     getEntry? a ([] : List ((a : α) × β a)) = none := rfl
 theorem getEntry?_cons [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} :
-    getEntry? a (⟨k, v⟩ :: l) = bif a == k then some ⟨k, v⟩ else getEntry? a l := rfl
+    getEntry? a (⟨k, v⟩ :: l) = bif k == a then some ⟨k, v⟩ else getEntry? a l := rfl
 
-theorem getEntry?_cons_of_true [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} (h : a == k) :
+theorem getEntry?_cons_of_true [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} (h : k == a) :
     getEntry? a (⟨k, v⟩ :: l) = some ⟨k, v⟩ := by
   simp [getEntry?, h]
 
 theorem getEntry?_cons_of_false [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k}
-    (h : (a == k) = false) : getEntry? a (⟨k, v⟩ :: l) = getEntry? a l := by
+    (h : (k == a) = false) : getEntry? a (⟨k, v⟩ :: l) = getEntry? a l := by
   simp [getEntry?, h]
 
 @[simp]
@@ -56,11 +56,11 @@ theorem getEntry?_cons_self [BEq α] [ReflBEq α] {l : List ((a : α) × β a)}
   getEntry?_cons_of_true BEq.refl
 
 theorem getEntry?_eq_some [BEq α] {l : List ((a : α) × β a)} {a : α} {p : (a : α) × β a}
-    (h : getEntry? a l = some p) : a == p.1 := by
+    (h : getEntry? a l = some p) : p.1 == a := by
   induction l using assoc_induction
   · simp at h
   · next k' v' t ih =>
-    cases h' : a == k'
+    cases h' : k' == a
     · rw [getEntry?_cons_of_false h'] at h
       exact ih h
     · rw [getEntry?_cons_of_true h', Option.some.injEq] at h
@@ -72,10 +72,10 @@ theorem getEntry?_congr [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β
   induction l using assoc_induction
   · simp
   · next k v l ih =>
-    cases h' : b == k
-    · have h₂ : (a == k) = false := BEq.neq_of_beq_of_neq h h'
+    cases h' : k == a
+    · have h₂ : (k == b) = false := BEq.neq_of_neq_of_beq h' h
       rw [getEntry?_cons_of_false h', getEntry?_cons_of_false h₂, ih]
-    · rw [getEntry?_cons_of_true h', getEntry?_cons_of_true (BEq.trans h h')]
+    · rw [getEntry?_cons_of_true h', getEntry?_cons_of_true (BEq.trans h' h)]
 
 theorem isEmpty_eq_false_iff_exists_isSome_getEntry? [BEq α] [ReflBEq α] :
     {l : List ((a : α) × β a)} → l.isEmpty = false ↔ ∃ a, (getEntry? a l).isSome
@@ -89,18 +89,18 @@ variable {β : Type v}
 /-- Internal implementation detail of the hash map -/
 def getValue? [BEq α] (a : α) : List ((_ : α) × β) → Option β
   | [] => none
-  | ⟨k, v⟩ :: l => bif a == k then some v else getValue? a l
+  | ⟨k, v⟩ :: l => bif k == a then some v else getValue? a l
 
 @[simp] theorem getValue?_nil [BEq α] {a : α} : getValue? a ([] : List ((_ : α) × β)) = none := rfl
 theorem getValue?_cons [BEq α] {l : List ((_ : α) × β)} {k a : α} {v : β} :
-    getValue? a (⟨k, v⟩ :: l) = bif a == k then some v else getValue? a l := rfl
+    getValue? a (⟨k, v⟩ :: l) = bif k == a then some v else getValue? a l := rfl
 
-theorem getValue?_cons_of_true [BEq α] {l : List ((_ : α) × β)} {k a : α} {v : β} (h : a == k) :
+theorem getValue?_cons_of_true [BEq α] {l : List ((_ : α) × β)} {k a : α} {v : β} (h : k == a) :
     getValue? a (⟨k, v⟩ :: l) = some v := by
   simp [getValue?, h]
 
 theorem getValue?_cons_of_false [BEq α] {l : List ((_ : α) × β)} {k a : α} {v : β}
-    (h : (a == k) = false) : getValue? a (⟨k, v⟩ :: l) = getValue? a l := by
+    (h : (k == a) = false) : getValue? a (⟨k, v⟩ :: l) = getValue? a l := by
   simp [getValue?, h]
 
 @[simp]
@@ -113,7 +113,7 @@ theorem getValue?_eq_getEntry? [BEq α] {l : List ((_ : α) × β)} {a : α} :
   induction l using assoc_induction
   · simp
   · next k v l ih =>
-    cases h : a == k
+    cases h : k == a
     · rw [getEntry?_cons_of_false h, getValue?_cons_of_false h, ih]
     · rw [getEntry?_cons_of_true h, getValue?_cons_of_true h, Option.map_some']
 
@@ -130,22 +130,22 @@ end
 /-- Internal implementation detail of the hash map -/
 def getValueCast? [BEq α] [LawfulBEq α] (a : α) : List ((a : α) × β a) → Option (β a)
   | [] => none
-  | ⟨k, v⟩ :: l => if h : a == k then some (cast (congrArg β (eq_of_beq h).symm) v)
+  | ⟨k, v⟩ :: l => if h : k == a then some (cast (congrArg β (eq_of_beq h)) v)
       else getValueCast? a l
 
 @[simp] theorem getValueCast?_nil [BEq α] [LawfulBEq α] {a : α} :
     getValueCast? a ([] : List ((a : α) × β a)) = none := rfl
 theorem getValueCast?_cons [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} :
-    getValueCast? a (⟨k, v⟩ :: l) = if h : a == k then some (cast (congrArg β (eq_of_beq h).symm) v)
+    getValueCast? a (⟨k, v⟩ :: l) = if h : k == a then some (cast (congrArg β (eq_of_beq h)) v)
       else getValueCast? a l := rfl
 
 theorem getValueCast?_cons_of_true [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α}
-    {v : β k} (h : a == k) :
-    getValueCast? a (⟨k, v⟩ :: l) = some (cast (congrArg β (eq_of_beq h).symm) v) := by
+    {v : β k} (h : k == a) :
+    getValueCast? a (⟨k, v⟩ :: l) = some (cast (congrArg β (eq_of_beq h)) v) := by
   simp [getValueCast?, h]
 
 theorem getValueCast?_cons_of_false [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α}
-    {v : β k} (h : (a == k) = false) : getValueCast? a (⟨k, v⟩ :: l) = getValueCast? a l := by
+    {v : β k} (h : (k == a) = false) : getValueCast? a (⟨k, v⟩ :: l) = getValueCast? a l := by
   simp [getValueCast?, h]
 
 @[simp]
@@ -187,11 +187,11 @@ end
 
 theorem getValueCast?_eq_getEntry? [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α} :
     getValueCast? a l = Option.dmap (getEntry? a l)
-      (fun p h => cast (congrArg β (eq_of_beq (getEntry?_eq_some h)).symm) p.2) := by
+      (fun p h => cast (congrArg β (eq_of_beq (getEntry?_eq_some h))) p.2) := by
   induction l using assoc_induction
   · simp
   · next k v t ih =>
-    cases h : a == k
+    cases h : k == a
     · rw [getValueCast?_cons_of_false h, ih, Option.dmap_congr (getEntry?_cons_of_false h)]
     · rw [getValueCast?_cons_of_true h, Option.dmap_congr (getEntry?_cons_of_true h),
         Option.dmap_some]
@@ -207,23 +207,23 @@ theorem isEmpty_eq_false_iff_exists_isSome_getValueCast? [BEq α] [LawfulBEq α]
 /-- Internal implementation detail of the hash map -/
 def containsKey [BEq α] (a : α) : List ((a : α) × β a) → Bool
   | [] => false
-  | ⟨k, _⟩ :: l => a == k || containsKey a l
+  | ⟨k, _⟩ :: l => k == a || containsKey a l
 
 @[simp] theorem containsKey_nil [BEq α] {a : α} :
     containsKey a ([] : List ((a : α) × β a)) = false := rfl
 @[simp] theorem containsKey_cons [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} :
-    containsKey a (⟨k, v⟩ :: l) = (a == k || containsKey a l) := rfl
+    containsKey a (⟨k, v⟩ :: l) = (k == a || containsKey a l) := rfl
 
 theorem containsKey_cons_eq_false [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} :
-    (containsKey a (⟨k, v⟩ :: l) = false) ↔ ((a == k) = false) ∧ (containsKey a l = false) := by
+    (containsKey a (⟨k, v⟩ :: l) = false) ↔ ((k == a) = false) ∧ (containsKey a l = false) := by
   simp [containsKey_cons, not_or]
 
 theorem containsKey_cons_eq_true [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} :
-    (containsKey a (⟨k, v⟩ :: l)) ↔ (a == k) ∨ (containsKey a l) := by
+    (containsKey a (⟨k, v⟩ :: l)) ↔ (k == a) ∨ (containsKey a l) := by
   simp [containsKey_cons]
 
 theorem containsKey_cons_of_beq [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k}
-    (h : a == k) : containsKey a (⟨k, v⟩ :: l) := containsKey_cons_eq_true.2 <| Or.inl h
+    (h : k == a) : containsKey a (⟨k, v⟩ :: l) := containsKey_cons_eq_true.2 <| Or.inl h
 
 @[simp]
 theorem containsKey_cons_self [BEq α] [ReflBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
@@ -233,7 +233,7 @@ theorem containsKey_cons_of_containsKey [BEq α] {l : List ((a : α) × β a)} {
     (h : containsKey a l) : containsKey a (⟨k, v⟩ :: l) := containsKey_cons_eq_true.2 <| Or.inr h
 
 theorem containsKey_of_containsKey_cons [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k}
-    (h₁ : containsKey a (⟨k, v⟩ :: l)) (h₂ : (a == k) = false) : containsKey a l := by
+    (h₁ : containsKey a (⟨k, v⟩ :: l)) (h₂ : (k == a) = false) : containsKey a l := by
   rcases (containsKey_cons_eq_true.1 h₁) with (h|h)
   · exact False.elim (Bool.eq_false_iff.1 h₂ h)
   · exact h
@@ -243,7 +243,7 @@ theorem containsKey_eq_isSome_getEntry? [BEq α] {l : List ((a : α) × β a)} {
   induction l using assoc_induction
   · simp
   · next k v l ih =>
-    cases h : a == k
+    cases h : k == a
     · simp [getEntry?_cons_of_false h, h, ih]
     · simp [getEntry?_cons_of_true h, h]
 
@@ -297,7 +297,7 @@ theorem getEntry_eq_of_getEntry?_eq_some [BEq α] {l : List ((a : α) × β a)}
     (h : getEntry? a l = some ⟨k, v⟩) {h'} : getEntry a l h' = ⟨k, v⟩ := by
   simp [getEntry, h]
 
-theorem getEntry_cons_of_beq [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} (h : a == k) :
+theorem getEntry_cons_of_beq [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} (h : k == a) :
     getEntry a (⟨k, v⟩ :: l) (containsKey_cons_of_beq (v := v) h) = ⟨k, v⟩ := by
   simp [getEntry, getEntry?_cons_of_true h]
 
@@ -307,7 +307,7 @@ theorem getEntry_cons_self [BEq α] [ReflBEq α] {l : List ((a : α) × β a)} {
   getEntry_cons_of_beq BEq.refl
 
 theorem getEntry_cons_of_false [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k}
-    {h₁ : containsKey a (⟨k, v⟩ :: l)} (h₂ : (a == k) = false) : getEntry a (⟨k, v⟩ :: l) h₁ =
+    {h₁ : containsKey a (⟨k, v⟩ :: l)} (h₂ : (k == a) = false) : getEntry a (⟨k, v⟩ :: l) h₁ =
       getEntry a l (containsKey_of_containsKey_cons (v := v) h₁ h₂) := by
   simp [getEntry, getEntry?_cons_of_false h₂]
 
@@ -323,7 +323,7 @@ theorem getValue?_eq_some_getValue [BEq α] {l : List ((_ : α) × β)} {a : α}
     getValue? a l = some (getValue a l h) := by
   simp [getValue]
 
-theorem getValue_cons_of_beq [BEq α] {l : List ((_ : α) × β)} {k a : α} {v : β} (h : a == k) :
+theorem getValue_cons_of_beq [BEq α] {l : List ((_ : α) × β)} {k a : α} {v : β} (h : k == a) :
     getValue a (⟨k, v⟩ :: l) (containsKey_cons_of_beq (k := k) (v := v) h) = v := by
   simp [getValue, getValue?_cons_of_true h]
 
@@ -333,12 +333,12 @@ theorem getValue_cons_self [BEq α] [ReflBEq α] {l : List ((_ : α) × β)} {k
   getValue_cons_of_beq BEq.refl
 
 theorem getValue_cons_of_false [BEq α] {l : List ((_ : α) × β)} {k a : α} {v : β}
-    {h₁ : containsKey a (⟨k, v⟩ :: l)} (h₂ : (a == k) = false) : getValue a (⟨k, v⟩ :: l) h₁ =
+    {h₁ : containsKey a (⟨k, v⟩ :: l)} (h₂ : (k == a) = false) : getValue a (⟨k, v⟩ :: l) h₁ =
       getValue a l (containsKey_of_containsKey_cons (k := k) (v := v) h₁ h₂) := by
   simp [getValue, getValue?_cons_of_false h₂]
 
 theorem getValue_cons [BEq α] {l : List ((_ : α) × β)} {k a : α} {v : β} {h} :
-    getValue a (⟨k, v⟩ :: l) h = if h' : a == k then v
+    getValue a (⟨k, v⟩ :: l) h = if h' : k == a then v
       else getValue a l (containsKey_of_containsKey_cons (k := k) h (Bool.eq_false_iff.2 h')) := by
   rw [← Option.some_inj, ← getValue?_eq_some_getValue, getValue?_cons, apply_dite Option.some,
     cond_eq_if]
@@ -369,8 +369,8 @@ theorem Option.get_congr {o o' : Option α} {ho : o.isSome} (h : o = o') :
 theorem getValueCast_cons [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k}
     (h : containsKey a (⟨k, v⟩ :: l)) :
     getValueCast a (⟨k, v⟩ :: l) h =
-      if h' : a == k then
-        cast (congrArg β (eq_of_beq h').symm) v
+      if h' : k == a then
+        cast (congrArg β (eq_of_beq h')) v
       else
         getValueCast a l (containsKey_of_containsKey_cons (k := k) h (Bool.eq_false_iff.2 h')) := by
   rw [getValueCast, Option.get_congr getValueCast?_cons]
@@ -515,19 +515,19 @@ end
 /-- Internal implementation detail of the hash map -/
 def replaceEntry [BEq α] (k : α) (v : β k) : List ((a : α) × β a) → List ((a : α) × β a)
   | [] => []
-  | ⟨k', v'⟩ :: l => bif k == k' then ⟨k, v⟩ :: l else ⟨k', v'⟩ :: replaceEntry k v l
+  | ⟨k', v'⟩ :: l => bif k' == k then ⟨k, v⟩ :: l else ⟨k', v'⟩ :: replaceEntry k v l
 
 @[simp] theorem replaceEntry_nil [BEq α] {k : α} {v : β k} : replaceEntry k v [] = [] := rfl
 theorem replaceEntry_cons [BEq α] {l : List ((a : α) × β a)} {k k' : α} {v : β k} {v' : β k'} :
     replaceEntry k v (⟨k', v'⟩ :: l) =
-      bif k == k' then ⟨k, v⟩ :: l else ⟨k', v'⟩ :: replaceEntry k v l := rfl
+      bif k' == k then ⟨k, v⟩ :: l else ⟨k', v'⟩ :: replaceEntry k v l := rfl
 
 theorem replaceEntry_cons_of_true [BEq α] {l : List ((a : α) × β a)} {k k' : α} {v : β k}
-    {v' : β k'} (h : k == k') : replaceEntry k v (⟨k', v'⟩ :: l) = ⟨k, v⟩ :: l := by
+    {v' : β k'} (h : k' == k) : replaceEntry k v (⟨k', v'⟩ :: l) = ⟨k, v⟩ :: l := by
   simp [replaceEntry, h]
 
 theorem replaceEntry_cons_of_false [BEq α] {l : List ((a : α) × β a)} {k k' : α} {v : β k}
-    {v' : β k'} (h : (k == k') = false) :
+    {v' : β k'} (h : (k' == k) = false) :
     replaceEntry k v (⟨k', v'⟩ :: l) = ⟨k', v'⟩ :: replaceEntry k v l := by
   simp [replaceEntry, h]
 
@@ -553,37 +553,37 @@ theorem getEntry?_replaceEntry_of_containsKey_eq_false [BEq α] {l : List ((a :
   rw [replaceEntry_of_containsKey_eq_false hl]
 
 theorem getEntry?_replaceEntry_of_false [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)}
-    {a k : α} {v : β k} (h : (a == k) = false) :
+    {a k : α} {v : β k} (h : (k == a) = false) :
     getEntry? a (replaceEntry k v l) = getEntry? a l := by
   induction l using assoc_induction
   · simp
   · next k' v' l ih =>
-    cases h' : k == k'
+    cases h' : k' == k
     · rw [replaceEntry_cons_of_false h', getEntry?_cons, getEntry?_cons, ih]
     · rw [replaceEntry_cons_of_true h']
-      have hk : (a == k') = false := BEq.neq_of_neq_of_beq h h'
+      have hk : (k' == a) = false := BEq.neq_of_beq_of_neq h' h
       simp [getEntry?_cons_of_false h, getEntry?_cons_of_false hk]
 
 theorem getEntry?_replaceEntry_of_true [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)}
-    {a k : α} {v : β k} (hl : containsKey k l = true) (h : a == k) :
+    {a k : α} {v : β k} (hl : containsKey k l = true) (h : k == a) :
     getEntry? a (replaceEntry k v l) = some ⟨k, v⟩ := by
   induction l using assoc_induction
   · simp at hl
   · next k' v' l ih =>
-    cases hk'a : k == k'
+    cases hk'a : k' == k
     · rw [replaceEntry_cons_of_false hk'a]
-      have hk'k : (a == k') = false := BEq.neq_of_beq_of_neq h hk'a
+      have hk'k : (k' == a) = false := BEq.neq_of_neq_of_beq hk'a h
       rw [getEntry?_cons_of_false hk'k]
       exact ih (containsKey_of_containsKey_cons hl hk'a)
     · rw [replaceEntry_cons_of_true hk'a, getEntry?_cons_of_true h]
 
 theorem getEntry?_replaceEntry [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a k : α}
     {v : β k} :
-    getEntry? a (replaceEntry k v l) = bif containsKey k l && a == k then some ⟨k, v⟩ else
+    getEntry? a (replaceEntry k v l) = bif containsKey k l && k == a then some ⟨k, v⟩ else
       getEntry? a l := by
   cases hl : containsKey k l
   · simp [getEntry?_replaceEntry_of_containsKey_eq_false hl]
-  · cases h : a == k
+  · cases h : k == a
     · simp [getEntry?_replaceEntry_of_false h]
     · simp [getEntry?_replaceEntry_of_true hl h]
 
@@ -601,12 +601,12 @@ theorem getValue?_replaceEntry_of_containsKey_eq_false [BEq α] {l : List ((_ :
   simp [getValue?_eq_getEntry?, getEntry?_replaceEntry_of_containsKey_eq_false hl]
 
 theorem getValue?_replaceEntry_of_false [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)}
-    {k a : α} {v : β} (h : (a == k) = false) :
+    {k a : α} {v : β} (h : (k == a) = false) :
     getValue? a (replaceEntry k v l) = getValue? a l := by
   simp [getValue?_eq_getEntry?, getEntry?_replaceEntry_of_false h]
 
 theorem getValue?_replaceEntry_of_true [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)}
-    {k a : α} {v : β} (hl : containsKey k l = true) (h : a == k) :
+    {k a : α} {v : β} (hl : containsKey k l = true) (h : k == a) :
     getValue? a (replaceEntry k v l) = some v := by
   simp [getValue?_eq_getEntry?, getEntry?_replaceEntry_of_true hl h]
 
@@ -614,7 +614,7 @@ end
 
 theorem getValueCast?_replaceEntry [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a k : α}
     {v : β k} : getValueCast? a (replaceEntry k v l) =
-      if h : containsKey k l ∧ a == k then some (cast (congrArg β (eq_of_beq h.2).symm) v)
+      if h : containsKey k l ∧ k == a then some (cast (congrArg β (eq_of_beq h.2)) v)
         else getValueCast? a l := by
   rw [getValueCast?_eq_getEntry?]
   split
@@ -632,25 +632,25 @@ theorem getValueCast?_replaceEntry [BEq α] [LawfulBEq α] {l : List ((a : α)
 @[simp]
 theorem containsKey_replaceEntry [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a k : α}
     {v : β k} : containsKey a (replaceEntry k v l) = containsKey a l := by
-  cases h : containsKey k l && a == k
+  cases h : containsKey k l && k == a
   · rw [containsKey_eq_isSome_getEntry?, getEntry?_replaceEntry, h, cond_false,
       containsKey_eq_isSome_getEntry?]
   · rw [containsKey_eq_isSome_getEntry?, getEntry?_replaceEntry, h, cond_true, Option.isSome_some,
       Eq.comm]
     rw [Bool.and_eq_true] at h
-    exact containsKey_of_beq h.1 (BEq.symm h.2)
+    exact containsKey_of_beq h.1 h.2
 
 /-- Internal implementation detail of the hash map -/
 def eraseKey [BEq α] (k : α) : List ((a : α) × β a) → List ((a : α) × β a)
   | [] => []
-  | ⟨k', v'⟩ :: l => bif k == k' then l else ⟨k', v'⟩ :: eraseKey k l
+  | ⟨k', v'⟩ :: l => bif k' == k then l else ⟨k', v'⟩ :: eraseKey k l
 
 @[simp] theorem eraseKey_nil [BEq α] {k : α} : eraseKey k ([] : List ((a : α) × β a)) = [] := rfl
 theorem eraseKey_cons [BEq α] {l : List ((a : α) × β a)} {k k' : α} {v' : β k'} :
-    eraseKey k (⟨k', v'⟩ :: l) = bif k == k' then l else ⟨k', v'⟩ :: eraseKey k l := rfl
+    eraseKey k (⟨k', v'⟩ :: l) = bif k' == k then l else ⟨k', v'⟩ :: eraseKey k l := rfl
 
 theorem eraseKey_cons_of_beq [BEq α] {l : List ((a : α) × β a)} {k k' : α} {v' : β k'}
-    (h : k == k') : eraseKey k (⟨k', v'⟩ :: l) = l :=
+    (h : k' == k) : eraseKey k (⟨k', v'⟩ :: l) = l :=
   by simp [eraseKey_cons, h]
 
 @[simp]
@@ -659,7 +659,7 @@ theorem eraseKey_cons_self [BEq α] [ReflBEq α] {l : List ((a : α) × β a)} {
   eraseKey_cons_of_beq BEq.refl
 
 theorem eraseKey_cons_of_false [BEq α] {l : List ((a : α) × β a)} {k k' : α} {v' : β k'}
-    (h : (k == k') = false) : eraseKey k (⟨k', v'⟩ :: l) = ⟨k', v'⟩ :: eraseKey k l := by
+    (h : (k' == k) = false) : eraseKey k (⟨k', v'⟩ :: l) = ⟨k', v'⟩ :: eraseKey k l := by
   simp [eraseKey_cons, h]
 
 theorem eraseKey_of_containsKey_eq_false [BEq α] {l : List ((a : α) × β a)} {k : α}
@@ -676,7 +676,7 @@ theorem sublist_eraseKey [BEq α] {l : List ((a : α) × β a)} {k : α} :
   · simp
   · next k' v' t ih =>
     rw [eraseKey_cons]
-    cases k == k'
+    cases k' == k
     · simpa
     · simpa using Sublist.cons_right Sublist.refl
 
@@ -686,7 +686,7 @@ theorem length_eraseKey [BEq α] {l : List ((a : α) × β a)} {k : α} :
   · simp
   · next k' v' t ih =>
     rw [eraseKey_cons, containsKey_cons]
-    cases k == k'
+    cases k' == k
     · rw [cond_false, Bool.false_or, List.length_cons, ih]
       cases h : containsKey k t
       · simp
@@ -722,7 +722,7 @@ theorem containsKey_eq_keys_contains [BEq α] [PartialEquivBEq α] {l : List ((a
   · next k _ l ih => simp [ih, BEq.comm]
 
 theorem containsKey_eq_true_iff_exists_mem [BEq α] {l : List ((a : α) × β a)} {a : α} :
-    containsKey a l = true ↔ ∃ p ∈ l, a == p.1 := by
+    containsKey a l = true ↔ ∃ p ∈ l, p.1 == a := by
   induction l using assoc_induction <;> simp_all
 
 theorem containsKey_of_mem [BEq α] [ReflBEq α] {l : List ((a : α) × β a)} {p : (a : α) × β a}
@@ -798,11 +798,11 @@ theorem mem_iff_getEntry?_eq_some [BEq α] [EquivBEq α] {l : List ((a : α) ×
     refine ⟨?_, ?_⟩
     · rintro (rfl|hk)
       · simp
-      · suffices (p.fst == k) = false by simp_all
+      · suffices (k == p.fst) = false by simp_all
         refine Bool.eq_false_iff.2 fun hcon => Bool.false_ne_true ?_
-        rw [← h.containsKey_eq_false, containsKey_congr (BEq.symm hcon),
+        rw [← h.containsKey_eq_false, containsKey_congr hcon,
           containsKey_eq_isSome_getEntry?, hk, Option.isSome_some]
-    · cases p.fst == k
+    · cases k == p.fst
       · rw [cond_false]
         exact Or.inr
       · rw [cond_true, Option.some.injEq]
@@ -814,7 +814,7 @@ theorem DistinctKeys.replaceEntry [BEq α] [PartialEquivBEq α] {l : List ((a :
   · simp
   · next k' v' l ih =>
     rw [distinctKeys_cons_iff] at h
-    cases hk'k : k == k'
+    cases hk'k : k' == k
     · rw [replaceEntry_cons_of_false hk'k, distinctKeys_cons_iff]
       refine ⟨ih h.1, ?_⟩
       simpa using h.2
@@ -870,7 +870,7 @@ section
 variable {β : Type v}
 
 theorem getValue?_insertEntry_of_beq [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α}
-    {v : β} (h : a == k) : getValue? a (insertEntry k v l) = some v := by
+    {v : β} (h : k == a) : getValue? a (insertEntry k v l) = some v := by
   cases h' : containsKey k l
   · rw [insertEntry_of_containsKey_eq_false h', getValue?_cons_of_true h]
   · rw [insertEntry_of_containsKey h', getValue?_replaceEntry_of_true h' h]
@@ -880,14 +880,14 @@ theorem getValue?_insertEntry_of_self [BEq α] [EquivBEq α] {l : List ((_ : α)
   getValue?_insertEntry_of_beq BEq.refl
 
 theorem getValue?_insertEntry_of_false [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)}
-    {k a : α} {v : β} (h : (a == k) = false) : getValue? a (insertEntry k v l) = getValue? a l := by
+    {k a : α} {v : β} (h : (k == a) = false) : getValue? a (insertEntry k v l) = getValue? a l := by
   cases h' : containsKey k l
   · rw [insertEntry_of_containsKey_eq_false h', getValue?_cons_of_false h]
   · rw [insertEntry_of_containsKey h', getValue?_replaceEntry_of_false h]
 
 theorem getValue?_insertEntry [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α}
-    {v : β} : getValue? a (insertEntry k v l) = bif a == k then some v else getValue? a l := by
-  cases h : a == k
+    {v : β} : getValue? a (insertEntry k v l) = bif k == a then some v else getValue? a l := by
+  cases h : k == a
   · simp [getValue?_insertEntry_of_false h, h]
   · simp [getValue?_insertEntry_of_beq h, h]
 
@@ -899,14 +899,14 @@ end
 
 theorem getEntry?_insertEntry [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α}
     {v : β k} :
-    getEntry? a (insertEntry k v l) = bif a == k then some ⟨k, v⟩ else getEntry? a l := by
+    getEntry? a (insertEntry k v l) = bif k == a then some ⟨k, v⟩ else getEntry? a l := by
   cases hl : containsKey k l
   · rw [insertEntry_of_containsKey_eq_false hl, getEntry?_cons]
   · rw [insertEntry_of_containsKey hl, getEntry?_replaceEntry, hl, Bool.true_and, BEq.comm]
 
 theorem getValueCast?_insertEntry [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α}
     {v : β k} : getValueCast? a (insertEntry k v l) =
-      if h : a == k then some (cast (congrArg β (eq_of_beq h).symm) v) else getValueCast? a l := by
+      if h : k == a then some (cast (congrArg β (eq_of_beq h)) v) else getValueCast? a l := by
   cases hl : containsKey k l
   · rw [insertEntry_of_containsKey_eq_false hl, getValueCast?_cons]
   · rw [insertEntry_of_containsKey hl, getValueCast?_replaceEntry, hl]
@@ -918,7 +918,7 @@ theorem getValueCast?_insertEntry_self [BEq α] [LawfulBEq α] {l : List ((a :
 
 theorem getValueCast!_insertEntry [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α}
     [Inhabited (β a)] {v : β k} : getValueCast! a (insertEntry k v l) =
-      if h : a == k then cast (congrArg β (eq_of_beq h).symm) v else getValueCast! a l := by
+      if h : k == a then cast (congrArg β (eq_of_beq h)) v else getValueCast! a l := by
   simp [getValueCast!_eq_getValueCast?, getValueCast?_insertEntry, apply_dite Option.get!]
 
 theorem getValueCast!_insertEntry_self [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α}
@@ -927,7 +927,7 @@ theorem getValueCast!_insertEntry_self [BEq α] [LawfulBEq α] {l : List ((a :
 
 theorem getValueCastD_insertEntry [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α}
     {fallback : β a} {v : β k} : getValueCastD a (insertEntry k v l) fallback =
-      if h : a == k then cast (congrArg β (eq_of_beq h).symm) v
+      if h : k == a then cast (congrArg β (eq_of_beq h)) v
       else getValueCastD a l fallback := by
   simp [getValueCastD_eq_getValueCast?, getValueCast?_insertEntry,
     apply_dite (fun x => Option.getD x fallback)]
@@ -938,7 +938,7 @@ theorem getValueCastD_insertEntry_self [BEq α] [LawfulBEq α] {l : List ((a :
 
 theorem getValue!_insertEntry {β : Type v} [BEq α] [PartialEquivBEq α] [Inhabited β]
     {l : List ((_ : α) × β)} {k a : α} {v : β} :
-    getValue! a (insertEntry k v l) = bif a == k then v else getValue! a l := by
+    getValue! a (insertEntry k v l) = bif k == a then v else getValue! a l := by
   simp [getValue!_eq_getValue?, getValue?_insertEntry, Bool.apply_cond Option.get!]
 
 theorem getValue!_insertEntry_self {β : Type v} [BEq α] [EquivBEq α] [Inhabited β]
@@ -947,7 +947,7 @@ theorem getValue!_insertEntry_self {β : Type v} [BEq α] [EquivBEq α] [Inhabit
 
 theorem getValueD_insertEntry {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)}
     {k a : α} {fallback v : β} : getValueD a (insertEntry k v l) fallback =
-      bif a == k then v else getValueD a l fallback := by
+      bif k == a then v else getValueD a l fallback := by
   simp [getValueD_eq_getValue?, getValue?_insertEntry, Bool.apply_cond (fun x => Option.getD x fallback)]
 
 theorem getValueD_insertEntry_self {β : Type v} [BEq α] [EquivBEq α] {l : List ((_ : α) × β)}
@@ -956,12 +956,12 @@ theorem getValueD_insertEntry_self {β : Type v} [BEq α] [EquivBEq α] {l : Lis
 
 @[simp]
 theorem containsKey_insertEntry [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α}
-    {v : β k} : containsKey a (insertEntry k v l) = ((a == k) || containsKey a l) := by
+    {v : β k} : containsKey a (insertEntry k v l) = ((k == a) || containsKey a l) := by
   rw [containsKey_eq_isSome_getEntry?, containsKey_eq_isSome_getEntry?, getEntry?_insertEntry]
-  cases a == k <;> simp
+  cases k == a <;> simp
 
 theorem containsKey_insertEntry_of_beq [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)}
-    {k a : α} {v : β k} (h : a == k) : containsKey a (insertEntry k v l) := by
+    {k a : α} {v : β k} (h : k == a) : containsKey a (insertEntry k v l) := by
   simp [h]
 
 @[simp]
@@ -971,12 +971,12 @@ theorem containsKey_insertEntry_self [BEq α] [EquivBEq α] {l : List ((a : α)
 
 theorem containsKey_of_containsKey_insertEntry [BEq α] [PartialEquivBEq α]
     {l : List ((a : α) × β a)} {k a : α} {v : β k} (h₁ : containsKey a (insertEntry k v l))
-    (h₂ : (a == k) = false) : containsKey a l := by
+    (h₂ : (k == a) = false) : containsKey a l := by
   rwa [containsKey_insertEntry, h₂, Bool.false_or] at h₁
 
 theorem getValueCast_insertEntry [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α}
     {v : β k} {h} : getValueCast a (insertEntry k v l) h =
-    if h' : a == k then cast (congrArg β (eq_of_beq h').symm) v
+    if h' : k == a then cast (congrArg β (eq_of_beq h')) v
     else getValueCast a l (containsKey_of_containsKey_insertEntry h (Bool.eq_false_iff.2 h')) := by
   rw [← Option.some_inj, ← getValueCast?_eq_some_getValueCast, apply_dite Option.some,
     getValueCast?_insertEntry]
@@ -988,7 +988,7 @@ theorem getValueCast_insertEntry_self [BEq α] [LawfulBEq α] {l : List ((a : α
 
 theorem getValue_insertEntry {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)}
     {k a : α} {v : β} {h} : getValue a (insertEntry k v l) h =
-      if h' : a == k then v
+      if h' : k == a then v
       else getValue a l (containsKey_of_containsKey_insertEntry h (Bool.eq_false_iff.2 h')) := by
   rw [← Option.some_inj, ← getValue?_eq_some_getValue, apply_dite Option.some,
     getValue?_insertEntry, cond_eq_if, ← dite_eq_ite]
@@ -1020,14 +1020,14 @@ theorem isEmpty_insertEntryIfNew [BEq α] {l : List ((a : α) × β a)} {k : α}
 
 theorem getEntry?_insertEntryIfNew [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α}
     {v : β k} : getEntry? a (insertEntryIfNew k v l) =
-      bif a == k && !containsKey k l then some ⟨k, v⟩ else getEntry? a l := by
+      bif k == a && !containsKey k l then some ⟨k, v⟩ else getEntry? a l := by
   cases h : containsKey k l
   · simp [insertEntryIfNew_of_containsKey_eq_false h, getEntry?_cons]
   · simp [insertEntryIfNew_of_containsKey h]
 
 theorem getValueCast?_insertEntryIfNew [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α}
     {v : β k} : getValueCast? a (insertEntryIfNew k v l) =
-      if h : a == k ∧ containsKey k l = false then some (cast (congrArg β (eq_of_beq h.1).symm) v)
+      if h : k == a ∧ containsKey k l = false then some (cast (congrArg β (eq_of_beq h.1)) v)
       else getValueCast? a l := by
   cases h : containsKey k l
   · rw [insertEntryIfNew_of_containsKey_eq_false h, getValueCast?_cons]
@@ -1036,16 +1036,16 @@ theorem getValueCast?_insertEntryIfNew [BEq α] [LawfulBEq α] {l : List ((a :
 
 theorem getValue?_insertEntryIfNew {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)}
     {k a : α} {v : β} : getValue? a (insertEntryIfNew k v l) =
-      bif a == k && !containsKey k l then some v else getValue? a l := by
+      bif k == a && !containsKey k l then some v else getValue? a l := by
   simp [getValue?_eq_getEntry?, getEntry?_insertEntryIfNew,
       Bool.apply_cond (Option.map (fun (y : ((_ : α) × β)) => y.2))]
 
 theorem containsKey_insertEntryIfNew [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)}
     {k a : α} {v : β k} :
-    containsKey a (insertEntryIfNew k v l) = ((a == k) || containsKey a l) := by
+    containsKey a (insertEntryIfNew k v l) = ((k == a) || containsKey a l) := by
   simp only [containsKey_eq_isSome_getEntry?, getEntry?_insertEntryIfNew, Bool.apply_cond Option.isSome,
     Option.isSome_some, Bool.cond_true_left]
-  cases h : a == k
+  cases h : k == a
   · simp
   · rw [Bool.true_and, Bool.true_or, getEntry?_congr h, Bool.not_or_self]
 
@@ -1055,7 +1055,7 @@ theorem containsKey_insertEntryIfNew_self [BEq α] [EquivBEq α] {l : List ((a :
 
 theorem containsKey_of_containsKey_insertEntryIfNew [BEq α] [PartialEquivBEq α]
     {l : List ((a : α) × β a)} {k a : α} {v : β k} (h₁ : containsKey a (insertEntryIfNew k v l))
-    (h₂ : (a == k) = false) : containsKey a l := by
+    (h₂ : (k == a) = false) : containsKey a l := by
   rwa [containsKey_insertEntryIfNew, h₂, Bool.false_or] at h₁
 
 /--
@@ -1064,7 +1064,7 @@ obligation in the statement of `getValueCast_insertEntryIfNew`.
 -/
 theorem containsKey_of_containsKey_insertEntryIfNew' [BEq α] [PartialEquivBEq α]
     {l : List ((a : α) × β a)} {k a : α} {v : β k} (h₁ : containsKey a (insertEntryIfNew k v l))
-    (h₂ : ¬((a == k) ∧ containsKey k l = false)) : containsKey a l := by
+    (h₂ : ¬((k == a) ∧ containsKey k l = false)) : containsKey a l := by
   rw [Decidable.not_and_iff_or_not, Bool.not_eq_true, Bool.not_eq_false] at h₂
   rcases h₂ with h₂|h₂
   · rwa [containsKey_insertEntryIfNew, h₂, Bool.false_or] at h₁
@@ -1072,8 +1072,8 @@ theorem containsKey_of_containsKey_insertEntryIfNew' [BEq α] [PartialEquivBEq
 
 theorem getValueCast_insertEntryIfNew [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α}
     {v : β k} {h} : getValueCast a (insertEntryIfNew k v l) h =
-    if h' : a == k ∧ containsKey k l = false then
-      cast (congrArg β (eq_of_beq h'.1).symm) v
+    if h' : k == a ∧ containsKey k l = false then
+      cast (congrArg β (eq_of_beq h'.1)) v
     else
       getValueCast a l (containsKey_of_containsKey_insertEntryIfNew' h h') := by
   rw [← Option.some_inj, ← getValueCast?_eq_some_getValueCast, apply_dite Option.some,
@@ -1082,7 +1082,7 @@ theorem getValueCast_insertEntryIfNew [BEq α] [LawfulBEq α] {l : List ((a : α
 
 theorem getValue_insertEntryIfNew {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)}
     {k a : α} {v : β} {h} : getValue a (insertEntryIfNew k v l) h =
-    if h' : a == k ∧ containsKey k l = false then v
+    if h' : k == a ∧ containsKey k l = false then v
     else getValue a l (containsKey_of_containsKey_insertEntryIfNew' h h') := by
   rw [← Option.some_inj, ← getValue?_eq_some_getValue, apply_dite Option.some,
     getValue?_insertEntryIfNew, cond_eq_if, ← dite_eq_ite]
@@ -1090,25 +1090,25 @@ theorem getValue_insertEntryIfNew {β : Type v} [BEq α] [PartialEquivBEq α] {l
 
 theorem getValueCast!_insertEntryIfNew [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α}
     {v : β k} [Inhabited (β a)] : getValueCast! a (insertEntryIfNew k v l) =
-      if h : a == k ∧ containsKey k l = false then cast (congrArg β (eq_of_beq h.1).symm) v
+      if h : k == a ∧ containsKey k l = false then cast (congrArg β (eq_of_beq h.1)) v
       else getValueCast! a l := by
   simp [getValueCast!_eq_getValueCast?, getValueCast?_insertEntryIfNew, apply_dite Option.get!]
 
 theorem getValue!_insertEntryIfNew {β : Type v} [BEq α] [PartialEquivBEq α] [Inhabited β]
     {l : List ((_ : α) × β)} {k a : α} {v : β} : getValue! a (insertEntryIfNew k v l) =
-      bif a == k && !containsKey k l then v else getValue! a l := by
+      bif k == a && !containsKey k l then v else getValue! a l := by
   simp [getValue!_eq_getValue?, getValue?_insertEntryIfNew, Bool.apply_cond Option.get!]
 
 theorem getValueCastD_insertEntryIfNew [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α}
     {v : β k} {fallback : β a} : getValueCastD a (insertEntryIfNew k v l) fallback =
-      if h : a == k ∧ containsKey k l = false then cast (congrArg β (eq_of_beq h.1).symm) v
+      if h : k == a ∧ containsKey k l = false then cast (congrArg β (eq_of_beq h.1)) v
       else getValueCastD a l fallback := by
   simp [getValueCastD_eq_getValueCast?, getValueCast?_insertEntryIfNew,
     apply_dite (fun x => Option.getD x fallback)]
 
 theorem getValueD_insertEntryIfNew {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)}
     {k a : α} {fallback v : β} : getValueD a (insertEntryIfNew k v l) fallback =
-      bif a == k && !containsKey k l then v else getValueD a l fallback := by
+      bif k == a && !containsKey k l then v else getValueD a l fallback := by
   simp [getValueD_eq_getValue?, getValue?_insertEntryIfNew,
     Bool.apply_cond (fun x => Option.getD x fallback)]
 
@@ -1131,7 +1131,7 @@ theorem keys_eraseKey [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)
   · next k' v' l ih =>
     simp only [eraseKey_cons, keys_cons, List.erase_cons]
     rw [BEq.comm]
-    cases k' == k <;> simp [ih]
+    cases k == k' <;> simp [ih]
 
 theorem DistinctKeys.eraseKey [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α} :
     DistinctKeys l → DistinctKeys (eraseKey k l) := by
@@ -1142,35 +1142,35 @@ theorem getEntry?_eraseKey_self [BEq α] [PartialEquivBEq α] {l : List ((a : α
   induction l using assoc_induction
   · simp
   · next k' v' t ih =>
-    cases h' : k == k'
+    cases h' : k' == k
     · rw [eraseKey_cons_of_false h', getEntry?_cons_of_false h']
       exact ih h.tail
     · rw [eraseKey_cons_of_beq h', ← Option.not_isSome_iff_eq_none, Bool.not_eq_true,
-        ← containsKey_eq_isSome_getEntry?, ← containsKey_congr (BEq.symm h')]
+        ← containsKey_eq_isSome_getEntry?, ← containsKey_congr h']
       exact h.containsKey_eq_false
 
 theorem getEntry?_eraseKey_of_beq [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α}
-    (hl : DistinctKeys l) (hka : a == k) : getEntry? a (eraseKey k l) = none := by
-  rw [← getEntry?_congr (BEq.symm hka), getEntry?_eraseKey_self hl]
+    (hl : DistinctKeys l) (hka : k == a) : getEntry? a (eraseKey k l) = none := by
+  rw [← getEntry?_congr hka, getEntry?_eraseKey_self hl]
 
 theorem getEntry?_eraseKey_of_false [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)}
-    {k a : α} (hka : (a == k) = false) : getEntry? a (eraseKey k l) = getEntry? a l := by
+    {k a : α} (hka : (k == a) = false) : getEntry? a (eraseKey k l) = getEntry? a l := by
   induction l using assoc_induction
   · simp
   · next k' v' t ih =>
-    cases h' : k == k'
+    cases h' : k' == k
     · rw [eraseKey_cons_of_false h']
-      cases h'' : a == k'
+      cases h'' : k' == a
       · rw [getEntry?_cons_of_false h'', ih, getEntry?_cons_of_false h'']
       · rw [getEntry?_cons_of_true h'', getEntry?_cons_of_true h'']
     · rw [eraseKey_cons_of_beq h']
-      have hx : (a == k') = false := BEq.neq_of_neq_of_beq hka h'
+      have hx : (k' == a) = false := BEq.neq_of_beq_of_neq h' hka
       rw [getEntry?_cons_of_false hx]
 
 theorem getEntry?_eraseKey [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α}
     (hl : DistinctKeys l) :
-    getEntry? a (eraseKey k l) = bif a == k then none else getEntry? a l := by
-  cases h : a == k
+    getEntry? a (eraseKey k l) = bif k == a then none else getEntry? a l := by
+  cases h : k == a
   · simp [getEntry?_eraseKey_of_false h, h]
   · simp [getEntry?_eraseKey_of_beq hl h, h]
 
@@ -1213,16 +1213,16 @@ theorem getValue?_eraseKey_self [BEq α] [PartialEquivBEq α] {l : List ((_ : α
   simp [getValue?_eq_getEntry?, getEntry?_eraseKey_self h]
 
 theorem getValue?_eraseKey_of_beq [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α}
-    (hl : DistinctKeys l) (hka : a == k) : getValue? a (eraseKey k l) = none := by
+    (hl : DistinctKeys l) (hka : k == a) : getValue? a (eraseKey k l) = none := by
   simp [getValue?_eq_getEntry?, getEntry?_eraseKey_of_beq hl hka]
 
 theorem getValue?_eraseKey_of_false [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α}
-    (hka : (a == k) = false) : getValue? a (eraseKey k l) = getValue? a l := by
+    (hka : (k == a) = false) : getValue? a (eraseKey k l) = getValue? a l := by
   simp [getValue?_eq_getEntry?, getEntry?_eraseKey_of_false hka]
 
 theorem getValue?_eraseKey [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α}
     (hl : DistinctKeys l) :
-    getValue? a (eraseKey k l) = bif a == k then none else getValue? a l := by
+    getValue? a (eraseKey k l) = bif k == a then none else getValue? a l := by
   simp [getValue?_eq_getEntry?, getEntry?_eraseKey hl, Bool.apply_cond (Option.map _)]
 
 end
@@ -1236,18 +1236,18 @@ theorem containsKey_eraseKey_of_beq [BEq α] [PartialEquivBEq α] {l : List ((a
   rw [containsKey_congr hka, containsKey_eraseKey_self hl]
 
 theorem containsKey_eraseKey_of_false [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)}
-    {k a : α} (hka : (a == k) = false) : containsKey a (eraseKey k l) = containsKey a l := by
+    {k a : α} (hka : (k == a) = false) : containsKey a (eraseKey k l) = containsKey a l := by
   simp [containsKey_eq_isSome_getEntry?, getEntry?_eraseKey_of_false hka]
 
 theorem containsKey_eraseKey [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α}
-    (hl : DistinctKeys l) : containsKey a (eraseKey k l) = (!(a == k) && containsKey a l) := by
+    (hl : DistinctKeys l) : containsKey a (eraseKey k l) = (!(k == a) && containsKey a l) := by
   simp [containsKey_eq_isSome_getEntry?, getEntry?_eraseKey hl, Bool.apply_cond]
 
 theorem getValueCast?_eraseKey [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α}
     (hl : DistinctKeys l) :
-    getValueCast? a (eraseKey k l) = bif a == k then none else getValueCast? a l := by
+    getValueCast? a (eraseKey k l) = bif k == a then none else getValueCast? a l := by
   rw [getValueCast?_eq_getEntry?, Option.dmap_congr (getEntry?_eraseKey hl)]
-  rcases Bool.eq_false_or_eq_true (a == k) with h|h
+  rcases Bool.eq_false_or_eq_true (k == a) with h|h
   · rw [Option.dmap_congr (Bool.cond_pos h), Option.dmap_none, Bool.cond_pos h]
   · rw [Option.dmap_congr (Bool.cond_neg h), getValueCast?_eq_getEntry?]
     exact (Bool.cond_neg h).symm
@@ -1258,7 +1258,7 @@ theorem getValueCast?_eraseKey_self [BEq α] [LawfulBEq α] {l : List ((a : α)
 
 theorem getValueCast!_eraseKey [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α}
     [Inhabited (β a)] (hl : DistinctKeys l) :
-    getValueCast! a (eraseKey k l) = bif a == k then default else getValueCast! a l := by
+    getValueCast! a (eraseKey k l) = bif k == a then default else getValueCast! a l := by
   simp [getValueCast!_eq_getValueCast?, getValueCast?_eraseKey hl, Bool.apply_cond Option.get!]
 
 theorem getValueCast!_eraseKey_self [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α}
@@ -1267,7 +1267,7 @@ theorem getValueCast!_eraseKey_self [BEq α] [LawfulBEq α] {l : List ((a : α)
 
 theorem getValueCastD_eraseKey [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α}
     {fallback : β a} (hl : DistinctKeys l) : getValueCastD a (eraseKey k l) fallback =
-      bif a == k then fallback else getValueCastD a l fallback := by
+      bif k == a then fallback else getValueCastD a l fallback := by
   simp [getValueCastD_eq_getValueCast?, getValueCast?_eraseKey hl,
     Bool.apply_cond (fun x => Option.getD x fallback)]
 
@@ -1278,7 +1278,7 @@ theorem getValueCastD_eraseKey_self [BEq α] [LawfulBEq α] {l : List ((a : α)
 
 theorem getValue!_eraseKey {β : Type v} [BEq α] [PartialEquivBEq α] [Inhabited β]
     {l : List ((_ : α) × β)} {k a : α} (hl : DistinctKeys l) :
-    getValue! a (eraseKey k l) = bif a == k then default else getValue! a l := by
+    getValue! a (eraseKey k l) = bif k == a then default else getValue! a l := by
   simp [getValue!_eq_getValue?, getValue?_eraseKey hl, Bool.apply_cond Option.get!]
 
 theorem getValue!_eraseKey_self {β : Type v} [BEq α] [PartialEquivBEq α] [Inhabited β]
@@ -1288,7 +1288,7 @@ theorem getValue!_eraseKey_self {β : Type v} [BEq α] [PartialEquivBEq α] [Inh
 
 theorem getValueD_eraseKey {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)}
     {k a : α} {fallback : β} (hl : DistinctKeys l) : getValueD a (eraseKey k l) fallback =
-      bif a == k then fallback else getValueD a l fallback := by
+      bif k == a then fallback else getValueD a l fallback := by
   simp [getValueD_eq_getValue?, getValue?_eraseKey hl, Bool.apply_cond (fun x => Option.getD x fallback)]
 
 theorem getValueD_eraseKey_self {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)}
@@ -1325,9 +1325,9 @@ theorem getEntry?_of_perm [BEq α] [PartialEquivBEq α] {l l' : List ((a : α)
     rcases p with ⟨k₁, v₁⟩
     rcases p' with ⟨k₂, v₂⟩
     simp only [getEntry?_cons]
-    cases h₂ : a == k₂ <;> cases h₁ : a == k₁ <;> try simp; done
+    cases h₂ : k₂ == a <;> cases h₁ : k₁ == a <;> try simp; done
     simp only [distinctKeys_cons_iff, containsKey_cons, Bool.or_eq_false_iff] at hl
-    exact ((Bool.eq_false_iff.1 hl.2.1).elim (BEq.trans (BEq.symm h₁) h₂)).elim
+    exact ((Bool.eq_false_iff.1 hl.2.1).elim (BEq.trans h₂ (BEq.symm h₁))).elim
   · next l₁ l₂ l₃ hl₁₂ _ ih₁ ih₂ => exact (ih₁ hl).trans (ih₂ (hl.perm (hl₁₂.symm)))
 
 theorem containsKey_of_perm [BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)} {k : α}
@@ -1392,7 +1392,7 @@ theorem perm_cons_getEntry [BEq α] {l : List ((a : α) × β a)} {a : α} (h :
   · simp at h
   · next k' v' t ih =>
     simp only [containsKey_cons, Bool.or_eq_true] at h
-    cases hk : a == k'
+    cases hk : k' == a
     · obtain ⟨l', hl'⟩ := ih (h.resolve_left (Bool.not_eq_true _ ▸ hk))
       rw [getEntry_cons_of_false hk]
       exact ⟨⟨k', v'⟩ :: l', (hl'.cons _).trans (Perm.swap _ _ (Perm.refl _))⟩
@@ -1414,9 +1414,9 @@ theorem getEntry?_ext [BEq α] [EquivBEq α] {l l' : List ((a : α) × β a)} (h
     suffices Perm t l'' from (this.cons _).trans hl''.symm
     apply ih hl.tail (hl'.perm hl''.symm).tail
     intro k'
-    cases hk' : k' == k
+    cases hk' : k == k'
     · simpa only [getEntry?_of_perm hl' hl'', getEntry?_cons_of_false hk'] using h k'
-    · rw [getEntry?_congr hk', getEntry?_congr hk', getEntry?_eq_none.2 hl.containsKey_eq_false,
+    · rw [← getEntry?_congr hk', ← getEntry?_congr hk', getEntry?_eq_none.2 hl.containsKey_eq_false,
           getEntry?_eq_none.2 (hl'.perm hl''.symm).containsKey_eq_false]
 
 theorem replaceEntry_of_perm [BEq α] [EquivBEq α] {l l' : List ((a : α) × β a)} {k : α} {v : β k}
@@ -1439,7 +1439,7 @@ theorem getEntry?_append [BEq α] {l l' : List ((a : α) × β a)} {a : α} :
     getEntry? a (l ++ l') = (getEntry? a l).or (getEntry? a l') := by
   induction l using assoc_induction
   · simp
-  · next k' v' t ih => cases h : a == k' <;> simp_all [getEntry?_cons]
+  · next k' v' t ih => cases h : k' == a <;> simp_all [getEntry?_cons]
 
 theorem getEntry?_append_of_containsKey_eq_false [BEq α] {l l' : List ((a : α) × β a)} {a : α}
     (h : containsKey a l' = false) : getEntry? a (l ++ l') = getEntry? a l := by
@@ -1501,7 +1501,7 @@ theorem replaceEntry_append_of_containsKey_left [BEq α] {l l' : List ((a : α)
   · simp at h
   · next k' v' t ih =>
     simp only [containsKey_cons, Bool.or_eq_true] at h
-    cases h' : k == k'
+    cases h' : k' == k
     · simpa [replaceEntry_cons, h'] using ih (h.resolve_left (Bool.not_eq_true _ ▸ h'))
     · simp [replaceEntry_cons, h']
 
@@ -1535,7 +1535,7 @@ theorem eraseKey_append_of_containsKey_right_eq_false [BEq α] {l l' : List ((a
   · simp [eraseKey_of_containsKey_eq_false h]
   · next k' v' t ih =>
     rw [List.cons_append, eraseKey_cons, eraseKey_cons]
-    cases k == k'
+    cases k' == k
     · rw [cond_false, cond_false, ih, List.cons_append]
     · rw [cond_true, cond_true]
 

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

@@ -241,7 +241,7 @@ theorem updateAllBuckets [BEq α] [Hashable α] [LawfulHashable α] {m : Array (
   simp only [Array.getElem_map, Array.size_map]
   refine ⟨fun h p hp => ?_⟩
   rcases containsKey_eq_true_iff_exists_mem.1 (hf _ _ hp) with ⟨q, hq₁, hq₂⟩
-  rw [hash_eq hq₂, (hm.hashes_to _ _).hash_self _ _ hq₁]
+  rw [← hash_eq hq₂, (hm.hashes_to _ _).hash_self _ _ hq₁]
 
 end IsHashSelf
 

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

@@ -127,11 +127,11 @@ theorem isEmpty_eq_false_iff_exists_contains_eq_true [EquivBEq α] [LawfulHashab
   simp_to_model using List.isEmpty_eq_false_iff_exists_containsKey
 
 theorem contains_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
-    (m.insert k v).contains a = ((a == k) || m.contains a) := by
+    (m.insert k v).contains a = ((k == a) || m.contains a) := by
   simp_to_model using List.containsKey_insertEntry
 
 theorem contains_of_contains_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
-    (m.insert k v).contains a → (a == k) = false → m.contains a := by
+    (m.insert k v).contains a → (k == a) = false → m.contains a := by
   simp_to_model using List.containsKey_of_containsKey_insertEntry
 
 theorem contains_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
@@ -161,7 +161,7 @@ theorem isEmpty_erase [EquivBEq α] [LawfulHashable α] {k : α} :
   simp_to_model using List.isEmpty_eraseKey
 
 theorem contains_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
-    (m.erase k).contains a = (!(a == k) && m.contains a) := by
+    (m.erase k).contains a = (!(k == a) && m.contains a) := by
   simp_to_model using List.containsKey_eraseKey
 
 theorem contains_of_contains_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
@@ -202,7 +202,7 @@ theorem get?_of_isEmpty [LawfulBEq α] {a : α} : m.1.isEmpty = true → m.get?
   simp_to_model; empty
 
 theorem get?_insert [LawfulBEq α] {a k : α} {v : β k} : (m.insert k v).get? a =
-    if h : a == k then some (cast (congrArg β (eq_of_beq h).symm) v) else m.get? a := by
+    if h : k == a then some (cast (congrArg β (eq_of_beq h)) v) else m.get? a := by
   simp_to_model using List.getValueCast?_insertEntry
 
 theorem get?_insert_self [LawfulBEq α] {k : α} {v : β k} : (m.insert k v).get? k = some v := by
@@ -215,7 +215,7 @@ theorem get?_eq_none [LawfulBEq α] {a : α} : m.contains a = false → m.get? a
   simp_to_model using List.getValueCast?_eq_none
 
 theorem get?_erase [LawfulBEq α] {k a : α} :
-    (m.erase k).get? a = bif a == k then none else m.get? a := by
+    (m.erase k).get? a = bif k == a then none else m.get? a := by
   simp_to_model using List.getValueCast?_eraseKey
 
 theorem get?_erase_self [LawfulBEq α] {k : α} : (m.erase k).get? k = none := by
@@ -234,7 +234,7 @@ theorem get?_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
   simp_to_model; empty
 
 theorem get?_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
-    get? (m.insert k v) a = bif a == k then some v else get? m a := by
+    get? (m.insert k v) a = bif k == a then some v else get? m a := by
   simp_to_model using List.getValue?_insertEntry
 
 theorem get?_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
@@ -250,7 +250,7 @@ theorem get?_eq_none [EquivBEq α] [LawfulHashable α] {a : α} :
   simp_to_model using List.getValue?_eq_none.2
 
 theorem get?_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
-    Const.get? (m.erase k) a = bif a == k then none else get? m a := by
+    Const.get? (m.erase k) a = bif k == a then none else get? m a := by
   simp_to_model using List.getValue?_eraseKey
 
 theorem get?_erase_self [EquivBEq α] [LawfulHashable α] {k : α} :
@@ -268,8 +268,8 @@ end Const
 
 theorem get_insert [LawfulBEq α] {k a : α} {v : β k} {h₁} :
     (m.insert k v).get a h₁ =
-      if h₂ : a == k then
-        cast (congrArg β (eq_of_beq h₂).symm) v
+      if h₂ : k == a then
+        cast (congrArg β (eq_of_beq h₂)) v
       else
         m.get a (contains_of_contains_insert _ h h₁ (Bool.eq_false_iff.2 h₂)) := by
   simp_to_model using List.getValueCast_insertEntry
@@ -292,7 +292,7 @@ variable {β : Type v} (m : Raw₀ α (fun _ => β)) (h : m.1.WF)
 
 theorem get_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁} :
     get (m.insert k v) a h₁ =
-      if h₂ : a == k then v
+      if h₂ : k == a then v
       else get m a (contains_of_contains_insert _ h h₁ (Bool.eq_false_iff.2 h₂)) := by
   simp_to_model using List.getValue_insertEntry
 
@@ -328,7 +328,7 @@ theorem get!_of_isEmpty [LawfulBEq α] {a : α} [Inhabited (β a)] :
 
 theorem get!_insert [LawfulBEq α] {k a : α} [Inhabited (β a)] {v : β k} :
     (m.insert k v).get! a =
-      if h : a == k then cast (congrArg β (eq_of_beq h).symm) v else m.get! a := by
+      if h : k == a then cast (congrArg β (eq_of_beq h)) v else m.get! a := by
   simp_to_model using List.getValueCast!_insertEntry
 
 theorem get!_insert_self [LawfulBEq α] {a : α} [Inhabited (β a)] {b : β a} :
@@ -340,7 +340,7 @@ theorem get!_eq_default [LawfulBEq α] {a : α} [Inhabited (β a)] :
   simp_to_model using List.getValueCast!_eq_default
 
 theorem get!_erase [LawfulBEq α] {k a : α} [Inhabited (β a)] :
-    (m.erase k).get! a = bif a == k then default else m.get! a := by
+    (m.erase k).get! a = bif k == a then default else m.get! a := by
   simp_to_model using List.getValueCast!_eraseKey
 
 theorem get!_erase_self [LawfulBEq α] {k : α} [Inhabited (β k)] :
@@ -372,7 +372,7 @@ theorem get!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α
   simp_to_model; empty
 
 theorem get!_insert [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} :
-    get! (m.insert k v) a = bif a == k then v else get! m a := by
+    get! (m.insert k v) a = bif k == a then v else get! m a := by
   simp_to_model using List.getValue!_insertEntry
 
 theorem get!_insert_self [EquivBEq α] [LawfulHashable α] [Inhabited β] {k : α} {v : β} :
@@ -384,7 +384,7 @@ theorem get!_eq_default [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α
   simp_to_model using List.getValue!_eq_default
 
 theorem get!_erase [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} :
-    get! (m.erase k) a = bif a == k then default else get! m a := by
+    get! (m.erase k) a = bif k == a then default else get! m a := by
   simp_to_model using List.getValue!_eraseKey
 
 theorem get!_erase_self [EquivBEq α] [LawfulHashable α] [Inhabited β] {k : α} :
@@ -423,7 +423,7 @@ theorem getD_of_isEmpty [LawfulBEq α] {a : α} {fallback : β a} :
 
 theorem getD_insert [LawfulBEq α] {k a : α} {fallback : β a} {v : β k} :
     (m.insert k v).getD a fallback =
-      if h : a == k then cast (congrArg β (eq_of_beq h).symm) v else m.getD a fallback := by
+      if h : k == a then cast (congrArg β (eq_of_beq h)) v else m.getD a fallback := by
   simp_to_model using List.getValueCastD_insertEntry
 
 theorem getD_insert_self [LawfulBEq α] {a : α} {fallback b : β a} :
@@ -435,7 +435,7 @@ theorem getD_eq_fallback [LawfulBEq α] {a : α} {fallback : β a} :
   simp_to_model using List.getValueCastD_eq_fallback
 
 theorem getD_erase [LawfulBEq α] {k a : α} {fallback : β a} :
-    (m.erase k).getD a fallback = bif a == k then fallback else m.getD a fallback := by
+    (m.erase k).getD a fallback = bif k == a then fallback else m.getD a fallback := by
   simp_to_model using List.getValueCastD_eraseKey
 
 theorem getD_erase_self [LawfulBEq α] {k : α} {fallback : β k} :
@@ -471,7 +471,7 @@ theorem getD_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} {fallback :
   simp_to_model; empty
 
 theorem getD_insert [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} :
-    getD (m.insert k v) a fallback = bif a == k then v else getD m a fallback := by
+    getD (m.insert k v) a fallback = bif k == a then v else getD m a fallback := by
   simp_to_model using List.getValueD_insertEntry
 
 theorem getD_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {fallback v : β} :
@@ -483,7 +483,7 @@ theorem getD_eq_fallback [EquivBEq α] [LawfulHashable α] {a : α} {fallback :
   simp_to_model using List.getValueD_eq_fallback
 
 theorem getD_erase [EquivBEq α] [LawfulHashable α] {k a : α} {fallback : β} :
-    getD (m.erase k) a fallback = bif a == k then fallback else getD m a fallback := by
+    getD (m.erase k) a fallback = bif k == a then fallback else getD m a fallback := by
   simp_to_model using List.getValueD_eraseKey
 
 theorem getD_erase_self [EquivBEq α] [LawfulHashable α] {k : α} {fallback : β} :
@@ -521,7 +521,7 @@ theorem isEmpty_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β k
   simp_to_model using List.isEmpty_insertEntryIfNew
 
 theorem contains_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
-    (m.insertIfNew k v).contains a = (a == k || m.contains a) := by
+    (m.insertIfNew k v).contains a = (k == a || m.contains a) := by
   simp_to_model using List.containsKey_insertEntryIfNew
 
 theorem contains_insertIfNew_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
@@ -529,13 +529,13 @@ theorem contains_insertIfNew_self [EquivBEq α] [LawfulHashable α] {k : α} {v
   simp_to_model using List.containsKey_insertEntryIfNew_self
 
 theorem contains_of_contains_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
-    (m.insertIfNew k v).contains a → (a == k) = false → m.contains a := by
+    (m.insertIfNew k v).contains a → (k == a) = false → m.contains a := by
   simp_to_model using List.containsKey_of_containsKey_insertEntryIfNew
 
 /-- This is a restatement of `contains_insertIfNew` that is written to exactly match the proof
 obligation in the statement of `get_insertIfNew`. -/
 theorem contains_of_contains_insertIfNew' [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
-    (m.insertIfNew k v).contains a → ¬((a == k) ∧ m.contains k = false) → m.contains a := by
+    (m.insertIfNew k v).contains a → ¬((k == a) ∧ m.contains k = false) → m.contains a := by
   simp_to_model using List.containsKey_of_containsKey_insertEntryIfNew'
 
 theorem size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
@@ -548,25 +548,25 @@ theorem size_le_size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v :
 
 theorem get?_insertIfNew [LawfulBEq α] {k a : α} {v : β k} :
     (m.insertIfNew k v).get? a =
-      if h : a == k ∧ m.contains k = false then some (cast (congrArg β (eq_of_beq h.1).symm) v)
+      if h : k == a ∧ m.contains k = false then some (cast (congrArg β (eq_of_beq h.1)) v)
       else m.get? a := by
   simp_to_model using List.getValueCast?_insertEntryIfNew
 
 theorem get_insertIfNew [LawfulBEq α] {k a : α} {v : β k} {h₁} :
     (m.insertIfNew k v).get a h₁ =
-      if h₂ : a == k ∧ m.contains k = false then cast (congrArg β (eq_of_beq h₂.1).symm) v
+      if h₂ : k == a ∧ m.contains k = false then cast (congrArg β (eq_of_beq h₂.1)) v
       else m.get a (contains_of_contains_insertIfNew' _ h h₁ h₂) := by
   simp_to_model using List.getValueCast_insertEntryIfNew
 
 theorem get!_insertIfNew [LawfulBEq α] {k a : α} [Inhabited (β a)] {v : β k} :
     (m.insertIfNew k v).get! a =
-      if h : a == k ∧ m.contains k = false then cast (congrArg β (eq_of_beq h.1).symm) v
+      if h : k == a ∧ m.contains k = false then cast (congrArg β (eq_of_beq h.1)) v
       else m.get! a := by
   simp_to_model using List.getValueCast!_insertEntryIfNew
 
 theorem getD_insertIfNew [LawfulBEq α] {k a : α} {fallback : β a} {v : β k} :
     (m.insertIfNew k v).getD a fallback =
-      if h : a == k ∧ m.contains k = false then cast (congrArg β (eq_of_beq h.1).symm) v
+      if h : k == a ∧ m.contains k = false then cast (congrArg β (eq_of_beq h.1)) v
       else m.getD a fallback := by
   simp_to_model using List.getValueCastD_insertEntryIfNew
 
@@ -575,22 +575,22 @@ namespace Const
 variable {β : Type v} (m : Raw₀ α (fun _ => β)) (h : m.1.WF)
 
 theorem get?_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
-    get? (m.insertIfNew k v) a = bif a == k && !m.contains k then some v else get? m a := by
+    get? (m.insertIfNew k v) a = bif k == a && !m.contains k then some v else get? m a := by
   simp_to_model using List.getValue?_insertEntryIfNew
 
 theorem get_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁} :
     get (m.insertIfNew k v) a h₁ =
-      if h₂ : a == k ∧ m.contains k = false then v
+      if h₂ : k == a ∧ m.contains k = false then v
       else get m a (contains_of_contains_insertIfNew' _ h h₁ h₂) := by
   simp_to_model using List.getValue_insertEntryIfNew
 
 theorem get!_insertIfNew [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} :
-    get! (m.insertIfNew k v) a = bif a == k && !m.contains k then v else get! m a := by
+    get! (m.insertIfNew k v) a = bif k == a && !m.contains k then v else get! m a := by
   simp_to_model using List.getValue!_insertEntryIfNew
 
 theorem getD_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} :
     getD (m.insertIfNew k v) a fallback =
-      bif a == k && !m.contains k then v else getD m a fallback := by
+      bif k == a && !m.contains k then v else getD m a fallback := by
   simp_to_model using List.getValueD_insertEntryIfNew
 
 end Const

src/Std/Data/DHashMap/Lemmas.lean

@@ -22,7 +22,7 @@ set_option autoImplicit false
 
 universe u v
 
-variable {α : Type u} {β : α → Type v} [BEq α] [Hashable α]
+variable {α : Type u} {β : α → Type v} {_ : BEq α} {_ : Hashable α}
 
 namespace Std.DHashMap
 
@@ -65,20 +65,20 @@ theorem mem_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) :
 
 @[simp]
 theorem contains_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
-    (m.insert k v).contains a = (a == k || m.contains a) :=
+    (m.insert k v).contains a = (k == a || m.contains a) :=
   Raw₀.contains_insert ⟨m.1, _⟩ m.2
 
 @[simp]
 theorem mem_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
-    a ∈ m.insert k v ↔ a == k ∨ a ∈ m := by
+    a ∈ m.insert k v ↔ k == a ∨ a ∈ m := by
   simp [mem_iff_contains, contains_insert]
 
 theorem contains_of_contains_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
-    (m.insert k v).contains a → (a == k) = false → m.contains a :=
+    (m.insert k v).contains a → (k == a) = false → m.contains a :=
   Raw₀.contains_of_contains_insert ⟨m.1, _⟩ m.2
 
 theorem mem_of_mem_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
-    a ∈ m.insert k v → (a == k) = false → a ∈ m := by
+    a ∈ m.insert k v → (k == a) = false → a ∈ m := by
   simpa [mem_iff_contains, -contains_insert] using contains_of_contains_insert
 
 @[simp]
@@ -124,12 +124,12 @@ theorem isEmpty_erase [EquivBEq α] [LawfulHashable α] {k : α} :
 
 @[simp]
 theorem contains_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
-    (m.erase k).contains a = (!(a == k) && m.contains a) :=
+    (m.erase k).contains a = (!(k == a) && m.contains a) :=
   Raw₀.contains_erase ⟨m.1, _⟩ m.2
 
 @[simp]
 theorem mem_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
-    a ∈ m.erase k ↔ (a == k) = false ∧ a ∈ m := by
+    a ∈ m.erase k ↔ (k == a) = false ∧ a ∈ m := by
   simp [mem_iff_contains, contains_erase]
 
 theorem contains_of_contains_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
@@ -176,7 +176,7 @@ theorem get?_of_isEmpty [LawfulBEq α] {a : α} : m.isEmpty = true → m.get? a
   Raw₀.get?_of_isEmpty ⟨m.1, _⟩ m.2
 
 theorem get?_insert [LawfulBEq α] {a k : α} {v : β k} : (m.insert k v).get? a =
-    if h : a == k then some (cast (congrArg β (eq_of_beq h).symm) v) else m.get? a :=
+    if h : k == a then some (cast (congrArg β (eq_of_beq h)) v) else m.get? a :=
   Raw₀.get?_insert ⟨m.1, _⟩ m.2
 
 @[simp]
@@ -194,7 +194,7 @@ theorem get?_eq_none [LawfulBEq α] {a : α} : ¬a ∈ m → m.get? a = none :=
   simpa [mem_iff_contains] using get?_eq_none_of_contains_eq_false
 
 theorem get?_erase [LawfulBEq α] {k a : α} :
-    (m.erase k).get? a = bif a == k then none else m.get? a :=
+    (m.erase k).get? a = bif k == a then none else m.get? a :=
   Raw₀.get?_erase ⟨m.1, _⟩ m.2
 
 @[simp]
@@ -218,7 +218,7 @@ theorem get?_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
   Raw₀.Const.get?_of_isEmpty ⟨m.1, _⟩ m.2
 
 theorem get?_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
-    get? (m.insert k v) a = bif a == k then some v else get? m a :=
+    get? (m.insert k v) a = bif k == a then some v else get? m a :=
   Raw₀.Const.get?_insert ⟨m.1, _⟩ m.2
 
 @[simp]
@@ -238,7 +238,7 @@ theorem get?_eq_none [EquivBEq α] [LawfulHashable α] {a : α } : ¬a ∈ m →
   simpa [mem_iff_contains] using get?_eq_none_of_contains_eq_false
 
 theorem get?_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
-    Const.get? (m.erase k) a = bif a == k then none else get? m a :=
+    Const.get? (m.erase k) a = bif k == a then none else get? m a :=
   Raw₀.Const.get?_erase ⟨m.1, _⟩ m.2
 
 @[simp]
@@ -255,8 +255,8 @@ end Const
 
 theorem get_insert [LawfulBEq α] {k a : α} {v : β k} {h₁} :
     (m.insert k v).get a h₁ =
-      if h₂ : a == k then
-        cast (congrArg β (eq_of_beq h₂).symm) v
+      if h₂ : k == a then
+        cast (congrArg β (eq_of_beq h₂)) v
       else
         m.get a (mem_of_mem_insert h₁ (Bool.eq_false_iff.2 h₂)) :=
   Raw₀.get_insert ⟨m.1, _⟩ m.2
@@ -280,7 +280,7 @@ variable {β : Type v} {m : DHashMap α (fun _ => β)}
 
 theorem get_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁} :
     get (m.insert k v) a h₁ =
-      if h₂ : a == k then v else get m a (mem_of_mem_insert h₁ (Bool.eq_false_iff.2 h₂)) :=
+      if h₂ : k == a then v else get m a (mem_of_mem_insert h₁ (Bool.eq_false_iff.2 h₂)) :=
   Raw₀.Const.get_insert ⟨m.1, _⟩ m.2
 
 @[simp]
@@ -322,7 +322,7 @@ theorem get!_of_isEmpty [LawfulBEq α] {a : α} [Inhabited (β a)] :
 
 theorem get!_insert [LawfulBEq α] {k a : α} [Inhabited (β a)] {v : β k} :
     (m.insert k v).get! a =
-      if h : a == k then cast (congrArg β (eq_of_beq h).symm) v else m.get! a :=
+      if h : k == a then cast (congrArg β (eq_of_beq h)) v else m.get! a :=
   Raw₀.get!_insert ⟨m.1, _⟩ m.2
 
 @[simp]
@@ -339,7 +339,7 @@ theorem get!_eq_default [LawfulBEq α] {a : α} [Inhabited (β a)] :
   simpa [mem_iff_contains] using get!_eq_default_of_contains_eq_false
 
 theorem get!_erase [LawfulBEq α] {k a : α} [Inhabited (β a)] :
-    (m.erase k).get! a = bif a == k then default else m.get! a :=
+    (m.erase k).get! a = bif k == a then default else m.get! a :=
   Raw₀.get!_erase ⟨m.1, _⟩ m.2
 
 @[simp]
@@ -381,7 +381,7 @@ theorem get!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α
   Raw₀.Const.get!_of_isEmpty ⟨m.1, _⟩ m.2
 
 theorem get!_insert [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} :
-    get! (m.insert k v) a = bif a == k then v else get! m a :=
+    get! (m.insert k v) a = bif k == a then v else get! m a :=
   Raw₀.Const.get!_insert ⟨m.1, _⟩ m.2
 
 @[simp]
@@ -398,7 +398,7 @@ theorem get!_eq_default [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α
   simpa [mem_iff_contains] using get!_eq_default_of_contains_eq_false
 
 theorem get!_erase [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} :
-    get! (m.erase k) a = bif a == k then default else get! m a :=
+    get! (m.erase k) a = bif k == a then default else get! m a :=
   Raw₀.Const.get!_erase ⟨m.1, _⟩ m.2
 
 @[simp]
@@ -448,7 +448,7 @@ theorem getD_of_isEmpty [LawfulBEq α] {a : α} {fallback : β a} :
 
 theorem getD_insert [LawfulBEq α] {k a : α} {fallback : β a} {v : β k} :
     (m.insert k v).getD a fallback =
-      if h : a == k then cast (congrArg β (eq_of_beq h).symm) v else m.getD a fallback :=
+      if h : k == a then cast (congrArg β (eq_of_beq h)) v else m.getD a fallback :=
   Raw₀.getD_insert ⟨m.1, _⟩ m.2
 
 @[simp]
@@ -465,7 +465,7 @@ theorem getD_eq_fallback [LawfulBEq α] {a : α} {fallback : β a} :
   simpa [mem_iff_contains] using getD_eq_fallback_of_contains_eq_false
 
 theorem getD_erase [LawfulBEq α] {k a : α} {fallback : β a} :
-    (m.erase k).getD a fallback = bif a == k then fallback else m.getD a fallback :=
+    (m.erase k).getD a fallback = bif k == a then fallback else m.getD a fallback :=
   Raw₀.getD_erase ⟨m.1, _⟩ m.2
 
 @[simp]
@@ -512,7 +512,7 @@ theorem getD_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} {fallback :
   Raw₀.Const.getD_of_isEmpty ⟨m.1, _⟩ m.2
 
 theorem getD_insert [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} :
-    getD (m.insert k v) a fallback = bif a == k then v else getD m a fallback :=
+    getD (m.insert k v) a fallback = bif k == a then v else getD m a fallback :=
   Raw₀.Const.getD_insert ⟨m.1, _⟩ m.2
 
 @[simp]
@@ -529,7 +529,7 @@ theorem getD_eq_fallback [EquivBEq α] [LawfulHashable α] {a : α} {fallback :
   simpa [mem_iff_contains] using getD_eq_fallback_of_contains_eq_false
 
 theorem getD_erase [EquivBEq α] [LawfulHashable α] {k a : α} {fallback : β} :
-    getD (m.erase k) a fallback = bif a == k then fallback else getD m a fallback :=
+    getD (m.erase k) a fallback = bif k == a then fallback else getD m a fallback :=
   Raw₀.Const.getD_erase ⟨m.1, _⟩ m.2
 
 @[simp]
@@ -574,12 +574,12 @@ theorem isEmpty_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β k
 
 @[simp]
 theorem contains_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
-    (m.insertIfNew k v).contains a = (a == k || m.contains a) :=
+    (m.insertIfNew k v).contains a = (k == a || m.contains a) :=
   Raw₀.contains_insertIfNew ⟨m.1, _⟩ m.2
 
 @[simp]
 theorem mem_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
-    a ∈ m.insertIfNew k v ↔ a == k ∨ a ∈ m := by
+    a ∈ m.insertIfNew k v ↔ k == a ∨ a ∈ m := by
   simp [mem_iff_contains, contains_insertIfNew]
 
 theorem contains_insertIfNew_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
@@ -591,23 +591,23 @@ theorem mem_insertIfNew_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β
   simpa [mem_iff_contains, -contains_insertIfNew] using contains_insertIfNew_self
 
 theorem contains_of_contains_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
-    (m.insertIfNew k v).contains a → (a == k) = false → m.contains a :=
+    (m.insertIfNew k v).contains a → (k == a) = false → m.contains a :=
   Raw₀.contains_of_contains_insertIfNew ⟨m.1, _⟩ m.2
 
 theorem mem_of_mem_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
-    a ∈ m.insertIfNew k v → (a == k) = false → a ∈ m := by
+    a ∈ m.insertIfNew k v → (k == a) = false → a ∈ m := by
   simpa [mem_iff_contains, -contains_insertIfNew] using contains_of_contains_insertIfNew
 
 /-- This is a restatement of `contains_insertIfNew` that is written to exactly match the proof
 obligation in the statement of `get_insertIfNew`. -/
 theorem contains_of_contains_insertIfNew' [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
-    (m.insertIfNew k v).contains a → ¬((a == k) ∧ m.contains k = false) → m.contains a :=
+    (m.insertIfNew k v).contains a → ¬((k == a) ∧ m.contains k = false) → m.contains a :=
   Raw₀.contains_of_contains_insertIfNew' ⟨m.1, _⟩ m.2
 
 /-- This is a restatement of `mem_insertIfNew` that is written to exactly match the proof obligation
 in the statement of `get_insertIfNew`. -/
 theorem mem_of_mem_insertIfNew' [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
-    a ∈ m.insertIfNew k v → ¬((a == k) ∧ ¬k ∈ m) → a ∈ m := by
+    a ∈ m.insertIfNew k v → ¬((k == a) ∧ ¬k ∈ m) → a ∈ m := by
   simpa [mem_iff_contains, -contains_insertIfNew] using contains_of_contains_insertIfNew'
 
 theorem size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
@@ -619,25 +619,25 @@ theorem size_le_size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v :
   Raw₀.size_le_size_insertIfNew ⟨m.1, _⟩ m.2
 
 theorem get?_insertIfNew [LawfulBEq α] {k a : α} {v : β k} : (m.insertIfNew k v).get? a =
-    if h : a == k ∧ ¬k ∈ m then some (cast (congrArg β (eq_of_beq h.1).symm) v) else m.get? a := by
+    if h : k == a ∧ ¬k ∈ m then some (cast (congrArg β (eq_of_beq h.1)) v) else m.get? a := by
   simp only [mem_iff_contains, Bool.not_eq_true]
   exact Raw₀.get?_insertIfNew ⟨m.1, _⟩ m.2
 
 theorem get_insertIfNew [LawfulBEq α] {k a : α} {v : β k} {h₁} : (m.insertIfNew k v).get a h₁ =
-    if h₂ : a == k ∧ ¬k ∈ m then cast (congrArg β (eq_of_beq h₂.1).symm) v else m.get a
+    if h₂ : k == a ∧ ¬k ∈ m then cast (congrArg β (eq_of_beq h₂.1)) v else m.get a
       (mem_of_mem_insertIfNew' h₁ h₂) := by
   simp only [mem_iff_contains, Bool.not_eq_true]
   exact Raw₀.get_insertIfNew ⟨m.1, _⟩ m.2
 
 theorem get!_insertIfNew [LawfulBEq α] {k a : α} [Inhabited (β a)] {v : β k} :
     (m.insertIfNew k v).get! a =
-      if h : a == k ∧ ¬k ∈ m then cast (congrArg β (eq_of_beq h.1).symm) v else m.get! a := by
+      if h : k == a ∧ ¬k ∈ m then cast (congrArg β (eq_of_beq h.1)) v else m.get! a := by
   simp only [mem_iff_contains, Bool.not_eq_true]
   exact Raw₀.get!_insertIfNew ⟨m.1, _⟩ m.2
 
 theorem getD_insertIfNew [LawfulBEq α] {k a : α} {fallback : β a} {v : β k} :
     (m.insertIfNew k v).getD a fallback =
-      if h : a == k ∧ ¬k ∈ m then cast (congrArg β (eq_of_beq h.1).symm) v
+      if h : k == a ∧ ¬k ∈ m then cast (congrArg β (eq_of_beq h.1)) v
       else m.getD a fallback := by
   simp only [mem_iff_contains, Bool.not_eq_true]
   exact Raw₀.getD_insertIfNew ⟨m.1, _⟩ m.2
@@ -647,22 +647,22 @@ namespace Const
 variable {β : Type v} {m : DHashMap α (fun _ => β)}
 
 theorem get?_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
-    get? (m.insertIfNew k v) a = bif a == k && !m.contains k then some v else get? m a :=
+    get? (m.insertIfNew k v) a = bif k == a && !m.contains k then some v else get? m a :=
   Raw₀.Const.get?_insertIfNew ⟨m.1, _⟩ m.2
 
 theorem get_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁} :
     get (m.insertIfNew k v) a h₁ =
-      if h₂ : a == k ∧ ¬k ∈ m then v else get m a (mem_of_mem_insertIfNew' h₁ h₂) := by
+      if h₂ : k == a ∧ ¬k ∈ m then v else get m a (mem_of_mem_insertIfNew' h₁ h₂) := by
   simp only [mem_iff_contains, Bool.not_eq_true]
   exact Raw₀.Const.get_insertIfNew ⟨m.1, _⟩ m.2
 
 theorem get!_insertIfNew [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} :
-    get! (m.insertIfNew k v) a = bif a == k && !m.contains k then v else get! m a :=
+    get! (m.insertIfNew k v) a = bif k == a && !m.contains k then v else get! m a :=
   Raw₀.Const.get!_insertIfNew ⟨m.1, _⟩ m.2
 
 theorem getD_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} :
     getD (m.insertIfNew k v) a fallback =
-      bif a == k && !m.contains k then v else getD m a fallback :=
+      bif k == a && !m.contains k then v else getD m a fallback :=
   Raw₀.Const.getD_insertIfNew ⟨m.1, _⟩ m.2
 
 end Const

src/Std/Data/DHashMap/RawDef.lean

@@ -26,16 +26,19 @@ inductive types. The well-formedness invariant is called `Raw.WF`. When in doubt
 over `DHashMap.Raw`. Lemmas about the operations on `Std.Data.DHashMap.Raw` are available in the
 module `Std.Data.DHashMap.RawLemmas`.
 
-The hash map uses `==` (provided by the `BEq` typeclass) to compare keys and `hash` (provided by
-the `Hashable` typeclass) to hash them. To ensure that the operations behave as expected, `==`
-should be an equivalence relation and `a == b` should imply `hash a = hash b` (see also the
-`EquivBEq` and `LawfulHashable` typeclasses). Both of these conditions are automatic if the BEq
-instance is lawful, i.e., if `a == b` implies `a = b`.
+The hash table is backed by an `Array`. Users should make sure that the hash map is used linearly to
+avoid expensive copies.
 
 This is a simple separate-chaining hash table. The data of the hash map consists of a cached size
 and an array of buckets, where each bucket is a linked list of key-value pais. The number of buckets
 is always a power of two. The hash map doubles its size upon inserting an element such that the
 number of elements is more than 75% of the number of buckets.
+
+The hash map uses `==` (provided by the `BEq` typeclass) to compare keys and `hash` (provided by
+the `Hashable` typeclass) to hash them. To ensure that the operations behave as expected, `==`
+should be an equivalence relation and `a == b` should imply `hash a = hash b` (see also the
+`EquivBEq` and `LawfulHashable` typeclasses). Both of these conditions are automatic if the BEq
+instance is lawful, i.e., if `a == b` implies `a = b`.
 -/
 structure Raw (α : Type u) (β : α → Type v) where
   /-- The number of mappings present in the hash map -/

src/Std/Data/DHashMap/RawLemmas.lean

@@ -113,20 +113,20 @@ theorem mem_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) :
 
 @[simp]
 theorem contains_insert [EquivBEq α] [LawfulHashable α] {a k : α} {v : β k} :
-    (m.insert k v).contains a = (a == k || m.contains a) := by
+    (m.insert k v).contains a = (k == a || m.contains a) := by
   simp_to_raw using Raw₀.contains_insert
 
 @[simp]
 theorem mem_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
-    a ∈ m.insert k v ↔ a == k ∨ a ∈ m := by
+    a ∈ m.insert k v ↔ k == a ∨ a ∈ m := by
   simp [mem_iff_contains, contains_insert h]
 
 theorem contains_of_contains_insert [EquivBEq α] [LawfulHashable α] {a k : α} {v : β k} :
-    (m.insert k v).contains a → (a == k) = false → m.contains a := by
+    (m.insert k v).contains a → (k == a) = false → m.contains a := by
   simp_to_raw using Raw₀.contains_of_contains_insert
 
 theorem mem_of_mem_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
-    a ∈ m.insert k v → (a == k) = false → a ∈ m := by
+    a ∈ m.insert k v → (k == a) = false → a ∈ m := by
   simpa [mem_iff_contains] using contains_of_contains_insert h
 
 @[simp]
@@ -173,12 +173,12 @@ theorem isEmpty_erase [EquivBEq α] [LawfulHashable α] {k : α} :
 
 @[simp]
 theorem contains_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
-    (m.erase k).contains a = (!(a == k) && m.contains a) := by
+    (m.erase k).contains a = (!(k == a) && m.contains a) := by
   simp_to_raw using Raw₀.contains_erase
 
 @[simp]
 theorem mem_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
-    a ∈ m.erase k ↔ (a == k) = false ∧ a ∈ m := by
+    a ∈ m.erase k ↔ (k == a) = false ∧ a ∈ m := by
   simp [mem_iff_contains, contains_erase h]
 
 theorem contains_of_contains_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
@@ -225,7 +225,7 @@ theorem get?_of_isEmpty [LawfulBEq α] {a : α} : m.isEmpty = true → m.get? a
   simp_to_raw using Raw₀.get?_of_isEmpty ⟨m, _⟩
 
 theorem get?_insert [LawfulBEq α] {a k : α} {v : β k} : (m.insert k v).get? a =
-    if h : a == k then some (cast (congrArg β (eq_of_beq h).symm) v) else m.get? a := by
+    if h : k == a then some (cast (congrArg β (eq_of_beq h)) v) else m.get? a := by
   simp_to_raw using Raw₀.get?_insert
 
 @[simp]
@@ -243,7 +243,7 @@ theorem get?_eq_none [LawfulBEq α] {a : α} : ¬a ∈ m → m.get? a = none :=
   simpa [mem_iff_contains] using get?_eq_none_of_contains_eq_false h
 
 theorem get?_erase [LawfulBEq α] {k a : α} :
-    (m.erase k).get? a = bif a == k then none else m.get? a := by
+    (m.erase k).get? a = bif k == a then none else m.get? a := by
   simp_to_raw using Raw₀.get?_erase
 
 @[simp]
@@ -267,7 +267,7 @@ theorem get?_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
   simp_to_raw using Raw₀.Const.get?_of_isEmpty ⟨m, _⟩
 
 theorem get?_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
-    get? (m.insert k v) a = bif a == k then some v else get? m a := by
+    get? (m.insert k v) a = bif k == a then some v else get? m a := by
   simp_to_raw using Raw₀.Const.get?_insert
 
 @[simp]
@@ -287,7 +287,7 @@ theorem get?_eq_none [EquivBEq α] [LawfulHashable α] {a : α} : ¬a ∈ m →
     simpa [mem_iff_contains] using get?_eq_none_of_contains_eq_false h
 
 theorem get?_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
-    Const.get? (m.erase k) a = bif a == k then none else get? m a := by
+    Const.get? (m.erase k) a = bif k == a then none else get? m a := by
   simp_to_raw using Raw₀.Const.get?_erase
 
 @[simp]
@@ -305,8 +305,8 @@ end Const
 
 theorem get_insert [LawfulBEq α] {k a : α} {v : β k} {h₁} :
     (m.insert k v).get a h₁ =
-      if h₂ : a == k then
-        cast (congrArg β (eq_of_beq h₂).symm) v
+      if h₂ : k == a then
+        cast (congrArg β (eq_of_beq h₂)) v
       else
         m.get a (mem_of_mem_insert h h₁ (Bool.eq_false_iff.2 h₂)) := by
   simp_to_raw using Raw₀.get_insert ⟨m, _⟩
@@ -330,7 +330,7 @@ variable {β : Type v} {m : DHashMap.Raw α (fun _ => β)} (h : m.WF)
 
 theorem get_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁} :
     get (m.insert k v) a h₁ =
-      if h₂ : a == k then v else get m a (mem_of_mem_insert h h₁ (Bool.eq_false_iff.2 h₂)) := by
+      if h₂ : k == a then v else get m a (mem_of_mem_insert h h₁ (Bool.eq_false_iff.2 h₂)) := by
   simp_to_raw using Raw₀.Const.get_insert ⟨m, _⟩
 
 @[simp]
@@ -371,7 +371,7 @@ theorem get!_of_isEmpty [LawfulBEq α] {a : α} [Inhabited (β a)] :
   simp_to_raw using Raw₀.get!_of_isEmpty ⟨m, _⟩
 
 theorem get!_insert [LawfulBEq α] {k a : α} [Inhabited (β a)] {v : β k} : (m.insert k v).get! a =
-    if h : a == k then cast (congrArg β (eq_of_beq h).symm) v else m.get! a := by
+    if h : k == a then cast (congrArg β (eq_of_beq h)) v else m.get! a := by
   simp_to_raw using Raw₀.get!_insert
 
 @[simp]
@@ -388,7 +388,7 @@ theorem get!_eq_default [LawfulBEq α] {a : α} [Inhabited (β a)] :
   simpa [mem_iff_contains] using get!_eq_default_of_contains_eq_false h
 
 theorem get!_erase [LawfulBEq α] {k a : α} [Inhabited (β a)] :
-    (m.erase k).get! a = bif a == k then default else m.get! a := by
+    (m.erase k).get! a = bif k == a then default else m.get! a := by
   simp_to_raw using Raw₀.get!_erase
 
 @[simp]
@@ -429,7 +429,7 @@ theorem get!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α
   simp_to_raw using Raw₀.Const.get!_of_isEmpty ⟨m, _⟩
 
 theorem get!_insert [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} :
-    get! (m.insert k v) a = bif a == k then v else get! m a := by
+    get! (m.insert k v) a = bif k == a then v else get! m a := by
   simp_to_raw using Raw₀.Const.get!_insert
 
 @[simp]
@@ -446,7 +446,7 @@ theorem get!_eq_default [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α
   simpa [mem_iff_contains] using get!_eq_default_of_contains_eq_false h
 
 theorem get!_erase [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} :
-    get! (m.erase k) a = bif a == k then default else get! m a := by
+    get! (m.erase k) a = bif k == a then default else get! m a := by
   simp_to_raw using Raw₀.Const.get!_erase
 
 @[simp]
@@ -496,7 +496,7 @@ theorem getD_of_isEmpty [LawfulBEq α] {a : α} {fallback : β a} :
 
 theorem getD_insert [LawfulBEq α] {k a : α} {fallback : β a} {v : β k} :
     (m.insert k v).getD a fallback =
-      if h : a == k then cast (congrArg β (eq_of_beq h).symm) v else m.getD a fallback := by
+      if h : k == a then cast (congrArg β (eq_of_beq h)) v else m.getD a fallback := by
   simp_to_raw using Raw₀.getD_insert
 
 @[simp]
@@ -513,7 +513,7 @@ theorem getD_eq_fallback [LawfulBEq α] {a : α} {fallback : β a} :
   simpa [mem_iff_contains] using getD_eq_fallback_of_contains_eq_false h
 
 theorem getD_erase [LawfulBEq α] {k a : α} {fallback : β a} :
-    (m.erase k).getD a fallback = bif a == k then fallback else m.getD a fallback := by
+    (m.erase k).getD a fallback = bif k == a then fallback else m.getD a fallback := by
   simp_to_raw using Raw₀.getD_erase
 
 @[simp]
@@ -559,7 +559,7 @@ theorem getD_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} {fallback :
   simp_to_raw using Raw₀.Const.getD_of_isEmpty ⟨m, _⟩
 
 theorem getD_insert [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} :
-    getD (m.insert k v) a fallback = bif a == k then v else getD m a fallback := by
+    getD (m.insert k v) a fallback = bif k == a then v else getD m a fallback := by
   simp_to_raw using Raw₀.Const.getD_insert
 
 @[simp]
@@ -576,7 +576,7 @@ theorem getD_eq_fallback [EquivBEq α] [LawfulHashable α] {a : α} {fallback :
   simpa [mem_iff_contains] using getD_eq_fallback_of_contains_eq_false h
 
 theorem getD_erase [EquivBEq α] [LawfulHashable α] {k a : α} {fallback : β} :
-    getD (m.erase k) a fallback = bif a == k then fallback else getD m a fallback := by
+    getD (m.erase k) a fallback = bif k == a then fallback else getD m a fallback := by
   simp_to_raw using Raw₀.Const.getD_erase
 
 @[simp]
@@ -621,12 +621,12 @@ theorem isEmpty_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β k
 
 @[simp]
 theorem contains_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
-    (m.insertIfNew k v).contains a = (a == k || m.contains a) := by
+    (m.insertIfNew k v).contains a = (k == a || m.contains a) := by
   simp_to_raw using Raw₀.contains_insertIfNew
 
 @[simp]
 theorem mem_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
-    a ∈ m.insertIfNew k v ↔ a == k ∨ a ∈ m := by
+    a ∈ m.insertIfNew k v ↔ k == a ∨ a ∈ m := by
   simp [mem_iff_contains, contains_insertIfNew h]
 
 theorem contains_insertIfNew_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
@@ -638,23 +638,23 @@ theorem mem_insertIfNew_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β
   simpa [mem_iff_contains, -contains_insertIfNew] using contains_insertIfNew_self h
 
 theorem contains_of_contains_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
-    (m.insertIfNew k v).contains a → (a == k) = false → m.contains a := by
+    (m.insertIfNew k v).contains a → (k == a) = false → m.contains a := by
   simp_to_raw using Raw₀.contains_of_contains_insertIfNew
 
 theorem mem_of_mem_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
-    a ∈ m.insertIfNew k v → (a == k) = false → a ∈ m := by
+    a ∈ m.insertIfNew k v → (k == a) = false → a ∈ m := by
   simpa [mem_iff_contains, -contains_insertIfNew] using contains_of_contains_insertIfNew h
 
 /-- This is a restatement of `contains_insertIfNew` that is written to exactly match the proof
 obligation in the statement of `get_insertIfNew`. -/
 theorem contains_of_contains_insertIfNew' [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
-    (m.insertIfNew k v).contains a → ¬((a == k) ∧ m.contains k = false) → m.contains a := by
+    (m.insertIfNew k v).contains a → ¬((k == a) ∧ m.contains k = false) → m.contains a := by
   simp_to_raw using Raw₀.contains_of_contains_insertIfNew'
 
 /-- This is a restatement of `mem_insertIfNew` that is written to exactly match the proof obligation
 in the statement of `get_insertIfNew`. -/
 theorem mem_of_mem_insertIfNew' [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
-    a ∈ m.insertIfNew k v → ¬((a == k) ∧ ¬k ∈ m) → a ∈ m := by
+    a ∈ m.insertIfNew k v → ¬((k == a) ∧ ¬k ∈ m) → a ∈ m := by
   simpa [mem_iff_contains] using contains_of_contains_insertIfNew' h
 
 theorem size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
@@ -667,27 +667,27 @@ theorem size_le_size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v :
 
 theorem get?_insertIfNew [LawfulBEq α] {k a : α} {v : β k} :
     (m.insertIfNew k v).get? a =
-      if h : a == k ∧ ¬k ∈ m then some (cast (congrArg β (eq_of_beq h.1).symm) v)
+      if h : k == a ∧ ¬k ∈ m then some (cast (congrArg β (eq_of_beq h.1)) v)
       else m.get? a := by
   simp only [mem_iff_contains, Bool.not_eq_true]
   simp_to_raw using Raw₀.get?_insertIfNew ⟨m, _⟩
 
 theorem get_insertIfNew [LawfulBEq α] {k a : α} {v : β k} {h₁} :
     (m.insertIfNew k v).get a h₁ =
-      if h₂ : a == k ∧ ¬k ∈ m then cast (congrArg β (eq_of_beq h₂.1).symm) v
+      if h₂ : k == a ∧ ¬k ∈ m then cast (congrArg β (eq_of_beq h₂.1)) v
       else m.get a (mem_of_mem_insertIfNew' h h₁ h₂) := by
   simp only [mem_iff_contains, Bool.not_eq_true]
   simp_to_raw using Raw₀.get_insertIfNew ⟨m, _⟩
 
 theorem get!_insertIfNew [LawfulBEq α] {k a : α} [Inhabited (β a)] {v : β k} :
     (m.insertIfNew k v).get! a =
-      if h : a == k ∧ ¬k ∈ m then cast (congrArg β (eq_of_beq h.1).symm) v else m.get! a := by
+      if h : k == a ∧ ¬k ∈ m then cast (congrArg β (eq_of_beq h.1)) v else m.get! a := by
   simp only [mem_iff_contains, Bool.not_eq_true]
   simp_to_raw using Raw₀.get!_insertIfNew ⟨m, _⟩
 
 theorem getD_insertIfNew [LawfulBEq α] {k a : α} {fallback : β a} {v : β k} :
     (m.insertIfNew k v).getD a fallback =
-      if h : a == k ∧ ¬k ∈ m then cast (congrArg β (eq_of_beq h.1).symm) v
+      if h : k == a ∧ ¬k ∈ m then cast (congrArg β (eq_of_beq h.1)) v
       else m.getD a fallback := by
   simp only [mem_iff_contains, Bool.not_eq_true]
   simp_to_raw using Raw₀.getD_insertIfNew
@@ -697,23 +697,23 @@ namespace Const
 variable {β : Type v} {m : DHashMap.Raw α (fun _ => β)} (h : m.WF)
 
 theorem get?_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
-    get? (m.insertIfNew k v) a = bif a == k && !m.contains k then some v else get? m a := by
+    get? (m.insertIfNew k v) a = bif k == a && !m.contains k then some v else get? m a := by
   simp_to_raw using Raw₀.Const.get?_insertIfNew
 
 theorem get_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁} :
     get (m.insertIfNew k v) a h₁ =
-      if h₂ : a == k ∧ ¬k ∈ m then v
+      if h₂ : k == a ∧ ¬k ∈ m then v
       else get m a (mem_of_mem_insertIfNew' h h₁ h₂) := by
   simp only [mem_iff_contains, Bool.not_eq_true]
   simp_to_raw using Raw₀.Const.get_insertIfNew ⟨m, _⟩
 
 theorem get!_insertIfNew [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} :
-    get! (m.insertIfNew k v) a = bif a == k && !m.contains k then v else get! m a := by
+    get! (m.insertIfNew k v) a = bif k == a && !m.contains k then v else get! m a := by
   simp_to_raw using Raw₀.Const.get!_insertIfNew
 
 theorem getD_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} :
     getD (m.insertIfNew k v) a fallback =
-      bif a == k && !m.contains k then v else getD m a fallback := by
+      bif k == a && !m.contains k then v else getD m a fallback := by
   simp_to_raw using Raw₀.Const.getD_insertIfNew
 
 end Const

src/Std/Data/HashMap/Basic.lean

@@ -27,7 +27,7 @@ nested inductive types.
 
 universe u v w
 
-variable {α : Type u} {β : Type v}
+variable {α : Type u} {β : Type v} {_ : BEq α} {_ : Hashable α}
 
 namespace Std
 
@@ -39,6 +39,9 @@ and an array of buckets, where each bucket is a linked list of key-value pais. T
 is always a power of two. The hash map doubles its size upon inserting an element such that the
 number of elements is more than 75% of the number of buckets.
 
+The hash table is backed by an `Array`. Users should make sure that the hash map is used linearly to
+avoid expensive copies.
+
 The hash map uses `==` (provided by the `BEq` typeclass) to compare keys and `hash` (provided by
 the `Hashable` typeclass) to hash them. To ensure that the operations behave as expected, `==`
 should be an equivalence relation and `a == b` should imply `hash a = hash b` (see also the
@@ -69,21 +72,21 @@ instance [BEq α] [Hashable α] : EmptyCollection (HashMap α β) where
 instance [BEq α] [Hashable α] : Inhabited (HashMap α β) where
   default := ∅
 
-@[inline, inherit_doc DHashMap.insert] def insert [BEq α] [Hashable α] (m : HashMap α β) (a : α)
+@[inline, inherit_doc DHashMap.insert] def insert (m : HashMap α β) (a : α)
     (b : β) : HashMap α β :=
   ⟨m.inner.insert a b⟩
 
-@[inline, inherit_doc DHashMap.insertIfNew] def insertIfNew [BEq α] [Hashable α] (m : HashMap α β)
+@[inline, inherit_doc DHashMap.insertIfNew] def insertIfNew (m : HashMap α β)
     (a : α) (b : β) : HashMap α β :=
   ⟨m.inner.insertIfNew a b⟩
 
-@[inline, inherit_doc DHashMap.containsThenInsert] def containsThenInsert [BEq α] [Hashable α]
+@[inline, inherit_doc DHashMap.containsThenInsert] def containsThenInsert
     (m : HashMap α β) (a : α) (b : β) : Bool × HashMap α β :=
   let ⟨replaced, r⟩ := m.inner.containsThenInsert a b
   ⟨replaced, ⟨r⟩⟩
 
-@[inline, inherit_doc DHashMap.containsThenInsertIfNew] def containsThenInsertIfNew [BEq α]
-    [Hashable α] (m : HashMap α β) (a : α) (b : β) : Bool × HashMap α β :=
+@[inline, inherit_doc DHashMap.containsThenInsertIfNew] def containsThenInsertIfNew
+    (m : HashMap α β) (a : α) (b : β) : Bool × HashMap α β :=
   let ⟨replaced, r⟩ := m.inner.containsThenInsertIfNew a b
   ⟨replaced, ⟨r⟩⟩
 
@@ -96,7 +99,7 @@ returned map has a new value inserted.
 
 Equivalent to (but potentially faster than) calling `get?` followed by `insertIfNew`.
 -/
-@[inline] def getThenInsertIfNew? [BEq α] [Hashable α] (m : HashMap α β) (a : α) (b : β) :
+@[inline] def getThenInsertIfNew? (m : HashMap α β) (a : α) (b : β) :
     Option β × HashMap α β :=
   let ⟨previous, r⟩ := DHashMap.Const.getThenInsertIfNew? m.inner a b
   ⟨previous, ⟨r⟩⟩
@@ -106,10 +109,10 @@ The notation `m[a]?` is preferred over calling this function directly.
 
 Tries to retrieve the mapping for the given key, returning `none` if no such mapping is present.
 -/
-@[inline] def get? [BEq α] [Hashable α] (m : HashMap α β) (a : α) : Option β :=
+@[inline] def get? (m : HashMap α β) (a : α) : Option β :=
   DHashMap.Const.get? m.inner a
 
-@[inline, inherit_doc DHashMap.contains] def contains [BEq α] [Hashable α] (m : HashMap α β)
+@[inline, inherit_doc DHashMap.contains] def contains (m : HashMap α β)
     (a : α) : Bool :=
   m.inner.contains a
 
@@ -125,10 +128,10 @@ The notation `m[a]` or `m[a]'h` is preferred over calling this function directly
 Retrieves the mapping for the given key. Ensures that such a mapping exists by requiring a proof of
 `a ∈ m`.
 -/
-@[inline] def get [BEq α] [Hashable α] (m : HashMap α β) (a : α) (h : a ∈ m) : β :=
+@[inline] def get (m : HashMap α β) (a : α) (h : a ∈ m) : β :=
   DHashMap.Const.get m.inner a h
 
-@[inline, inherit_doc DHashMap.Const.getD] def getD [BEq α] [Hashable α] (m : HashMap α β) (a : α)
+@[inline, inherit_doc DHashMap.Const.getD] def getD (m : HashMap α β) (a : α)
     (fallback : β) : β :=
   DHashMap.Const.getD m.inner a fallback
 
@@ -137,7 +140,7 @@ The notation `m[a]!` is preferred over calling this function directly.
 
 Tries to retrieve the mapping for the given key, panicking if no such mapping is present.
 -/
-@[inline] def get! [BEq α] [Hashable α] [Inhabited β] (m : HashMap α β) (a : α) : β :=
+@[inline] def get! [Inhabited β] (m : HashMap α β) (a : α) : β :=
   DHashMap.Const.get! m.inner a
 
 instance [BEq α] [Hashable α] : GetElem? (HashMap α β) α β (fun m a => a ∈ m) where
@@ -145,37 +148,37 @@ instance [BEq α] [Hashable α] : GetElem? (HashMap α β) α β (fun m a => a
   getElem? m a := m.get? a
   getElem! m a := m.get! a
 
-@[inline, inherit_doc DHashMap.erase] def erase [BEq α] [Hashable α] (m : HashMap α β) (a : α) :
+@[inline, inherit_doc DHashMap.erase] def erase (m : HashMap α β) (a : α) :
     HashMap α β :=
   ⟨m.inner.erase a⟩
 
-@[inline, inherit_doc DHashMap.size] def size [BEq α] [Hashable α] (m : HashMap α β) : Nat :=
+@[inline, inherit_doc DHashMap.size] def size (m : HashMap α β) : Nat :=
   m.inner.size
 
-@[inline, inherit_doc DHashMap.isEmpty] def isEmpty [BEq α] [Hashable α] (m : HashMap α β) : Bool :=
+@[inline, inherit_doc DHashMap.isEmpty] def isEmpty (m : HashMap α β) : Bool :=
   m.inner.isEmpty
 
 section Unverified
 
 /-! We currently do not provide lemmas for the functions below. -/
 
-@[inline, inherit_doc DHashMap.filter] def filter [BEq α] [Hashable α] (f : α → β → Bool)
+@[inline, inherit_doc DHashMap.filter] def filter (f : α → β → Bool)
     (m : HashMap α β) : HashMap α β :=
   ⟨m.inner.filter f⟩
 
-@[inline, inherit_doc DHashMap.foldM] def foldM [BEq α] [Hashable α] {m : Type w → Type w}
+@[inline, inherit_doc DHashMap.foldM] def foldM {m : Type w → Type w}
     [Monad m] {γ : Type w} (f : γ → α → β → m γ) (init : γ) (b : HashMap α β) : m γ :=
   b.inner.foldM f init
 
-@[inline, inherit_doc DHashMap.fold] def fold [BEq α] [Hashable α] {γ : Type w}
+@[inline, inherit_doc DHashMap.fold] def fold {γ : Type w}
     (f : γ → α → β → γ) (init : γ) (b : HashMap α β) : γ :=
   b.inner.fold f init
 
-@[inline, inherit_doc DHashMap.forM] def forM [BEq α] [Hashable α] {m : Type w → Type w} [Monad m]
+@[inline, inherit_doc DHashMap.forM] def forM {m : Type w → Type w} [Monad m]
     (f : (a : α) → β → m PUnit) (b : HashMap α β) : m PUnit :=
   b.inner.forM f
 
-@[inline, inherit_doc DHashMap.forIn] def forIn [BEq α] [Hashable α] {m : Type w → Type w} [Monad m]
+@[inline, inherit_doc DHashMap.forIn] def forIn {m : Type w → Type w} [Monad m]
     {γ : Type w} (f : (a : α) → β → γ → m (ForInStep γ)) (init : γ) (b : HashMap α β) : m γ :=
   b.inner.forIn f init
 
@@ -185,33 +188,33 @@ instance [BEq α] [Hashable α] {m : Type w → Type w} : ForM m (HashMap α β)
 instance [BEq α] [Hashable α] {m : Type w → Type w} : ForIn m (HashMap α β) (α × β) where
   forIn m init f := m.forIn (fun a b acc => f (a, b) acc) init
 
-@[inline, inherit_doc DHashMap.Const.toList] def toList [BEq α] [Hashable α] (m : HashMap α β) :
+@[inline, inherit_doc DHashMap.Const.toList] def toList (m : HashMap α β) :
     List (α × β) :=
   DHashMap.Const.toList m.inner
 
-@[inline, inherit_doc DHashMap.Const.toArray] def toArray [BEq α] [Hashable α] (m : HashMap α β) :
+@[inline, inherit_doc DHashMap.Const.toArray] def toArray (m : HashMap α β) :
     Array (α × β) :=
   DHashMap.Const.toArray m.inner
 
-@[inline, inherit_doc DHashMap.keys] def keys [BEq α] [Hashable α] (m : HashMap α β) : List α :=
+@[inline, inherit_doc DHashMap.keys] def keys (m : HashMap α β) : List α :=
   m.inner.keys
 
-@[inline, inherit_doc DHashMap.keysArray] def keysArray [BEq α] [Hashable α] (m : HashMap α β) :
+@[inline, inherit_doc DHashMap.keysArray] def keysArray (m : HashMap α β) :
     Array α :=
   m.inner.keysArray
 
-@[inline, inherit_doc DHashMap.values] def values [BEq α] [Hashable α] (m : HashMap α β) : List β :=
+@[inline, inherit_doc DHashMap.values] def values (m : HashMap α β) : List β :=
   m.inner.values
 
-@[inline, inherit_doc DHashMap.valuesArray] def valuesArray [BEq α] [Hashable α] (m : HashMap α β) :
+@[inline, inherit_doc DHashMap.valuesArray] def valuesArray (m : HashMap α β) :
     Array β :=
   m.inner.valuesArray
 
-@[inline, inherit_doc DHashMap.Const.insertMany] def insertMany [BEq α] [Hashable α] {ρ : Type w}
+@[inline, inherit_doc DHashMap.Const.insertMany] def insertMany {ρ : Type w}
     [ForIn Id ρ (α × β)] (m : HashMap α β) (l : ρ) : HashMap α β :=
   ⟨DHashMap.Const.insertMany m.inner l⟩
 
-@[inline, inherit_doc DHashMap.Const.insertManyUnit] def insertManyUnit [BEq α] [Hashable α]
+@[inline, inherit_doc DHashMap.Const.insertManyUnit] def insertManyUnit
     {ρ : Type w} [ForIn Id ρ α] (m : HashMap α Unit) (l : ρ) : HashMap α Unit :=
   ⟨DHashMap.Const.insertManyUnit m.inner l⟩
 
@@ -223,7 +226,7 @@ instance [BEq α] [Hashable α] {m : Type w → Type w} : ForIn m (HashMap α β
     HashMap α Unit :=
   ⟨DHashMap.Const.unitOfList l⟩
 
-@[inline, inherit_doc DHashMap.Internal.numBuckets] def Internal.numBuckets [BEq α] [Hashable α]
+@[inline, inherit_doc DHashMap.Internal.numBuckets] def Internal.numBuckets
     (m : HashMap α β) : Nat :=
   DHashMap.Internal.numBuckets m.inner
 

src/Std/Data/HashMap/Lemmas.lean

@@ -20,7 +20,7 @@ set_option autoImplicit false
 
 universe u v
 
-variable {α : Type u} {β : Type v} [BEq α] [Hashable α]
+variable {α : Type u} {β : Type v} {_ : BEq α} {_ : Hashable α}
 
 namespace Std.HashMap
 
@@ -73,20 +73,20 @@ theorem mem_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) :
 
 @[simp]
 theorem contains_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
-    (m.insert k v).contains a = (a == k || m.contains a) :=
+    (m.insert k v).contains a = (k == a || m.contains a) :=
   DHashMap.contains_insert
 
 @[simp]
 theorem mem_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
-    a ∈ m.insert k v ↔ a == k ∨ a ∈ m :=
+    a ∈ m.insert k v ↔ k == a ∨ a ∈ m :=
   DHashMap.mem_insert
 
 theorem contains_of_contains_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
-    (m.insert k v).contains a → (a == k) = false → m.contains a :=
+    (m.insert k v).contains a → (k == a) = false → m.contains a :=
   DHashMap.contains_of_contains_insert
 
 theorem mem_of_mem_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
-    a ∈ m.insert k v → (a == k) = false → a ∈ m :=
+    a ∈ m.insert k v → (k == a) = false → a ∈ m :=
   DHashMap.mem_of_mem_insert
 
 @[simp]
@@ -132,12 +132,12 @@ theorem isEmpty_erase [EquivBEq α] [LawfulHashable α] {k : α} :
 
 @[simp]
 theorem contains_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
-    (m.erase k).contains a = (!(a == k) && m.contains a) :=
+    (m.erase k).contains a = (!(k == a) && m.contains a) :=
   DHashMap.contains_erase
 
 @[simp]
 theorem mem_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
-    a ∈ m.erase k ↔ (a == k) = false ∧ a ∈ m :=
+    a ∈ m.erase k ↔ (k == a) = false ∧ a ∈ m :=
   DHashMap.mem_erase
 
 theorem contains_of_contains_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
@@ -185,7 +185,7 @@ theorem getElem?_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
   DHashMap.Const.get?_of_isEmpty
 
 theorem getElem?_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
-    (m.insert k v)[a]? = bif a == k then some v else m[a]? :=
+    (m.insert k v)[a]? = bif k == a then some v else m[a]? :=
   DHashMap.Const.get?_insert
 
 @[simp]
@@ -205,7 +205,7 @@ theorem getElem?_eq_none [EquivBEq α] [LawfulHashable α] {a : α} : ¬a ∈ m
   DHashMap.Const.get?_eq_none
 
 theorem getElem?_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
-    (m.erase k)[a]? = bif a == k then none else m[a]? :=
+    (m.erase k)[a]? = bif k == a then none else m[a]? :=
   DHashMap.Const.get?_erase
 
 @[simp]
@@ -217,7 +217,7 @@ theorem getElem?_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a ==
 
 theorem getElem_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁} :
     (m.insert k v)[a]'h₁ =
-      if h₂ : a == k then v else m[a]'(mem_of_mem_insert h₁ (Bool.eq_false_iff.2 h₂)) :=
+      if h₂ : k == a then v else m[a]'(mem_of_mem_insert h₁ (Bool.eq_false_iff.2 h₂)) :=
   DHashMap.Const.get_insert (h₁ := h₁)
 
 @[simp]
@@ -251,7 +251,7 @@ theorem getElem!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited β] {a
   DHashMap.Const.get!_of_isEmpty
 
 theorem getElem!_insert [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} :
-    (m.insert k v)[a]! = bif a == k then v else m[a]! :=
+    (m.insert k v)[a]! = bif k == a then v else m[a]! :=
   DHashMap.Const.get!_insert
 
 @[simp]
@@ -268,7 +268,7 @@ theorem getElem!_eq_default [EquivBEq α] [LawfulHashable α] [Inhabited β] {a
   DHashMap.Const.get!_eq_default
 
 theorem getElem!_erase [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} :
-    (m.erase k)[a]! = bif a == k then default else m[a]! :=
+    (m.erase k)[a]! = bif k == a then default else m[a]! :=
   DHashMap.Const.get!_erase
 
 @[simp]
@@ -310,7 +310,7 @@ theorem getD_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} {fallback :
   DHashMap.Const.getD_of_isEmpty
 
 theorem getD_insert [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} :
-    (m.insert k v).getD a fallback = bif a == k then v else m.getD a fallback :=
+    (m.insert k v).getD a fallback = bif k == a then v else m.getD a fallback :=
   DHashMap.Const.getD_insert
 
 @[simp]
@@ -327,7 +327,7 @@ theorem getD_eq_fallback [EquivBEq α] [LawfulHashable α] {a : α} {fallback :
   DHashMap.Const.getD_eq_fallback
 
 theorem getD_erase [EquivBEq α] [LawfulHashable α] {k a : α} {fallback : β} :
-    (m.erase k).getD a fallback = bif a == k then fallback else m.getD a fallback :=
+    (m.erase k).getD a fallback = bif k == a then fallback else m.getD a fallback :=
   DHashMap.Const.getD_erase
 
 @[simp]
@@ -366,12 +366,12 @@ theorem isEmpty_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β}
 
 @[simp]
 theorem contains_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
-    (m.insertIfNew k v).contains a = (a == k || m.contains a) :=
+    (m.insertIfNew k v).contains a = (k == a || m.contains a) :=
   DHashMap.contains_insertIfNew
 
 @[simp]
 theorem mem_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
-    a ∈ m.insertIfNew k v ↔ a == k ∨ a ∈ m :=
+    a ∈ m.insertIfNew k v ↔ k == a ∨ a ∈ m :=
   DHashMap.mem_insertIfNew
 
 theorem contains_insertIfNew_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
@@ -383,23 +383,23 @@ theorem mem_insertIfNew_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β}
   DHashMap.mem_insertIfNew_self
 
 theorem contains_of_contains_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
-    (m.insertIfNew k v).contains a → (a == k) = false → m.contains a :=
+    (m.insertIfNew k v).contains a → (k == a) = false → m.contains a :=
   DHashMap.contains_of_contains_insertIfNew
 
 theorem mem_of_mem_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
-    a ∈ m.insertIfNew k v → (a == k) = false → a ∈ m :=
+    a ∈ m.insertIfNew k v → (k == a) = false → a ∈ m :=
   DHashMap.mem_of_mem_insertIfNew
 
 /-- This is a restatement of `contains_insertIfNew` that is written to exactly match the proof
 obligation in the statement of `getElem_insertIfNew`. -/
 theorem contains_of_contains_insertIfNew' [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
-    (m.insertIfNew k v).contains a → ¬((a == k) ∧ m.contains k = false) → m.contains a :=
+    (m.insertIfNew k v).contains a → ¬((k == a) ∧ m.contains k = false) → m.contains a :=
   DHashMap.contains_of_contains_insertIfNew'
 
 /-- This is a restatement of `mem_insertIfNew` that is written to exactly match the proof obligation
 in the statement of `getElem_insertIfNew`. -/
 theorem mem_of_mem_insertIfNew' [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
-    a ∈ m.insertIfNew k v → ¬((a == k) ∧ ¬k ∈ m) → a ∈ m :=
+    a ∈ m.insertIfNew k v → ¬((k == a) ∧ ¬k ∈ m) → a ∈ m :=
   DHashMap.mem_of_mem_insertIfNew'
 
 theorem size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
@@ -411,21 +411,21 @@ theorem size_le_size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v :
   DHashMap.size_le_size_insertIfNew
 
 theorem getElem?_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
-    (m.insertIfNew k v)[a]? = bif a == k && !m.contains k then some v else m[a]? :=
+    (m.insertIfNew k v)[a]? = bif k == a && !m.contains k then some v else m[a]? :=
   DHashMap.Const.get?_insertIfNew
 
 theorem getElem_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁} :
     (m.insertIfNew k v)[a]'h₁ =
-      if h₂ : a == k ∧ ¬k ∈ m then v else m[a]'(mem_of_mem_insertIfNew' h₁ h₂) :=
+      if h₂ : k == a ∧ ¬k ∈ m then v else m[a]'(mem_of_mem_insertIfNew' h₁ h₂) :=
   DHashMap.Const.get_insertIfNew (h₁ := h₁)
 
 theorem getElem!_insertIfNew [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} :
-    (m.insertIfNew k v)[a]! = bif a == k && !m.contains k then v else m[a]! :=
+    (m.insertIfNew k v)[a]! = bif k == a && !m.contains k then v else m[a]! :=
   DHashMap.Const.get!_insertIfNew
 
 theorem getD_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} :
     (m.insertIfNew k v).getD a fallback =
-      bif a == k && !m.contains k then v else m.getD a fallback :=
+      bif k == a && !m.contains k then v else m.getD a fallback :=
   DHashMap.Const.getD_insertIfNew
 
 @[simp]

src/Std/Data/HashMap/Raw.lean

@@ -37,17 +37,20 @@ inductive types. The well-formedness invariant is called `Raw.WF`. When in doubt
 over `HashMap.Raw`. Lemmas about the operations on `Std.Data.HashMap.Raw` are available in the
 module `Std.Data.HashMap.RawLemmas`.
 
+This is a simple separate-chaining hash table. The data of the hash map consists of a cached size
+and an array of buckets, where each bucket is a linked list of key-value pais. The number of buckets
+is always a power of two. The hash map doubles its size upon inserting an element such that the
+number of elements is more than 75% of the number of buckets.
+
+The hash table is backed by an `Array`. Users should make sure that the hash map is used linearly to
+avoid expensive copies.
+
 The hash map uses `==` (provided by the `BEq` typeclass) to compare keys and `hash` (provided by
 the `Hashable` typeclass) to hash them. To ensure that the operations behave as expected, `==`
 should be an equivalence relation and `a == b` should imply `hash a = hash b` (see also the
 `EquivBEq` and `LawfulHashable` typeclasses). Both of these conditions are automatic if the BEq
 instance is lawful, i.e., if `a == b` implies `a = b`.
 
-This is a simple separate-chaining hash table. The data of the hash map consists of a cached size
-and an array of buckets, where each bucket is a linked list of key-value pais. The number of buckets
-is always a power of two. The hash map doubles its size upon inserting an element such that the
-number of elements is more than 75% of the number of buckets.
-
 Dependent hash maps, in which keys may occur in their values' types, are available as
 `Std.Data.Raw.DHashMap`.
 -/

src/Std/Data/HashMap/RawLemmas.lean

@@ -72,20 +72,20 @@ theorem mem_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) :
 
 @[simp]
 theorem contains_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
-    (m.insert k v).contains a = (a == k || m.contains a) :=
+    (m.insert k v).contains a = (k == a || m.contains a) :=
   DHashMap.Raw.contains_insert h.out
 
 @[simp]
 theorem mem_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
-    a ∈ m.insert k v ↔ a == k ∨ a ∈ m :=
+    a ∈ m.insert k v ↔ k == a ∨ a ∈ m :=
   DHashMap.Raw.mem_insert h.out
 
 theorem contains_of_contains_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
-    (m.insert k v).contains a → (a == k) = false → m.contains a :=
+    (m.insert k v).contains a → (k == a) = false → m.contains a :=
   DHashMap.Raw.contains_of_contains_insert h.out
 
 theorem mem_of_mem_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
-    a ∈ m.insert k v → (a == k) = false → a ∈ m :=
+    a ∈ m.insert k v → (k == a) = false → a ∈ m :=
   DHashMap.Raw.mem_of_mem_insert h.out
 
 @[simp]
@@ -131,12 +131,12 @@ theorem isEmpty_erase [EquivBEq α] [LawfulHashable α] {k : α} :
 
 @[simp]
 theorem contains_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
-    (m.erase k).contains a = (!(a == k) && m.contains a) :=
+    (m.erase k).contains a = (!(k == a) && m.contains a) :=
   DHashMap.Raw.contains_erase h.out
 
 @[simp]
 theorem mem_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
-    a ∈ m.erase k ↔ (a == k) = false ∧ a ∈ m :=
+    a ∈ m.erase k ↔ (k == a) = false ∧ a ∈ m :=
   DHashMap.Raw.mem_erase h.out
 
 theorem contains_of_contains_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
@@ -184,7 +184,7 @@ theorem getElem?_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
   DHashMap.Raw.Const.get?_of_isEmpty h.out
 
 theorem getElem?_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
-    (m.insert k v)[a]? = bif a == k then some v else m[a]? :=
+    (m.insert k v)[a]? = bif k == a then some v else m[a]? :=
   DHashMap.Raw.Const.get?_insert h.out
 
 @[simp]
@@ -204,7 +204,7 @@ theorem getElem?_eq_none [EquivBEq α] [LawfulHashable α] {a : α} : ¬a ∈ m
   DHashMap.Raw.Const.get?_eq_none h.out
 
 theorem getElem?_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
-    (m.erase k)[a]? = bif a == k then none else m[a]? :=
+    (m.erase k)[a]? = bif k == a then none else m[a]? :=
   DHashMap.Raw.Const.get?_erase h.out
 
 @[simp]
@@ -216,7 +216,7 @@ theorem getElem?_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a ==
 
 theorem getElem_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁} :
     (m.insert k v)[a]'h₁ =
-      if h₂ : a == k then v else m[a]'(mem_of_mem_insert h h₁ (Bool.eq_false_iff.2 h₂)) :=
+      if h₂ : k == a then v else m[a]'(mem_of_mem_insert h h₁ (Bool.eq_false_iff.2 h₂)) :=
   DHashMap.Raw.Const.get_insert (h₁ := h₁) h.out
 
 @[simp]
@@ -250,7 +250,7 @@ theorem getElem!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited β] {a
   DHashMap.Raw.Const.get!_of_isEmpty h.out
 
 theorem getElem!_insert [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} :
-    (m.insert k v)[a]! = bif a == k then v else m[a]! :=
+    (m.insert k v)[a]! = bif k == a then v else m[a]! :=
   DHashMap.Raw.Const.get!_insert h.out
 
 @[simp]
@@ -267,7 +267,7 @@ theorem getElem!_eq_default [EquivBEq α] [LawfulHashable α] [Inhabited β] {a
   DHashMap.Raw.Const.get!_eq_default h.out
 
 theorem getElem!_erase [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} :
-    (m.erase k)[a]! = bif a == k then default else m[a]! :=
+    (m.erase k)[a]! = bif k == a then default else m[a]! :=
   DHashMap.Raw.Const.get!_erase h.out
 
 @[simp]
@@ -308,7 +308,7 @@ theorem getD_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} {fallback :
   DHashMap.Raw.Const.getD_of_isEmpty h.out
 
 theorem getD_insert [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} :
-    (m.insert k v).getD a fallback = bif a == k then v else m.getD a fallback :=
+    (m.insert k v).getD a fallback = bif k == a then v else m.getD a fallback :=
   DHashMap.Raw.Const.getD_insert h.out
 
 @[simp]
@@ -325,7 +325,7 @@ theorem getD_eq_fallback [EquivBEq α] [LawfulHashable α] {a : α} {fallback :
   DHashMap.Raw.Const.getD_eq_fallback h.out
 
 theorem getD_erase [EquivBEq α] [LawfulHashable α] {k a : α} {fallback : β} :
-    (m.erase k).getD a fallback = bif a == k then fallback else m.getD a fallback :=
+    (m.erase k).getD a fallback = bif k == a then fallback else m.getD a fallback :=
   DHashMap.Raw.Const.getD_erase h.out
 
 @[simp]
@@ -364,12 +364,12 @@ theorem isEmpty_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β}
 
 @[simp]
 theorem contains_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
-    (m.insertIfNew k v).contains a = (a == k || m.contains a) :=
+    (m.insertIfNew k v).contains a = (k == a || m.contains a) :=
   DHashMap.Raw.contains_insertIfNew h.out
 
 @[simp]
 theorem mem_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
-    a ∈ m.insertIfNew k v ↔ a == k ∨ a ∈ m :=
+    a ∈ m.insertIfNew k v ↔ k == a ∨ a ∈ m :=
   DHashMap.Raw.mem_insertIfNew h.out
 
 theorem contains_insertIfNew_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
@@ -381,23 +381,23 @@ theorem mem_insertIfNew_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β}
   DHashMap.Raw.mem_insertIfNew_self h.out
 
 theorem contains_of_contains_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
-    (m.insertIfNew k v).contains a → (a == k) = false → m.contains a :=
+    (m.insertIfNew k v).contains a → (k == a) = false → m.contains a :=
   DHashMap.Raw.contains_of_contains_insertIfNew h.out
 
 theorem mem_of_mem_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
-    a ∈ m.insertIfNew k v → (a == k) = false → a ∈ m :=
+    a ∈ m.insertIfNew k v → (k == a) = false → a ∈ m :=
   DHashMap.Raw.mem_of_mem_insertIfNew h.out
 
 /-- This is a restatement of `contains_insertIfNew` that is written to exactly match the proof
 obligation in the statement of `getElem_insertIfNew`. -/
 theorem contains_of_contains_insertIfNew' [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
-    (m.insertIfNew k v).contains a → ¬((a == k) ∧ m.contains k = false) → m.contains a :=
+    (m.insertIfNew k v).contains a → ¬((k == a) ∧ m.contains k = false) → m.contains a :=
   DHashMap.Raw.contains_of_contains_insertIfNew' h.out
 
 /-- This is a restatement of `mem_insertIfNew` that is written to exactly match the proof obligation
 in the statement of `getElem_insertIfNew`. -/
 theorem mem_of_mem_insertIfNew' [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
-    a ∈ m.insertIfNew k v → ¬((a == k) ∧ ¬k ∈ m) → a ∈ m :=
+    a ∈ m.insertIfNew k v → ¬((k == a) ∧ ¬k ∈ m) → a ∈ m :=
   DHashMap.Raw.mem_of_mem_insertIfNew' h.out
 
 theorem size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
@@ -409,21 +409,21 @@ theorem size_le_size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v :
   DHashMap.Raw.size_le_size_insertIfNew h.out
 
 theorem getElem?_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
-    (m.insertIfNew k v)[a]? = bif a == k && !m.contains k then some v else m[a]? :=
+    (m.insertIfNew k v)[a]? = bif k == a && !m.contains k then some v else m[a]? :=
   DHashMap.Raw.Const.get?_insertIfNew h.out
 
 theorem getElem_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁} :
     (m.insertIfNew k v)[a]'h₁ =
-      if h₂ : a == k ∧ ¬k ∈ m then v else m[a]'(mem_of_mem_insertIfNew' h h₁ h₂) :=
+      if h₂ : k == a ∧ ¬k ∈ m then v else m[a]'(mem_of_mem_insertIfNew' h h₁ h₂) :=
   DHashMap.Raw.Const.get_insertIfNew h.out (h₁ := h₁)
 
 theorem getElem!_insertIfNew [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} :
-    (m.insertIfNew k v)[a]! = bif a == k && !m.contains k then v else m[a]! :=
+    (m.insertIfNew k v)[a]! = bif k == a && !m.contains k then v else m[a]! :=
   DHashMap.Raw.Const.get!_insertIfNew h.out
 
 theorem getD_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} :
     (m.insertIfNew k v).getD a fallback =
-      bif a == k && !m.contains k then v else m.getD a fallback :=
+      bif k == a && !m.contains k then v else m.getD a fallback :=
   DHashMap.Raw.Const.getD_insertIfNew h.out
 
 @[simp]

src/Std/Data/HashSet/Basic.lean

@@ -23,7 +23,7 @@ set_option autoImplicit false
 
 universe u v
 
-variable {α : Type u}
+variable {α : Type u} {_ : BEq α} {_ : Hashable α}
 
 namespace Std
 
@@ -35,6 +35,9 @@ and an array of buckets, where each bucket is a linked list of keys. The number
 is always a power of two. The hash set doubles its size upon inserting an element such that the
 number of elements is more than 75% of the number of buckets.
 
+The hash table is backed by an `Array`. Users should make sure that the hash set is used linearly to
+avoid expensive copies.
+
 The hash set uses `==` (provided by the `BEq` typeclass) to compare elements and `hash` (provided by
 the `Hashable` typeclass) to hash them. To ensure that the operations behave as expected, `==`
 should be an equivalence relation and `a == b` should imply `hash a = hash b` (see also the
@@ -71,7 +74,7 @@ instance [BEq α] [Hashable α] : Inhabited (HashSet α) where
 Inserts the given element into the set. If the hash set already contains an element that is
 equal (with regard to `==`) to the given element, then the hash set is returned unchanged.
 -/
-@[inline] def insert [BEq α] [Hashable α] (m : HashSet α) (a : α) : HashSet α :=
+@[inline] def insert (m : HashSet α) (a : α) : HashSet α :=
   ⟨m.inner.insertIfNew a ()⟩
 
 /--
@@ -81,7 +84,7 @@ element, then the hash set is returned unchanged.
 
 Equivalent to (but potentially faster than) calling `contains` followed by `insert`.
 -/
-@[inline] def containsThenInsert [BEq α] [Hashable α] (m : HashSet α) (a : α) : Bool × HashSet α :=
+@[inline] def containsThenInsert (m : HashSet α) (a : α) : Bool × HashSet α :=
   let ⟨replaced, r⟩ := m.inner.containsThenInsertIfNew a ()
   ⟨replaced, ⟨r⟩⟩
 
@@ -92,7 +95,7 @@ this: `a ∈ m` is equivalent to `m.contains a = true`.
 Observe that this is different behavior than for lists: for lists, `∈` uses `=` and `contains` use
 `==` for comparisons, while for hash sets, both use `==`.
 -/
-@[inline] def contains [BEq α] [Hashable α] (m : HashSet α) (a : α) : Bool :=
+@[inline] def contains (m : HashSet α) (a : α) : Bool :=
   m.inner.contains a
 
 instance [BEq α] [Hashable α] : Membership α (HashSet α) where
@@ -102,11 +105,11 @@ instance [BEq α] [Hashable α] {m : HashSet α} {a : α} : Decidable (a ∈ m)
   inferInstanceAs (Decidable (a ∈ m.inner))
 
 /-- Removes the element if it exists. -/
-@[inline] def erase [BEq α] [Hashable α] (m : HashSet α) (a : α) : HashSet α :=
+@[inline] def erase (m : HashSet α) (a : α) : HashSet α :=
   ⟨m.inner.erase a⟩
 
 /-- The number of elements present in the set -/
-@[inline] def size [BEq α] [Hashable α] (m : HashSet α) : Nat :=
+@[inline] def size (m : HashSet α) : Nat :=
   m.inner.size
 
 /--
@@ -116,7 +119,7 @@ Note that if your `BEq` instance is not reflexive or your `Hashable` instance is
 lawful, then it is possible that this function returns `false` even though `m.contains a = false`
 for all `a`.
 -/
-@[inline] def isEmpty [BEq α] [Hashable α] (m : HashSet α) : Bool :=
+@[inline] def isEmpty (m : HashSet α) : Bool :=
   m.inner.isEmpty
 
 section Unverified
@@ -124,29 +127,29 @@ section Unverified
 /-! We currently do not provide lemmas for the functions below. -/
 
 /-- Removes all elements from the hash set for which the given function returns `false`. -/
-@[inline] def filter [BEq α] [Hashable α] (f : α → Bool) (m : HashSet α) : HashSet α :=
+@[inline] def filter (f : α → Bool) (m : HashSet α) : HashSet α :=
   ⟨m.inner.filter fun a _ => f a⟩
 
 /--
 Monadically computes a value by folding the given function over the elements in the hash set in some
 order.
 -/
-@[inline] def foldM [BEq α] [Hashable α] {m : Type v → Type v} [Monad m] {β : Type v}
+@[inline] def foldM {m : Type v → Type v} [Monad m] {β : Type v}
     (f : β → α → m β) (init : β) (b : HashSet α) : m β :=
   b.inner.foldM (fun b a _ => f b a) init
 
 /-- Folds the given function over the elements of the hash set in some order. -/
-@[inline] def fold [BEq α] [Hashable α] {β : Type v} (f : β → α → β) (init : β) (m : HashSet α) :
+@[inline] def fold {β : Type v} (f : β → α → β) (init : β) (m : HashSet α) :
     β :=
   m.inner.fold (fun b a _ => f b a) init
 
 /-- Carries out a monadic action on each element in the hash set in some order. -/
-@[inline] def forM [BEq α] [Hashable α] {m : Type v → Type v} [Monad m] (f : α → m PUnit)
+@[inline] def forM {m : Type v → Type v} [Monad m] (f : α → m PUnit)
     (b : HashSet α) : m PUnit :=
   b.inner.forM (fun a _ => f a)
 
 /-- Support for the `for` loop construct in `do` blocks. -/
-@[inline] def forIn [BEq α] [Hashable α] {m : Type v → Type v} [Monad m] {β : Type v}
+@[inline] def forIn {m : Type v → Type v} [Monad m] {β : Type v}
     (f : α → β → m (ForInStep β)) (init : β) (b : HashSet α) : m β :=
   b.inner.forIn (fun a _ acc => f a acc) init
 
@@ -157,11 +160,11 @@ instance [BEq α] [Hashable α] {m : Type v → Type v} : ForIn m (HashSet α)
   forIn m init f := m.forIn f init
 
 /-- Transforms the hash set into a list of elements in some order. -/
-@[inline] def toList [BEq α] [Hashable α] (m : HashSet α) : List α :=
+@[inline] def toList (m : HashSet α) : List α :=
   m.inner.keys
 
 /-- Transforms the hash set into an array of elements in some order. -/
-@[inline] def toArray [BEq α] [Hashable α] (m : HashSet α) : Array α :=
+@[inline] def toArray (m : HashSet α) : Array α :=
   m.inner.keysArray
 
 /--
@@ -169,7 +172,7 @@ Inserts multiple elements into the hash set. Note that unlike repeatedly calling
 collection contains multiple elements that are equal (with regard to `==`), then the last element
 in the collection will be present in the returned hash set.
 -/
-@[inline] def insertMany [BEq α] [Hashable α] {ρ : Type v} [ForIn Id ρ α] (m : HashSet α) (l : ρ) :
+@[inline] def insertMany {ρ : Type v} [ForIn Id ρ α] (m : HashSet α) (l : ρ) :
     HashSet α :=
   ⟨m.inner.insertManyUnit l⟩
 
@@ -186,7 +189,7 @@ Returns the number of buckets in the internal representation of the hash set. Th
 be useful for things like monitoring system health, but it should be considered an internal
 implementation detail.
 -/
-def Internal.numBuckets [BEq α] [Hashable α] (m : HashSet α) : Nat :=
+def Internal.numBuckets (m : HashSet α) : Nat :=
   HashMap.Internal.numBuckets m.inner
 
 instance [BEq α] [Hashable α] [Repr α] : Repr (HashSet α) where

src/Std/Data/HashSet/Lemmas.lean

@@ -20,7 +20,7 @@ set_option autoImplicit false
 
 universe u v
 
-variable {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α]
+variable {α : Type u} {_ : BEq α} {_ : Hashable α} [EquivBEq α] [LawfulHashable α]
 
 namespace Std.HashSet
 
@@ -67,19 +67,19 @@ theorem mem_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) :
 
 @[simp]
 theorem contains_insert [EquivBEq α] [LawfulHashable α] {k a : α} :
-    (m.insert k).contains a = (a == k || m.contains a) :=
+    (m.insert k).contains a = (k == a || m.contains a) :=
   HashMap.contains_insertIfNew
 
 @[simp]
-theorem mem_insert [EquivBEq α] [LawfulHashable α] {k a : α} : a ∈ m.insert k ↔ a == k ∨ a ∈ m :=
+theorem mem_insert [EquivBEq α] [LawfulHashable α] {k a : α} : a ∈ m.insert k ↔ k == a ∨ a ∈ m :=
   HashMap.mem_insertIfNew
 
 theorem contains_of_contains_insert [EquivBEq α] [LawfulHashable α] {k a : α} :
-    (m.insert k).contains a → (a == k) = false → m.contains a :=
+    (m.insert k).contains a → (k == a) = false → m.contains a :=
   HashMap.contains_of_contains_insertIfNew
 
 theorem mem_of_mem_insert [EquivBEq α] [LawfulHashable α] {k a : α} :
-    a ∈ m.insert k → (a == k) = false → a ∈ m :=
+    a ∈ m.insert k → (k == a) = false → a ∈ m :=
   HashMap.mem_of_mem_insertIfNew
 
 @[simp]
@@ -123,12 +123,12 @@ theorem isEmpty_erase [EquivBEq α] [LawfulHashable α] {k : α} :
 
 @[simp]
 theorem contains_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
-    (m.erase k).contains a = (!(a == k) && m.contains a) :=
+    (m.erase k).contains a = (!(k == a) && m.contains a) :=
   HashMap.contains_erase
 
 @[simp]
 theorem mem_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
-    a ∈ m.erase k ↔ (a == k) = false ∧ a ∈ m :=
+    a ∈ m.erase k ↔ (k == a) = false ∧ a ∈ m :=
   HashMap.mem_erase
 
 theorem contains_of_contains_erase [EquivBEq α] [LawfulHashable α] {k a : α} :

src/Std/Data/HashSet/Raw.lean

@@ -37,16 +37,19 @@ inductive types. The well-formedness invariant is called `Raw.WF`. When in doubt
 over `HashSet.Raw`. Lemmas about the operations on `Std.Data.HashSet.Raw` are available in the
 module `Std.Data.HashSet.RawLemmas`.
 
+This is a simple separate-chaining hash table. The data of the hash set consists of a cached size
+and an array of buckets, where each bucket is a linked list of keys. The number of buckets
+is always a power of two. The hash set doubles its size upon inserting an element such that the
+number of elements is more than 75% of the number of buckets.
+
+The hash table is backed by an `Array`. Users should make sure that the hash set is used linearly to
+avoid expensive copies.
+
 The hash set uses `==` (provided by the `BEq` typeclass) to compare elements and `hash` (provided by
 the `Hashable` typeclass) to hash them. To ensure that the operations behave as expected, `==`
 should be an equivalence relation and `a == b` should imply `hash a = hash b` (see also the
 `EquivBEq` and `LawfulHashable` typeclasses). Both of these conditions are automatic if the BEq
 instance is lawful, i.e., if `a == b` implies `a = b`.
-
-This is a simple separate-chaining hash table. The data of the hash set consists of a cached size
-and an array of buckets, where each bucket is a linked list of keys. The number of buckets
-is always a power of two. The hash set doubles its size upon inserting an element such that the
-number of elements is more than 75% of the number of buckets.
 -/
 structure Raw (α : Type u) where
   /-- Internal implementation detail of the hash set. -/

src/Std/Data/HashSet/RawLemmas.lean

@@ -67,19 +67,19 @@ theorem mem_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) :
 
 @[simp]
 theorem contains_insert [EquivBEq α] [LawfulHashable α] {k a : α} :
-    (m.insert k).contains a = (a == k || m.contains a) :=
+    (m.insert k).contains a = (k == a || m.contains a) :=
   HashMap.Raw.contains_insertIfNew h.out
 
 @[simp]
-theorem mem_insert [EquivBEq α] [LawfulHashable α] {k a : α} : a ∈ m.insert k ↔ a == k ∨ a ∈ m :=
+theorem mem_insert [EquivBEq α] [LawfulHashable α] {k a : α} : a ∈ m.insert k ↔ k == a ∨ a ∈ m :=
   HashMap.Raw.mem_insertIfNew h.out
 
 theorem contains_of_contains_insert [EquivBEq α] [LawfulHashable α] {k a : α} :
-    (m.insert k).contains a → (a == k) = false → m.contains a :=
+    (m.insert k).contains a → (k == a) = false → m.contains a :=
   HashMap.Raw.contains_of_contains_insertIfNew h.out
 
 theorem mem_of_mem_insert [EquivBEq α] [LawfulHashable α] {k a : α} :
-    a ∈ m.insert k → (a == k) = false → a ∈ m :=
+    a ∈ m.insert k → (k == a) = false → a ∈ m :=
   HashMap.Raw.mem_of_mem_insertIfNew h.out
 
 @[simp]
@@ -123,12 +123,12 @@ theorem isEmpty_erase [EquivBEq α] [LawfulHashable α] {k : α} :
 
 @[simp]
 theorem contains_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
-    (m.erase k).contains a = (!(a == k) && m.contains a) :=
+    (m.erase k).contains a = (!(k == a) && m.contains a) :=
   HashMap.Raw.contains_erase h.out
 
 @[simp]
 theorem mem_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
-    a ∈ m.erase k ↔ (a == k) = false ∧ a ∈ m :=
+    a ∈ m.erase k ↔ (k == a) = false ∧ a ∈ m :=
   HashMap.Raw.mem_erase h.out
 
 theorem contains_of_contains_erase [EquivBEq α] [LawfulHashable α] {k a : α} :

src/include/lean/lean.h

@@ -448,9 +448,6 @@ static inline void lean_inc(lean_object * o) { if (!lean_is_scalar(o)) lean_inc_
 static inline void lean_inc_n(lean_object * o, size_t n) { if (!lean_is_scalar(o)) lean_inc_ref_n(o, n); }
 static inline void lean_dec(lean_object * o) { if (!lean_is_scalar(o)) lean_dec_ref(o); }
 
-/* Just free memory */
-LEAN_EXPORT void lean_dealloc(lean_object * o);
-
 static inline bool lean_is_ctor(lean_object * o) { return lean_ptr_tag(o) <= LeanMaxCtorTag; }
 static inline bool lean_is_closure(lean_object * o) { return lean_ptr_tag(o) == LeanClosure; }
 static inline bool lean_is_array(lean_object * o) { return lean_ptr_tag(o) == LeanArray; }
@@ -484,6 +481,10 @@ static inline bool lean_is_exclusive(lean_object * o) {
     }
 }
 
+static inline uint8_t lean_is_exclusive_obj(lean_object * o) {
+    return lean_is_exclusive(o);
+}
+
 static inline bool lean_is_shared(lean_object * o) {
     if (LEAN_LIKELY(lean_is_st(o))) {
         return o->m_rc > 1;
@@ -1136,6 +1137,17 @@ static inline void * lean_get_external_data(lean_object * o) {
     return lean_to_external(o)->m_data;
 }
 
+static inline lean_object * lean_set_external_data(lean_object * o, void * data) {
+    if (lean_is_exclusive(o)) {
+        lean_to_external(o)->m_data = data;
+        return o;
+    } else {
+        lean_object * o_new = lean_alloc_external(lean_get_external_class(o), data);
+        lean_dec_ref(o);
+        return o_new;
+    }
+}
+
 /* Natural numbers */
 
 #define LEAN_MAX_SMALL_NAT (SIZE_MAX >> 1)

src/runtime/sharecommon.cpp

@@ -6,6 +6,8 @@ Author: Leonardo de Moura
 */
 #include <vector>
 #include <cstring>
+#include <unordered_map>
+#include <unordered_set>
 #include "runtime/object.h"
 #include "runtime/hash.h"
 
@@ -268,4 +270,177 @@ public:
 extern "C" LEAN_EXPORT obj_res lean_state_sharecommon(b_obj_arg tc, obj_arg s, obj_arg a) {
     return sharecommon_fn(tc, s)(a);
 }
+
+/*
+A faster version of `sharecommon_fn` which only uses a local state.
+It optimizes the number of RC operations, the strategy for caching results,
+and uses C++ hashmap.
+*/
+class sharecommon_quick_fn {
+    struct set_hash {
+        std::size_t operator()(lean_object * o) const { return lean_sharecommon_hash(o); }
+    };
+    struct set_eq {
+        std::size_t operator()(lean_object * o1, lean_object * o2) const { return lean_sharecommon_eq(o1, o2); }
+    };
+
+    /*
+    We use `m_cache` to ensure we do **not** traverse a DAG as a tree.
+    We use pointer equality for this collection.
+    */
+    std::unordered_map<lean_object *, lean_object *> m_cache;
+    /* Set of maximally shared terms. AKA hash-consing table. */
+    std::unordered_set<lean_object *, set_hash, set_eq> m_set;
+
+    /*
+      We do not increment reference counters when inserting Lean objects at `m_cache` and `m_set`.
+      This is correct because
+      - The domain of `m_cache` contains only sub-objects of `lean_sharecommon_quick` parameter,
+        and we know the object referenced by this parameter will remain alive.
+      - The range of `m_cache` contains only new objects that have been maxed shared, and these
+        objects will be are sub-objects of the object returned by `lean_sharecommon_quick`.
+      - `m_set` is like the range of `m_cache`.
+    */
+
+    lean_object * check_cache(lean_object * a) {
+        if (!lean_is_exclusive(a)) {
+            // We only check the cache if `a` is a shared object
+            auto it = m_cache.find(a);
+            if (it != m_cache.end()) {
+                // All objects stored in the range of `m_cache` are single threaded.
+                lean_assert(lean_is_st(it->second));
+                // We increment the reference counter because this object
+                // will be returned by `lean_sharecommon_quick` or stored into a new object.
+                it->second->m_rc++;
+                return it->second;
+            }
+        }
+        return nullptr;
+    }
+
+    /*
+    `new_a` is a new object that is equal to `a`, but its subobjects are maximally shared.
+    */
+    lean_object * save(lean_object * a, lean_object * new_a) {
+        lean_assert(lean_is_st(new_a));
+        lean_assert(new_a->m_rc == 1);
+        auto it = m_set.find(new_a);
+        lean_object * result;
+        if (it == m_set.end()) {
+            // `new_a` is a new object
+            m_set.insert(new_a);
+            result = new_a;
+        } else {
+            // We already have a maximally shared object that is equal to `new_a`
+            result = *it;
+            DEBUG_CODE({
+                    if (lean_is_ctor(new_a)) {
+                        lean_assert(lean_is_ctor(result));
+                        unsigned num_objs = lean_ctor_num_objs(new_a);
+                        lean_assert(lean_ctor_num_objs(result) == num_objs);
+                        for (unsigned i = 0; i < num_objs; i++) {
+                            lean_assert(lean_ctor_get(result, i) == lean_ctor_get(new_a, i));
+                        }
+                    }
+                });
+            lean_dec_ref(new_a); // delete `new_a`
+            // All objects in `m_set` are single threaded.
+            lean_assert(lean_is_st(result));
+            result->m_rc++;
+            lean_assert(result->m_rc > 1);
+        }
+        if (!lean_is_exclusive(a)) {
+            // We only cache the result if `a` is a shared object.
+            m_cache.insert(std::make_pair(a, result));
+        }
+        lean_assert(result == new_a || result->m_rc > 1);
+        lean_assert(result != new_a || result->m_rc == 1);
+        return result;
+    }
+
+    // `sarray` and `string`
+    lean_object * visit_terminal(lean_object * a) {
+        auto it = m_set.find(a);
+        if (it == m_set.end()) {
+            m_set.insert(a);
+        } else {
+            a = *it;
+        }
+        lean_inc_ref(a);
+        return a;
+    }
+
+    lean_object * visit_array(lean_object * a) {
+        lean_object * r = check_cache(a);
+        if (r != nullptr) { lean_assert(r->m_rc > 1); return r; }
+
+        size_t sz = array_size(a);
+        lean_array_object * new_a = (lean_array_object*)lean_alloc_array(sz, sz);
+        for (size_t i = 0; i < sz; i++) {
+            lean_array_set_core((lean_object*)new_a, i, visit(lean_array_get_core(a, i)));
+        }
+        return save(a, (lean_object*)new_a);
+    }
+
+    lean_object * visit_ctor(lean_object * a) {
+        lean_object * r = check_cache(a);
+        if (r != nullptr) { lean_assert(r->m_rc > 1); return r; }
+        unsigned num_objs      = lean_ctor_num_objs(a);
+        unsigned tag           = lean_ptr_tag(a);
+        unsigned sz            = lean_object_byte_size(a);
+        unsigned scalar_offset = sizeof(lean_object) + num_objs*sizeof(void*);
+        unsigned scalar_sz     = sz - scalar_offset;
+        lean_object * new_a    = lean_alloc_ctor(tag, num_objs, scalar_sz);
+        for (unsigned i = 0; i < num_objs; i++) {
+            lean_ctor_set(new_a, i, visit(lean_ctor_get(a, i)));
+        }
+        if (scalar_sz > 0) {
+            memcpy(reinterpret_cast<char*>(new_a) + scalar_offset, reinterpret_cast<char*>(a) + scalar_offset, scalar_sz);
+        }
+        return save(a, new_a);
+    }
+
+public:
+
+    /*
+    **TODO:** We did not implement stack overflow detection.
+    We claim it is not needed in the current uses of `shareCommon'`.
+    If this becomes an issue, we can use the following approach to address the issue without
+    affecting the performance.
+    - Add an extra `depth` parameter.
+    - In `operator()`, estimate the maximum depth based on the remaining stack space. See `check_stack`.
+    - If the limit is reached, simply return `a`.
+    */
+    lean_object * visit(lean_object * a) {
+        if (lean_is_scalar(a)) {
+            return a;
+        }
+        switch (lean_ptr_tag(a)) {
+        /*
+        Similarly to `sharecommon_fn`, we only maximally share arrays, scalar arrays, strings, and
+        constructor objects.
+        */
+        case LeanMPZ:             lean_inc_ref(a); return a;
+        case LeanClosure:         lean_inc_ref(a); return a;
+        case LeanThunk:           lean_inc_ref(a); return a;
+        case LeanTask:            lean_inc_ref(a); return a;
+        case LeanRef:             lean_inc_ref(a); return a;
+        case LeanExternal:        lean_inc_ref(a); return a;
+        case LeanReserved:        lean_inc_ref(a); return a;
+        case LeanScalarArray:     return visit_terminal(a);
+        case LeanString:          return visit_terminal(a);
+        case LeanArray:           return visit_array(a);
+        default:                  return visit_ctor(a);
+        }
+    }
+
+    lean_object * operator()(lean_object * a) {
+        return visit(a);
+    }
+};
+
+// def ShareCommon.shareCommon' (a : A) : A := a
+extern "C" LEAN_EXPORT obj_res lean_sharecommon_quick(obj_arg a) {
+    return sharecommon_quick_fn()(a);
+}
 };

tests/lean/348.lean.expected.out

@@ -1 +1 @@
-348.lean:3:24-3:25: error: unexpected token '⟩'; expected ')', ')ₘ' or ')ₚ'
+348.lean:3:24-3:25: error: unexpected token '⟩'; expected ')'

tests/lean/interactive/incrementalTactic.lean.expected.out

@@ -32,8 +32,7 @@ t 2
    "severity": 1,
    "range":
    {"start": {"line": 1, "character": 38}, "end": {"line": 4, "character": 3}},
-   "message":
-   "unexpected token '/-!'; expected ')', ')ₚ', '_', identifier or term",
+   "message": "unexpected token '/-!'; expected ')', '_', identifier or term",
    "fullRange":
    {"start": {"line": 1, "character": 38},
     "end": {"line": 4, "character": 3}}}]}

tests/lean/run/PProd_syntax.lean

@@ -0,0 +1,46 @@
+/-- info: Bool ×' Nat ×' List Unit : Type -/
+#guard_msgs in
+#check Bool ×' Nat ×' List Unit
+
+/-- info: Bool ×' Nat ×' List Unit : Type -/
+#guard_msgs in
+#check PProd Bool (PProd Nat (List Unit))
+
+/-- info: (Bool ×' Nat) ×' List Unit : Type -/
+#guard_msgs in
+#check PProd (PProd Bool Nat) (List Unit)
+
+/-- info: PUnit.{u} : Sort u -/
+#guard_msgs in
+#check PUnit
+
+/-- info: ⟨true, 5, [()]⟩ : Bool ×' Nat ×' List Unit -/
+#guard_msgs in
+#check (⟨true, 5, [()]⟩ : Bool ×' Nat ×' List Unit)
+
+/-- info: ⟨true, 5, [()]⟩ : MProd Bool (MProd Nat (List Unit)) -/
+#guard_msgs in
+#check (⟨true, 5, [()]⟩ : MProd Bool (MProd Nat (List Unit)))
+
+/-- info: ⟨true, 5, [()]⟩ : Bool ×' Nat ×' List Unit -/
+#guard_msgs in
+#check PProd.mk true (PProd.mk 5 [()])
+
+/-- info: ⟨true, 5, [()]⟩ : MProd Bool (MProd Nat (List Unit)) -/
+#guard_msgs in
+#check MProd.mk true (MProd.mk 5 [()])
+
+/-- info: PUnit.unit.{u} : PUnit -/
+#guard_msgs in
+#check PUnit.unit
+
+-- check that only `PProd` is flattened, not other structure
+
+@[pp_using_anonymous_constructor]
+structure TwoNats where
+  firstNat : Nat
+  secondNat : Nat
+
+/-- info: ⟨true, 5, ⟨23, 42⟩⟩ : Bool ×' Nat ×' TwoNats -/
+#guard_msgs in
+#check PProd.mk true (PProd.mk 5 (TwoNats.mk 23 42))

tests/lean/run/PUnit_syntax.lean

@@ -1,47 +0,0 @@
-/-- info: Bool ×ₚ Nat ×ₚ List Unit : Type -/
-#guard_msgs in
-#check Bool ×ₚ Nat ×ₚ List Unit
-
-/-- info: Bool ×ₚ Nat ×ₚ List Unit : Type -/
-#guard_msgs in
-#check PProd Bool (PProd Nat (List Unit))
-
-/-- info: (Bool ×ₚ Nat) ×ₚ List Unit : Type -/
-#guard_msgs in
-#check PProd (PProd Bool Nat) (List Unit)
-
-/-- info: Bool ×ₘ Nat ×ₘ List Unit : Type -/
-#guard_msgs in
-#check Bool ×ₘ Nat ×ₘ List Unit
-
-/-- info: Bool ×ₘ Nat ×ₘ List Unit : Type -/
-#guard_msgs in
-#check MProd Bool (MProd Nat (List Unit))
-
-/-- info: (Bool ×ₘ Nat) ×ₘ List Unit : Type -/
-#guard_msgs in
-#check MProd (MProd Bool Nat) (List Unit)
-
-/-- info: PUnit.unit : PUnit -/
-#guard_msgs in
-#check ()ₚ
-
-/-- info: (true, 5, [()])ₚ : Bool ×ₚ Nat ×ₚ List Unit -/
-#guard_msgs in
-#check (true, 5, [()])ₚ
-
-/-- info: (true, 5, [()])ₘ : Bool ×ₘ Nat ×ₘ List Unit -/
-#guard_msgs in
-#check (true, 5, [()])ₘ
-
-/-- info: (true, 5, [()])ₚ : Bool ×ₚ Nat ×ₚ List Unit -/
-#guard_msgs in
-#check PProd.mk true (PProd.mk 5 [()])
-
-/-- info: (true, 5, [()])ₘ : Bool ×ₘ Nat ×ₘ List Unit -/
-#guard_msgs in
-#check MProd.mk true (MProd.mk 5 [()])
-
-/-- info: PUnit.unit.{u} : PUnit -/
-#guard_msgs in
-#check PUnit.unit

tests/lean/run/array_simp.lean

@@ -0,0 +1,7 @@
+#check_simp #[1,2,3,4,5][2]  ~> 3
+#check_simp #[1,2,3,4,5][2]? ~> some 3
+#check_simp #[1,2,3,4,5][7]? ~> none
+#check_simp #[][0]? ~> none
+#check_simp #[1,2,3,4,5][2]! ~> 3
+#check_simp #[1,2,3,4,5][7]! ~> (default : Nat)
+#check_simp (#[] : Array Nat)[0]! ~> (default : Nat)

tests/lean/run/hashmap-implicits.lean

@@ -0,0 +1,71 @@
+import Std.Data.HashMap
+import Std.Data.HashSet
+import Std.Data.DHashMap
+
+open Std (DHashMap HashMap HashSet)
+
+/-! (Non-exhaustive) tests that `BEq` and `Hashable` arguments to query operations and lemmas are
+correctly solved by unification. -/
+
+namespace DHashMap
+
+structure A (α) extends BEq α, Hashable α where
+  foo : DHashMap α (fun _ => Nat)
+
+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 : α) : (@DHashMap.empty _ (fun _ => Nat) xs.toBEq xs.toHashable 5).contains x = false := by
+  rw [DHashMap.contains_empty]
+
+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 : α) [@LawfulBEq α xs.toBEq] : xs.foo.size ≤ (xs.foo.insert x 5).size :=
+  DHashMap.size_le_size_insert
+
+end DHashMap
+
+namespace HashMap
+
+structure A (α) extends BEq α, Hashable α where
+  foo : HashMap α Nat
+
+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 : α) : (@HashMap.empty _ Nat xs.toBEq xs.toHashable 5).contains x = false := by
+  rw [HashMap.contains_empty]
+
+example (xs : A α) (x : α) : (@HashMap.empty _ Nat xs.toBEq xs.toHashable 5)[x]? = none := by
+  rw [HashMap.getElem?_empty]
+
+example (xs : A α) (x : α) [@LawfulBEq α xs.toBEq] : xs.foo.size ≤ (xs.foo.insert x 5).size :=
+  HashMap.size_le_size_insert
+
+end HashMap
+
+namespace HashSet
+
+structure A (α) extends BEq α, Hashable α where
+  foo : HashSet α
+
+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 : α) : (@HashSet.empty _ xs.toBEq xs.toHashable 5).contains x = false := by
+  rw [HashSet.contains_empty]
+
+example (xs : A α) (x : α) [@LawfulBEq α xs.toBEq] : xs.foo.size ≤ (xs.foo.insert x).size :=
+  HashSet.size_le_size_insert
+
+end HashSet

tests/lean/trailingComma.lean.expected.out

@@ -1,4 +1,4 @@
 [1, 2, 3]
 (2, 3)
 trailingComma.lean:6:13-6:14: error: unexpected token ','; expected ']'
-trailingComma.lean:7:11-7:12: error: unexpected token ','; expected ')', ')ₘ' or ')ₚ'
+trailingComma.lean:7:11-7:12: error: unexpected token ','; expected ')'