initial exploration for a ExtHashMapD

This PR corrects some `Array` lemmas to be about `Array` not `List`.

Discovered [on
Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/duplicate.20declarations/near/518942094)

src/Init/Data/Array/Lex/Lemmas.lean

@@ -23,9 +23,9 @@ namespace Array
 @[simp, grind =] theorem lt_toList [LT α] {xs ys : Array α} : xs.toList < ys.toList ↔ xs < ys := Iff.rfl
 @[simp, grind =] theorem le_toList [LT α] {xs ys : Array α} : xs.toList ≤ ys.toList ↔ xs ≤ ys := Iff.rfl
 
-protected theorem not_lt_iff_ge [LT α] {l₁ l₂ : List α} : ¬ l₁ < l₂ ↔ l₂ ≤ l₁ := Iff.rfl
-protected theorem not_le_iff_gt [DecidableEq α] [LT α] [DecidableLT α] {l₁ l₂ : List α} :
-    ¬ l₁ ≤ l₂ ↔ l₂ < l₁ :=
+protected theorem not_lt_iff_ge [LT α] {xs ys : Array α} : ¬ xs < ys ↔ ys ≤ xs := Iff.rfl
+protected theorem not_le_iff_gt [DecidableEq α] [LT α] [DecidableLT α] {xs ys : Array α} :
+    ¬ xs ≤ ys ↔ ys < xs :=
   Decidable.not_not
 
 @[simp] theorem lex_empty [BEq α] {lt : α → α → Bool} {xs : Array α} : xs.lex #[] lt = false := by

src/Init/Grind.lean

@@ -15,5 +15,4 @@ import Init.Grind.Util
 import Init.Grind.Offset
 import Init.Grind.PP
 import Init.Grind.CommRing
-import Init.Grind.Module
 import Init.Grind.Ext

src/Init/Grind/Module.lean

@@ -1,10 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kim Morrison
--/
-module
-
-prelude
-import Init.Grind.Module.Basic
-import Init.Grind.Module.Int

src/Init/Grind/Module/Basic.lean

@@ -1,72 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kim Morrison
--/
-module
-
-prelude
-import Init.Data.Int.Order
-
-namespace Lean.Grind
-
-class NatModule (M : Type u) extends Zero M, Add M, HSMul Nat M M where
-  add_zero : ∀ a : M, a + 0 = a
-  zero_add : ∀ a : M, 0 + a = a
-  add_comm : ∀ a b : M, a + b = b + a
-  add_assoc : ∀ a b c : M, a + b + c = a + (b + c)
-  zero_smul : ∀ a : M, 0 • a = 0
-  one_smul : ∀ a : M, 1 • a = a
-  add_smul : ∀ n m : Nat, ∀ a : M, (n + m) • a = n • a + m • a
-  smul_zero : ∀ n : Nat, n • (0 : M) = 0
-  smul_add : ∀ n : Nat, ∀ a b : M, n • (a + b) = n • a + n • b
-  mul_smul : ∀ n m : Nat, ∀ a : M, (n * m) • a = n • (m • a)
-
-class IntModule (M : Type u) extends Zero M, Add M, Neg M, Sub M, HSMul Int M M where
-  add_zero : ∀ a : M, a + 0 = a
-  zero_add : ∀ a : M, 0 + a = a
-  add_comm : ∀ a b : M, a + b = b + a
-  add_assoc : ∀ a b c : M, a + b + c = a + (b + c)
-  zero_smul : ∀ a : M, (0 : Int) • a = 0
-  one_smul : ∀ a : M, (1 : Int) • a = a
-  add_smul : ∀ n m : Int, ∀ a : M, (n + m) • a = n • a + m • a
-  neg_smul : ∀ n : Int, ∀ a : M, (-n) • a = - (n • a)
-  smul_zero : ∀ n : Int, n • (0 : M) = 0
-  smul_add : ∀ n : Int, ∀ a b : M, n • (a + b) = n • a + n • b
-  mul_smul : ∀ n m : Int, ∀ a : M, (n * m) • a = n • (m • a)
-  neg_add_cancel : ∀ a : M, -a + a = 0
-  sub_eq_add_neg : ∀ a b : M, a - b = a + -b
-
-instance IntModule.toNatModule (M : Type u) [i : IntModule M] : NatModule M :=
-  { i with
-    hSMul a x := (a : Int) • x
-    smul_zero := by simp [IntModule.smul_zero]
-    add_smul := by simp [IntModule.add_smul]
-    smul_add := by simp [IntModule.smul_add]
-    mul_smul := by simp [IntModule.mul_smul] }
-
-/--
-We keep track of rational linear combinations as integer linear combinations,
-but with the assurance that we can cancel the GCD of the coefficients.
--/
-class RatModule (M : Type u) extends IntModule M where
-  no_int_zero_divisors : ∀ (k : Int) (a : M), k ≠ 0 → k • a = 0 → a = 0
-
-/-- A preorder is a reflexive, transitive relation `≤` with `a < b` defined in the obvious way. -/
-class Preorder (α : Type u) extends LE α, LT α where
-  le_refl : ∀ a : α, a ≤ a
-  le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c
-  lt := fun a b => a ≤ b ∧ ¬b ≤ a
-  lt_iff_le_not_le : ∀ a b : α, a < b ↔ a ≤ b ∧ ¬b ≤ a := by intros; rfl
-
-class IntModule.IsOrdered (M : Type u) [Preorder M] [IntModule M] where
-  neg_le_iff : ∀ a b : M, -a ≤ b ↔ -b ≤ a
-  neg_lt_iff : ∀ a b : M, -a < b ↔ -b < a
-  add_lt_left : ∀ a b c : M, a < b → a + c < b + c
-  add_lt_right : ∀ a b c : M, a < b → c + a < c + b
-  smul_pos : ∀ (k : Int) (a : M), 0 < a → (0 < k ↔ 0 < k • a)
-  smul_neg : ∀ (k : Int) (a : M), a < 0 → (0 < k ↔ k • a < 0)
-  smul_nonneg : ∀ (k : Int) (a : M), 0 ≤ a → 0 ≤ k → 0 ≤ k • a
-  smul_nonpos : ∀ (k : Int) (a : M), a ≤ 0 → 0 ≤ k → k • a ≤ 0
-
-end Lean.Grind

src/Init/Grind/Module/Int.lean

@@ -1,48 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kim Morrison
--/
-module
-
-prelude
-import Init.Grind.Module.Basic
-import Init.Omega
-
-/-!
-# `grind` instances for `Int` as an ordered module.
--/
-
-namespace Lean.Grind
-
-instance : IntModule Int where
-  add_zero := Int.add_zero
-  zero_add := Int.zero_add
-  add_comm := Int.add_comm
-  add_assoc := Int.add_assoc
-  zero_smul := Int.zero_mul
-  one_smul := Int.one_mul
-  add_smul := Int.add_mul
-  neg_smul := Int.neg_mul
-  smul_zero := Int.mul_zero
-  smul_add := Int.mul_add
-  mul_smul := Int.mul_assoc
-  neg_add_cancel := Int.add_left_neg
-  sub_eq_add_neg _ _ := Int.sub_eq_add_neg
-
-instance : Preorder Int where
-  le_refl := Int.le_refl
-  le_trans _ _ _ := Int.le_trans
-  lt_iff_le_not_le := by omega
-
-instance : IntModule.IsOrdered Int where
-  neg_le_iff := by omega
-  neg_lt_iff := by omega
-  add_lt_left := by omega
-  add_lt_right := by omega
-  smul_pos k a ha := ⟨fun hk => Int.mul_pos hk ha, fun h => Int.pos_of_mul_pos_left h ha⟩
-  smul_neg k a ha := ⟨fun hk => Int.mul_neg_of_pos_of_neg hk ha, fun h => Int.pos_of_mul_neg_left h ha⟩
-  smul_nonpos k a ha hk := Int.mul_nonpos_of_nonneg_of_nonpos hk ha
-  smul_nonneg k a ha hk := Int.mul_nonneg hk ha
-
-end Lean.Grind

src/Init/Notation.lean

@@ -295,7 +295,6 @@ recommended_spelling "PProd" for "×'" in [PProd, «term_×'_»]
 @[inherit_doc] prefix:75 "-"     => Neg.neg
 @[inherit_doc] prefix:100 "~~~"  => Complement.complement
 @[inherit_doc] postfix:max "⁻¹"  => Inv.inv
-@[inherit_doc] infixr:73 " • " => HSMul.hSMul
 
 /-!
   Remark: the infix commands above ensure a delaborator is generated for each relations.
@@ -313,40 +312,6 @@ macro_rules | `($x % $y)   => `(binop% HMod.hMod $x $y)
 macro_rules | `($x ^ $y)   => `(rightact% HPow.hPow $x $y)
 macro_rules | `($x ++ $y)  => `(binop% HAppend.hAppend $x $y)
 macro_rules | `(- $x)      => `(unop% Neg.neg $x)
-/-!
-We have a macro to make `x • y` notation participate in the expression tree elaborator,
-like other arithmetic expressions such as `+`, `*`, `/`, `^`, `=`, inequalities, etc.
-The macro is using the `leftact%` elaborator introduced in
-[this RFC](https://github.com/leanprover/lean4/issues/2854).
-
-As a concrete example of the effect of this macro, consider
-```lean
-variable [Ring R] [AddCommMonoid M] [Module R M] (r : R) (N : Submodule R M) (m : M) (n : N)
-#check m + r • n
-```
-Without the macro, the expression would elaborate as `m + ↑(r • n : ↑N) : M`.
-With the macro, the expression elaborates as `m + r • (↑n : M) : M`.
-To get the first interpretation, one can write `m + (r • n :)`.
-
-Here is a quick review of the expression tree elaborator:
-1. It builds up an expression tree of all the immediately accessible operations
-   that are marked with `binop%`, `unop%`, `leftact%`, `rightact%`, `binrel%`, etc.
-2. It elaborates every leaf term of this tree
-   (without an expected type, so as if it were temporarily wrapped in `(... :)`).
-3. Using the types of each elaborated leaf, it computes a supremum type they can all be
-   coerced to, if such a supremum exists.
-4. It inserts coercions around leaf terms wherever needed.
-
-The hypothesis is that individual expression trees tend to be calculations with respect
-to a single algebraic structure.
-
-Note(kmill): If we were to remove `HSMul` and switch to using `SMul` directly,
-then the expression tree elaborator would not be able to insert coercions within the right operand;
-they would likely appear as `↑(x • y)` rather than `x • ↑y`, unlike other arithmetic operations.
--/
-
-@[inherit_doc HSMul.hSMul]
-macro_rules | `($x • $y) => `(leftact% HSMul.hSMul $x $y)
 
 recommended_spelling "or" for "|||" in [HOr.hOr, «term_|||_»]
 recommended_spelling "xor" for "^^^" in [HXor.hXor, «term_^^^_»]
@@ -358,7 +323,6 @@ recommended_spelling "mul" for "*" in [HMul.hMul, «term_*_»]
 recommended_spelling "div" for "/" in [HDiv.hDiv, «term_/_»]
 recommended_spelling "mod" for "%" in [HMod.hMod, «term_%_»]
 recommended_spelling "pow" for "^" in [HPow.hPow, «term_^_»]
-recommended_spelling "smul" for "•" in [HSMul.hSMul, «term_•_»]
 recommended_spelling "append" for "++" in [HAppend.hAppend, «term_++_»]
 /-- when used as a unary operator -/
 recommended_spelling "neg" for "-" in [Neg.neg, «term-_»]

src/Init/Prelude.lean

@@ -1348,23 +1348,6 @@ class HPow (α : Type u) (β : Type v) (γ : outParam (Type w)) where
   The meaning of this notation is type-dependent. -/
   hPow : α → β → γ
 
-/--
-The notation typeclass for heterogeneous scalar multiplication.
-This enables the notation `a • b : γ` where `a : α`, `b : β`.
-
-It is assumed to represent a left action in some sense.
-The notation `a • b` is augmented with a macro (below) to have it elaborate as a left action.
-Only the `b` argument participates in the elaboration algorithm: the algorithm uses the type of `b`
-when calculating the type of the surrounding arithmetic expression
-and it tries to insert coercions into `b` to get some `b'`
-such that `a • b'` has the same type as `b'`.
-See the module documentation near the macro for more details.
--/
-class HSMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where
-  /-- `a • b` computes the product of `a` and `b`.
-  The meaning of this notation is type-dependent, but it is intended to be used for left actions. -/
-  hSMul : α → β → γ
-
 /--
 The notation typeclass for heterogeneous append.
 This enables the notation `a ++ b : γ` where `a : α`, `b : β`.
@@ -1527,12 +1510,6 @@ class HomogeneousPow (α : Type u) where
   /-- `a ^ b` computes `a` to the power of `b` where `a` and `b` both have the same type. -/
   protected pow : α → α → α
 
-/-- Typeclass for types with a scalar multiplication operation, denoted `•` (`\bu`) -/
-class SMul (M : Type u) (α : Type v) where
-  /-- `a • b` computes the product of `a` and `b`. The meaning of this notation is type-dependent,
-  but it is intended to be used for left actions. -/
-  smul : M → α → α
-
 /-- The homogeneous version of `HAppend`: `a ++ b : α` where `a b : α`. -/
 class Append (α : Type u) where
   /-- `a ++ b` is the result of concatenation of `a` and `b`. See `HAppend`. -/
@@ -1624,13 +1601,6 @@ instance instPowNat [NatPow α] : Pow α Nat where
 instance [HomogeneousPow α] : Pow α α where
   pow a b := HomogeneousPow.pow a b
 
-@[default_instance]
-instance instHSMul {α β} [SMul α β] : HSMul α β β where
-  hSMul := SMul.smul
-
-instance (priority := 910) {α : Type u} [Mul α] : SMul α α where
-  smul x y := Mul.mul x y
-
 @[default_instance]
 instance [Append α] : HAppend α α α where
   hAppend a b := Append.append a b

src/Lean/Compiler/IR/ToIR.lean

@@ -65,8 +65,8 @@ def addDecl (d : Decl) : M Unit :=
 
 def lowerLitValue (v : LCNF.LitValue) : LitVal :=
   match v with
-  | .natVal n => .num n
-  | .strVal s => .str s
+  | .nat n => .num n
+  | .str s => .str s
 
 -- TODO: This should be cached.
 def lowerEnumToScalarType (name : Name) : M (Option IRType) := do
@@ -224,7 +224,7 @@ partial def lowerLet (decl : LCNF.LetDecl) (k : LCNF.Code) : M FnBody := do
       return none
 
   match decl.value with
-  | .value litValue =>
+  | .lit litValue =>
     mkExpr (.lit (lowerLitValue litValue))
   | .proj typeName i fvarId =>
     match (← get).fvars[fvarId]? with

src/Lean/Compiler/LCNF/AlphaEqv.lean

@@ -54,7 +54,7 @@ def eqvArgs (as₁ as₂ : Array Arg) : EqvM Bool := do
 
 def eqvLetValue (e₁ e₂ : LetValue) : EqvM Bool := do
   match e₁, e₂ with
-  | .value v₁, .value v₂ => return v₁ == v₂
+  | .lit v₁, .lit v₂ => return v₁ == v₂
   | .erased, .erased => return true
   | .proj s₁ i₁ x₁, .proj s₂ i₂ x₂ => pure (s₁ == s₂ && i₁ == i₂) <&&> eqvFVar x₁ x₂
   | .const n₁ us₁ as₁, .const n₂ us₂ as₂ => pure (n₁ == n₂ && us₁ == us₂) <&&> eqvArgs as₁ as₂

src/Lean/Compiler/LCNF/Basic.lean

@@ -34,14 +34,14 @@ def Param.toExpr (p : Param) : Expr :=
   .fvar p.fvarId
 
 inductive LitValue where
-  | natVal (val : Nat)
-  | strVal (val : String)
+  | nat (val : Nat)
+  | str (val : String)
   -- TODO: add constructors for `Int`, `Float`, `UInt` ...
   deriving Inhabited, BEq, Hashable
 
 def LitValue.toExpr : LitValue → Expr
-  | .natVal v => .lit (.natVal v)
-  | .strVal v => .lit (.strVal v)
+  | .nat v => .lit (.natVal v)
+  | .str v => .lit (.strVal v)
 
 inductive Arg where
   | erased
@@ -73,7 +73,7 @@ private unsafe def Arg.updateFVarImp (arg : Arg) (fvarId' : FVarId) : Arg :=
 @[implemented_by Arg.updateFVarImp] opaque Arg.updateFVar! (arg : Arg) (fvarId' : FVarId) : Arg
 
 inductive LetValue where
-  | value (value : LitValue)
+  | lit (value : LitValue)
   | erased
   | proj (typeName : Name) (idx : Nat) (struct : FVarId)
   | const (declName : Name) (us : List Level) (args : Array Arg)
@@ -117,8 +117,7 @@ private unsafe def LetValue.updateArgsImp (e : LetValue) (args' : Array Arg) : L
 
 def LetValue.toExpr (e : LetValue) : Expr :=
   match e with
-  | .value (.natVal val) => .lit (.natVal val)
-  | .value (.strVal val) => .lit (.strVal val)
+  | .lit v => v.toExpr
   | .erased => erasedExpr
   | .proj n i s => .proj n i (.fvar s)
   | .const n us as => mkAppN (.const n us) (as.map Arg.toExpr)
@@ -457,7 +456,7 @@ where
     match e with
     | .const declName vs args => e.updateConst! declName (vs.mapMono instLevel) (args.mapMono instArg)
     | .fvar fvarId args => e.updateFVar! fvarId (args.mapMono instArg)
-    | .proj .. | .value .. | .erased => e
+    | .proj .. | .lit .. | .erased => e
 
   instLetDecl (decl : LetDecl) :=
     decl.updateCore (instExpr decl.type) (instLetValue decl.value)
@@ -673,7 +672,7 @@ private def collectLetValue (e : LetValue) (s : FVarIdSet) : FVarIdSet :=
   | .fvar fvarId args => collectArgs args <| s.insert fvarId
   | .const _ _ args => collectArgs args s
   | .proj _ _ fvarId => s.insert fvarId
-  | .value .. | .erased => s
+  | .lit .. | .erased => s
 
 private partial def collectParams (ps : Array Param) (s : FVarIdSet) : FVarIdSet :=
   ps.foldl (init := s) fun s p => collectType p.type s

src/Lean/Compiler/LCNF/Check.lean

@@ -140,7 +140,7 @@ def checkAppArgs (f : Expr) (args : Array Arg) : CheckM Unit := do
 
 def checkLetValue (e : LetValue) : CheckM Unit := do
   match e with
-  | .value .. | .erased => pure ()
+  | .lit .. | .erased => pure ()
   | .const declName us args => checkAppArgs (mkConst declName us) args
   | .fvar fvarId args => checkFVar fvarId; checkAppArgs (.fvar fvarId) args
   | .proj _ _ fvarId => checkFVar fvarId

src/Lean/Compiler/LCNF/Closure.lean

@@ -86,7 +86,7 @@ mutual
 
   partial def collectLetValue (e : LetValue) : ClosureM Unit := do
     match e with
-    | .erased | .value .. => return ()
+    | .erased | .lit .. => return ()
     | .proj _ _ fvarId => collectFVar fvarId
     | .const _ _ args => args.forM collectArg
     | .fvar fvarId args => collectFVar fvarId; args.forM collectArg

src/Lean/Compiler/LCNF/CompilerM.lean

@@ -264,7 +264,7 @@ See `normExprImp`
 -/
 private partial def normLetValueImp (s : FVarSubst) (e : LetValue) (translator : Bool) : LetValue :=
   match e with
-  | .erased | .value .. => e
+  | .erased | .lit .. => e
   | .proj _ _ fvarId => match normFVarImp s fvarId translator with
     | .fvar fvarId' => e.updateProj! fvarId'
     | .erased => .erased

src/Lean/Compiler/LCNF/DependsOn.lean

@@ -25,7 +25,7 @@ private def argDepOn (a : Arg) : M Bool := do
 
 private def letValueDepOn (e : LetValue) : M Bool :=
   match e with
-  | .erased | .value .. => return false
+  | .erased | .lit .. => return false
   | .proj _ _ fvarId => fvarDepOn fvarId
   | .fvar fvarId args => fvarDepOn fvarId <||> args.anyM argDepOn
   | .const _ _ args => args.anyM argDepOn

src/Lean/Compiler/LCNF/ElimDead.lean

@@ -37,7 +37,7 @@ def collectLocalDeclsArgs (s : UsedLocalDecls) (args : Array Arg) : UsedLocalDec
 
 def collectLocalDeclsLetValue (s : UsedLocalDecls) (e : LetValue) : UsedLocalDecls :=
   match e with
-  | .erased  | .value .. => s
+  | .erased  | .lit .. => s
   | .proj _ _ fvarId => s.insert fvarId
   | .const _ _ args => collectLocalDeclsArgs s args
   | .fvar fvarId args => collectLocalDeclsArgs (s.insert fvarId) args

src/Lean/Compiler/LCNF/ElimDeadBranches.lean

@@ -171,9 +171,9 @@ where
   | n + 1 => .ctor ``Nat.succ #[goSmall n]
 
 def ofLCNFLit : LCNF.LitValue → Value
-| .natVal n => ofNat n
+| .nat n => ofNat n
 -- TODO: We could make this much more precise but the payoff is questionable
-| .strVal .. => .top
+| .str .. => .top
 
 partial def proj : Value → Nat → Value
 | .ctor _ vs , i => vs.getD i bot
@@ -206,11 +206,11 @@ partial def getLiteral (v : Value) : CompilerM (Option ((Array CodeDecl) × FVar
 where
   go : Value → CompilerM ((Array CodeDecl) × FVarId)
   | .ctor `Nat.zero #[] .. => do
-    let decl ← mkAuxLetDecl <| .value <| .natVal <| 0
+    let decl ← mkAuxLetDecl <| .lit <| .nat <| 0
     return (#[.let decl], decl.fvarId)
   | .ctor `Nat.succ #[val] .. => do
     let val := getNatConstant val + 1
-    let decl ← mkAuxLetDecl <| .value <| .natVal <| val
+    let decl ← mkAuxLetDecl <| .lit <| .nat <| val
     return (#[.let decl], decl.fvarId)
   | .ctor i vs => do
     let args ← vs.mapM go
@@ -456,7 +456,7 @@ where
   -/
   interpLetValue (letVal : LetValue) : InterpM Value := do
     match letVal with
-    | .value val => return .ofLCNFLit val
+    | .lit val => return .ofLCNFLit val
     | .proj _ idx struct => return (← findVarValue struct).proj idx
     | .const declName _ args =>
       let env ← getEnv

src/Lean/Compiler/LCNF/FVarUtil.lean

@@ -64,14 +64,14 @@ instance : TraverseFVar Arg where
 
 def LetValue.mapFVarM [MonadLiftT CompilerM m] [Monad m] (f : FVarId → m FVarId) (e : LetValue) : m LetValue := do
   match e with
-  | .value .. | .erased => return e
+  | .lit .. | .erased => return e
   | .proj _ _ fvarId => return e.updateProj! (← f fvarId)
   | .const _ _ args => return e.updateArgs! (← args.mapM (TraverseFVar.mapFVarM f))
   | .fvar fvarId args => return e.updateFVar! (← f fvarId) (← args.mapM (TraverseFVar.mapFVarM f))
 
 def LetValue.forFVarM [Monad m] (f : FVarId → m Unit) (e : LetValue) : m Unit := do
   match e with
-  | .value .. | .erased => return ()
+  | .lit .. | .erased => return ()
   | .proj _ _ fvarId => f fvarId
   | .const _ _ args => args.forM (TraverseFVar.forFVarM f)
   | .fvar fvarId args => f fvarId; args.forM (TraverseFVar.forFVarM f)

src/Lean/Compiler/LCNF/InferType.lean

@@ -103,8 +103,8 @@ def inferConstType (declName : Name) (us : List Level) : CompilerM Expr := do
 
 def inferLitValueType (value : LitValue) : Expr :=
   match value with
-  | .natVal .. => mkConst ``Nat
-  | .strVal .. => mkConst ``String
+  | .nat .. => mkConst ``Nat
+  | .str .. => mkConst ``String
 
 mutual
   partial def inferArgType (arg : Arg) : InferTypeM Expr :=
@@ -126,7 +126,7 @@ mutual
   partial def inferLetValueType (e : LetValue) : InferTypeM Expr := do
     match e with
     | .erased => return erasedExpr
-    | .value v => return inferLitValueType v
+    | .lit v => return inferLitValueType v
     | .proj structName idx fvarId => inferProjType structName idx fvarId
     | .const declName us args => inferAppTypeCore (← inferConstType declName us) args
     | .fvar fvarId args => inferAppTypeCore (← getType fvarId) args

src/Lean/Compiler/LCNF/Level.lean

@@ -111,7 +111,7 @@ def visitArgs (args : Array Arg) : Visitor :=
 
 def visitLetValue (e : LetValue) : Visitor :=
   match e with
-  | .erased | .value .. | .proj .. => id
+  | .erased | .lit .. | .proj .. => id
   | .const _ us args => visitLevels us ∘ visitArgs args
   | .fvar _ args => visitArgs args
 

src/Lean/Compiler/LCNF/PrettyPrinter.lean

@@ -59,7 +59,7 @@ def ppArgs (args : Array Arg) : M Format := do
 def ppLetValue (e : LetValue) : M Format := do
   match e with
   | .erased => return "◾"
-  | .value v => ppExpr v.toExpr
+  | .lit v => ppExpr v.toExpr
   | .proj _ i fvarId => return f!"{← ppFVar fvarId} # {i}"
   | .fvar fvarId args => return f!"{← ppFVar fvarId}{← ppArgs args}"
   | .const declName us args => return f!"{← ppExpr (.const declName us)}{← ppArgs args}"

src/Lean/Compiler/LCNF/ReduceArity.lean

@@ -70,7 +70,7 @@ def visitArg (arg : Arg) : FindUsedM Unit := do
 
 def visitLetValue (e : LetValue) : FindUsedM Unit := do
   match e with
-  | .erased | .value .. => return ()
+  | .erased | .lit .. => return ()
   | .proj _ _ fvarId => visitFVar fvarId
   | .fvar fvarId args => visitFVar fvarId; args.forM visitArg
   | .const declName _ args =>

src/Lean/Compiler/LCNF/Simp/ConstantFold.lean

@@ -64,22 +64,22 @@ def mkAuxLit [Literal α] (x : α) (prefixName := `_x) : FolderM FVarId := do
   mkAuxLetDecl lit prefixName
 
 partial def getNatLit (fvarId : FVarId) : CompilerM (Option Nat) := do
-  let some (.value (.natVal n)) ← findLetValue? fvarId | return none
+  let some (.lit (.nat n)) ← findLetValue? fvarId | return none
   return n
 
 def mkNatLit (n : Nat) : FolderM LetValue :=
-  return .value (.natVal n)
+  return .lit (.nat n)
 
 instance : Literal Nat where
   getLit := getNatLit
   mkLit := mkNatLit
 
 def getStringLit (fvarId : FVarId) : CompilerM (Option String) := do
-  let some (.value (.strVal s)) ← findLetValue? fvarId | return none
+  let some (.lit (.str s)) ← findLetValue? fvarId | return none
   return s
 
 def mkStringLit (n : String) : FolderM LetValue :=
-  return .value (.strVal n)
+  return .lit (.str n)
 
 instance : Literal String where
   getLit := getStringLit

src/Lean/Compiler/LCNF/Simp/DiscrM.lean

@@ -54,7 +54,7 @@ Remark: We use this method when simplifying projections and cases-constructor.
 -/
 def findCtor? (fvarId : FVarId) : DiscrM (Option CtorInfo) := do
   match (← findLetDecl? fvarId) with
-  | some { value := .value (.natVal n), .. } =>
+  | some { value := .lit (.nat n), .. } =>
     return some <| .natVal n
   | some { value := .const declName _ args, .. } =>
     let some (.ctorInfo val) := (← getEnv).find? declName | return none

src/Lean/Compiler/LCNF/Simp/FunDeclInfo.lean

@@ -103,7 +103,7 @@ where
 
   addLetValueOccs (e : LetValue) : StateRefT FunDeclInfoMap CompilerM Unit := do
     match e with
-    | .erased | .value .. | .proj .. => return ()
+    | .erased | .lit .. | .proj .. => return ()
     | .const _ _ args => args.forM addArgOcc
     | .fvar fvarId args =>
       let some funDecl ← findFunDecl'? fvarId | return ()

src/Lean/Compiler/LCNF/Simp/InlineProj.lean

@@ -52,7 +52,7 @@ where
     let some letDecl ← findLetDecl? fvarId | failure
     match letDecl.value with
     | .proj _ i s => visit s (i :: projs)
-    | .fvar .. | .value .. | .erased => failure
+    | .fvar .. | .lit .. | .erased => failure
     | .const declName us args =>
       if let some (.ctorInfo ctorVal) := (← getEnv).find? declName then
         let i :: projs := projs | unreachable!

src/Lean/Compiler/LCNF/Simp/JpCases.lean

@@ -290,7 +290,7 @@ where
         let argsNew := mkJmpNewArgs args info.paramIdx #[] jpAlt.dependsOnDiscr
         return some <| .jmp jpAlt.decl.fvarId argsNew
       | .natVal (n+1) =>
-        let auxDecl ← mkAuxLetDecl (.value (.natVal n))
+        let auxDecl ← mkAuxLetDecl (.lit (.nat n))
         let argsNew := mkJmpNewArgs args info.paramIdx #[.fvar auxDecl.fvarId] jpAlt.dependsOnDiscr
         return some <| .let auxDecl (.jmp jpAlt.decl.fvarId argsNew)
 

src/Lean/Compiler/LCNF/Simp/Main.lean

@@ -207,7 +207,7 @@ partial def simpCasesOnCtor? (cases : Cases) : SimpM (Option Code) := do
         return k
       | .natVal 0 => simp k
       | .natVal (n+1) =>
-        let auxDecl ← mkAuxLetDecl (.value (.natVal n))
+        let auxDecl ← mkAuxLetDecl (.lit (.nat n))
         addFVarSubst params[0]!.fvarId auxDecl.fvarId
         let k ← simp k
         eraseParams params

src/Lean/Compiler/LCNF/Simp/SimpValue.lean

@@ -37,7 +37,7 @@ def simpAppApp? (e : LetValue) : OptionT SimpM LetValue := do
     return .fvar f (args' ++ args)
   | .const declName us args' => return .const declName us (args' ++ args)
   | .erased => return .erased
-  | .proj .. | .value .. => failure
+  | .proj .. | .lit .. => failure
 
 def simpCtorDiscr? (e : LetValue) : OptionT SimpM LetValue := do
   let .const declName _ _ := e | failure

src/Lean/Compiler/LCNF/Simp/Used.lean

@@ -37,7 +37,7 @@ Mark all free variables occurring in `e` as used.
 -/
 def markUsedLetValue (e : LetValue) : SimpM Unit := do
   match e with
-  | .value .. | .erased => return ()
+  | .lit .. | .erased => return ()
   | .proj _ _ fvarId => markUsedFVar fvarId
   | .const _ _ args => args.forM markUsedArg
   | .fvar fvarId args => markUsedFVar fvarId; args.forM markUsedArg

src/Lean/Compiler/LCNF/StructProjCases.lean

@@ -105,7 +105,7 @@ partial def visitLetValue (v : LetValue) : M LetValue := do
     return v.updateArgs! (← args.mapM visitArg)
   | .fvar fvarId args =>
     return v.updateFVar! (← remapFVar fvarId) (← args.mapM visitArg)
-  | .value _ | .erased => return v
+  | .lit _ | .erased => return v
   -- Projections should be handled directly by `visitCode`.
   | .proj .. => unreachable!
 

src/Lean/Compiler/LCNF/Testing.lean

@@ -27,7 +27,7 @@ where
     | _ => false
   goLetValue (l : LetValue) : Bool :=
     match l with
-    | .value .. | .erased | .proj .. | .fvar .. => false
+    | .lit .. | .erased | .proj .. | .fvar .. => false
     | .const name .. => name == constName
 
 namespace Testing

src/Lean/Compiler/LCNF/ToLCNF.lean

@@ -407,8 +407,8 @@ partial def etaReduceImplicit (e : Expr) : Expr :=
 
 def litToValue (lit : Literal) : LitValue :=
   match lit with
-  | .natVal val => .natVal val
-  | .strVal val => .strVal val
+  | .natVal val => .nat val
+  | .strVal val => .str val
 
 /--
 Put the given expression in `LCNF`.
@@ -453,7 +453,7 @@ where
     visitCore e
 
   visitLit (lit : Literal) : M Arg :=
-    letValueToArg (.value (litToValue lit))
+    letValueToArg (.lit (litToValue lit))
 
   visitAppArg (e : Expr) : M Arg := do
     if isLCProof e then

src/Lean/Compiler/LCNF/ToMono.lean

@@ -44,7 +44,7 @@ def ctorAppToMono (ctorInfo : ConstructorVal) (args : Array Arg) : ToMonoM LetVa
 
 partial def LetValue.toMono (e : LetValue) : ToMonoM LetValue := do
   match e with
-  | .erased | .value .. => return e
+  | .erased | .lit .. => return e
   | .const declName _ args =>
     if declName == ``Decidable.isTrue then
       return .const ``Bool.true [] #[]
@@ -105,7 +105,7 @@ partial def decToMono (c : Cases) (_ : c.typeName == ``Decidable) : ToMonoM Code
 partial def casesNatToMono (c: Cases) (_ : c.typeName == ``Nat) : ToMonoM Code := do
   let resultType ← toMonoType c.resultType
   let natType := mkConst ``Nat
-  let zeroDecl ← mkLetDecl `zero natType (.value (.natVal 0))
+  let zeroDecl ← mkLetDecl `zero natType (.lit (.nat 0))
   let isZeroDecl ← mkLetDecl `isZero (mkConst ``Bool) (.const ``Nat.decEq [] #[.fvar c.discr, .fvar zeroDecl.fvarId])
   let alts ← c.alts.mapM fun alt => do
     match alt with
@@ -114,7 +114,7 @@ partial def casesNatToMono (c: Cases) (_ : c.typeName == ``Nat) : ToMonoM Code :
       eraseParams ps
       if ctorName == ``Nat.succ then
         let p := ps[0]!
-        let oneDecl ← mkLetDecl `one natType (.value (.natVal 1))
+        let oneDecl ← mkLetDecl `one natType (.lit (.nat 1))
         let subOneDecl := { fvarId := p.fvarId, binderName := p.binderName, type := natType, value := .const ``Nat.sub [] #[.fvar c.discr, .fvar oneDecl.fvarId] }
         modifyLCtx fun lctx => lctx.addLetDecl subOneDecl
         return .alt ``Bool.false #[] (.let oneDecl (.let subOneDecl (← k.toMono)))
@@ -126,7 +126,7 @@ partial def casesNatToMono (c: Cases) (_ : c.typeName == ``Nat) : ToMonoM Code :
 partial def casesIntToMono (c: Cases) (_ : c.typeName == ``Int) : ToMonoM Code := do
   let resultType ← toMonoType c.resultType
   let natType := mkConst ``Nat
-  let zeroNatDecl ← mkLetDecl `natZero natType (.value (.natVal 0))
+  let zeroNatDecl ← mkLetDecl `natZero natType (.lit (.nat 0))
   let zeroIntDecl ← mkLetDecl `intZero (mkConst ``Int) (.const ``Int.ofNat [] #[.fvar zeroNatDecl.fvarId])
   let isNegDecl ← mkLetDecl `isNeg (mkConst ``Bool) (.const ``Int.decLt [] #[.fvar c.discr, .fvar zeroIntDecl.fvarId])
   let alts ← c.alts.mapM fun alt => do
@@ -137,7 +137,7 @@ partial def casesIntToMono (c: Cases) (_ : c.typeName == ``Int) : ToMonoM Code :
       let p := ps[0]!
       if ctorName == ``Int.negSucc then
         let absDecl ← mkLetDecl `abs natType (.const ``Int.natAbs [] #[.fvar c.discr])
-        let oneDecl ← mkLetDecl `one natType (.value (.natVal 1))
+        let oneDecl ← mkLetDecl `one natType (.lit (.nat 1))
         let subOneDecl := { fvarId := p.fvarId, binderName := p.binderName, type := natType, value := .const ``Nat.sub [] #[.fvar absDecl.fvarId, .fvar oneDecl.fvarId] }
         modifyLCtx fun lctx => lctx.addLetDecl subOneDecl
         return .alt ``Bool.true #[] (.let absDecl (.let oneDecl (.let subOneDecl (← k.toMono))))

src/Std/Data/ExtHashMapD.lean

@@ -0,0 +1,61 @@
+prelude
+import Std.Data.ExtHashMap
+import Init.Grind
+
+namespace Std
+
+structure ExtHashMapD (α : Type u) [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α] (β : Type v) [BEq β] [Inhabited β] where
+  /-- Internal implementation detail of the hash map -/
+  inner : ExtHashMap α β
+  /-- None of the values in the hash map are equal to the default value. -/
+  get_ne_default : ∀ (x : α) h, inner[x] != default
+
+namespace ExtHashMapD
+
+variable {α : Type u} [BEq α] [LawfulBEq α] [Hashable α] [LawfulHashable α] {β : Type v} [BEq β] [Inhabited β]
+
+@[inline, inherit_doc ExtHashMap.emptyWithCapacity]
+def emptyWithCapacity (capacity := 8) : ExtHashMapD α β :=
+  ⟨ExtHashMap.emptyWithCapacity capacity, by sorry⟩
+
+instance : EmptyCollection (ExtHashMapD α β) where
+  emptyCollection := emptyWithCapacity
+
+instance : Inhabited (ExtHashMapD α β) where
+  default := ∅
+
+def set (m : ExtHashMapD α β) (a : α) (b : β) : ExtHashMapD α β :=
+  if b == default then ⟨m.inner.erase a, by sorry⟩ else ⟨m.inner.insert a b, by sorry⟩
+
+instance : Singleton (α × β) (ExtHashMapD α β) where
+  singleton | ⟨a, b⟩ => (∅ : ExtHashMapD α β).set a b
+
+instance : Insert (α × β) (ExtHashMapD α β) where
+  insert | ⟨a, b⟩, s => s.set a b
+
+instance : LawfulSingleton (α × β) (ExtHashMapD α β) :=
+  ⟨fun _ => rfl⟩
+
+instance : GetElem (ExtHashMapD α β) α β (fun _ _ => True) where
+  getElem m a _ := m.inner.getD a default
+
+def map [BEq γ] [Inhabited γ] (f : α → β → γ) (m : ExtHashMapD α β) : ExtHashMapD α γ :=
+  ⟨m.inner.filterMap fun a b => let g := f a b; if g == default then none else some g, by sorry⟩
+
+def insertMany {ρ : Type w}
+    [ForIn Id ρ (α × β)] (m : ExtHashMapD α β) (l : ρ) := Id.run do
+  let mut m := m
+  for (a, b) in l do
+    m := m.set a b
+  return m
+
+def ofList (l : List (α × β)) : ExtHashMapD α β := (∅ : ExtHashMapD α β).insertMany l
+
+def modify (m : ExtHashMapD α β) (a : α) (f : β → β) : ExtHashMapD α β :=
+  ⟨m.inner.alter a (fun | none => none | some b => let b' := f b; if b' == default then none else some b'),
+    by sorry⟩
+
+def alter (m : ExtHashMapD α β) (a : α) (f : Option β → Option β) : ExtHashMapD α β :=
+  ⟨m.inner.alter a (fun b? => let b?' := f b?; if b?' == some default then none else b?'), by sorry⟩
+
+end ExtHashMapD

tests/lean/grind/module_normalization.lean

@@ -1,32 +0,0 @@
--- Tests for `grind` as a module normalization tactic, when only `NatModule`, `IntModule`, or `RatModule` is available.
-
-open Lean.Grind
-
-section NatModule
-
-variable (R : Type u) [NatModule R]
-
-example (a b : R) : a + b = b + a := by grind
-example (a : R) : a + 0 = a := by grind
-example (a : R) : 0 + a = a := by grind
-example (a b c : R) : a + b + c = a + (b + c) := by grind
-example (a : R) : 2 • a = a + a := by grind
-example (a b : R) : 2 • (b + c) = c + 2 • b + c := by grind
-
-end NatModule
-
-section IntModule
-
-variable (R : Type u) [IntModule R]
-
-example (a b : R) : a + b = b + a := by grind
-example (a : R) : a + 0 = a := by grind
-example (a : R) : 0 + a = a := by grind
-example (a b c : R) : a + b + c = a + (b + c) := by grind
-example (a : R) : 2 • a = a + a := by grind
-example (a : R) : (-2 : Int) • a = -a - a := by grind
-example (a b : R) : 2 • (b + c) = c + 2 • b + c := by grind
-example (a b c : R) : 2 • (b + c) - 3 • c + b + b = c + 5 • b - 2 • c := by grind
-example (a b c : R) : 2 • (b + c) + (-3 : Int) • c + b + b = c + (5 : Int) • b - 2 • c := by grind
-
-end IntModule

tests/lean/grind/module_relations.lean

@@ -1,27 +0,0 @@
--- Tests for `grind` as solver for linear equations in an `IntModule` or `RatModule`.
-
-open Lean.Grind
-
-section IntModule
-
-variable (R : Type u) [IntModule R]
-
--- In an `IntModule`, we should be able to handle relations
--- this is harder, and less important, than being able to do this in `RatModule`.
-example (a b : R) (h : a + b = 0) : 3 • a - 7 • b = 9 • a + a := by grind
-example (a b c : R) (h : 2 • a + 2 • b = 4 • c) : 3 • a + c = 5 • c - b + (-b) + a := by grind
-
-end IntModule
-
-section RatModule
-
-variable (R : Type u) [RatModule R]
-
-example (a b : R) (h : a + b = 0) : 3 • a - 7 • b = 9 • a + a := by grind
-example (a b c : R) (h : 2 • a + 2 • b = 4 • c) : 3 • a + c = 5 • c - b + (-b) + a := by grind
-
--- In a `RatModule` we can clear common divisors.
-example (a : R) (h : a + a = 0) : a = 0 := by grind
-example (a b c : R) (h : 2 • a + 2 • b = 4 • c) : 3 • a + c = 5 • c - 3 • b := by grind
-
-end RatModule

tests/lean/grind/ordered_modules.lean

@@ -1,64 +0,0 @@
-open Lean.Grind
-
-set_option grind.warning false
-
-variable (R : Type u) [RatModule R] [Preorder R] [IntModule.IsOrdered R]
-
-example (a b c : R) (h : a < b) : a + c < b + c := by grind
-example (a b c : R) (h : a < b) : c + a < c + b := by grind
-example (a b : R) (h : a < b) : -b < -a := by grind
-example (a b : R) (h : a < b) : -a < -b := by grind
-
-example (a b c : R) (h : a ≤ b) : a + c ≤ b + c := by grind
-example (a b c : R) (h : a ≤ b) : c + a ≤ c + b := by grind
-example (a b : R) (h : a ≤ b) : -b ≤ -a := by grind
-example (a b : R) (h : a ≤ b) : -a ≤ -b := by grind
-
-example (a : R) (h : 0 < a) : 0 ≤ a := by grind
-example (a : R) (h : 0 < a) : -2 • a < 0 := by grind
-
-example (a b c : R) (_ : a ≤ b) (_ : b ≤ c) : a ≤ c := by grind
-example (a b c : R) (_ : a ≤ b) (_ : b < c) : a < c := by grind
-example (a b c : R) (_ : a < b) (_ : b ≤ c) : a < c := by grind
-example (a b c : R) (_ : a < b) (_ : b < c) : a < c := by grind
-
-example (a : R) (h : 2 • a < 0) : a < 0 := by grind
-example (a : R) (h : 2 • a < 0) : 0 ≤ -a := by grind
-
-example (a b : R) (_ : a < b) (_ : b < a) : False := by grind
-example (a b : R) (_ : a < b ∧ b < a) : False := by grind
-example (a b : R) (_ : a < b) : a ≠ b := by grind
-
-example (a b c e v0 v1 : R) (h1 : v0 = 5 • a) (h2 : v1 = 3 • b) (h3 : v0 + v1 + c = 10 • e) :
-    v0 + 5 • e + (v1 - 3 • e) + (c - 2 • e) = 10 • e := by
-  grind
-
-example (x y z : Int) (h1 : 2 * x < 3 * y) (h2 : -4 * x + 2 * z < 0) (h3 : 12 * y - 4 * z < 0) : False := by
-  grind
-example (x y z : R) (h1 : 2 • x < 3 • y) (h2 : -4 • x + 2 • z < 0) (h3 : 12 • y - 4 • z < 0) : False := by
-  grind
-
-example (x y z : Int) (h1 : 2 * x < 3 * y) (h2 : -4 * x + 2 * z < 0) (h3 : x * y < 5) (h3 : 12 * y - 4 * z < 0) :
-    False := by grind
-example (x y z : R) (h1 : 2 • x < 3 • y) (h2 : -4 • x + 2 • z < 0) (h3 : 12 • y - 4 • z < 0) :
-    False := by grind
-
-example (x y z : Int) (hx : x ≤ 3 * y) (h2 : y ≤ 2 * z) (h3 : x ≥ 6 * z) : x = 3*y := by
-  grind
-example (x y z : R) (hx : x ≤ 3 • y) (h2 : y ≤ 2 • z) (h3 : x ≥ 6 • z) : x = 3 • y := by
-  grind
-
-example (x y z : Int) (h1 : 2 * x < 3 * y) (h2 : -4 * x + 2 * z < 0) (h3 : x * y < 5) : ¬ 12*y - 4* z < 0 := by
-  grind
-example (x y z : R) (h1 : 2 • x < 3 • y) (h2 : -4 • x + 2 • z < 0) : ¬ 12 • y - 4 • z < 0 := by
-  grind
-
-example (x y z : Int) (hx : ¬ x > 3 * y) (h2 : ¬ y > 2 * z) (h3 : x ≥ 6 * z) : x = 3 * y := by
-  grind
-example (x y z : R) (hx : ¬ x > 3 • y) (h2 : ¬ y > 2 • z) (h3 : x ≥ 6 • z) : x = 3 • y := by
-  grind
-
-example (x y z : Nat) (hx : x ≤ 3 * y) (h2 : y ≤ 2 * z) (h3 : x ≥ 6 * z) : x = 3 * y := by
-  grind
-example (x y z : R) (hx : x ≤ 3 • y) (h2 : y ≤ 2 • z) (h3 : x ≥ 6 • z) : x = 3 • y := by
-  grind

tests/lean/grind/ring_normalization.lean

@@ -0,0 +1,37 @@
+-- Tests for `grind` as a ring normalization tactic, when only `Semiring`, `CommSemiring`, or `Ring` is available.
+-- Note that in these cases we *do not* support hypotheses: there's no (good) analogue of Grobner bases here.
+
+open Lean.Grind
+
+section Semiring
+
+variable (R : Type u) [Semiring R]
+
+example (a b c : R) : a * (b + c) = a * c + a * b := by grind
+example (a b : R) : (a + b)^2 = a^2 + a * b + b * a + b^2 := by grind
+example (a b : R) : (a + 2 * b)^2 = a^2 + 2 * a * b + 2 * b * a + 4 * b^2 := by grind
+example (a b : R) : (a + 2 * b)^2 = a^2 + 2 * a * b + b * 2 * a + 4 * b^2 := by grind
+
+end Semiring
+
+section CommSemiring
+
+variable (R : Type u) [Semiring R]
+
+example (a b c : R) : a * (b + c) = a * c + b * a := by grind
+example (a b : R) : (a + b)^2 = a^2 + 2 * a * b + b^2 := by grind
+example (a b : R) : (a + 2 * b)^2 = a^2 + 4 * a * b + 4 * b^2 := by grind
+example (a b : R) : (a + 2 * b)^2 = 4 * b^2 + b * 4 * a + a^2 := by grind
+
+end CommSemiring
+
+section Ring
+
+variable (R : Type u) [Ring R]
+
+example (a b c : R) : a * (b - c) = - a * c + a * b := by grind
+example (a b : R) : (a - b)^2 = a^2 - a * b - b * a + b^2 := by grind
+example (a b : R) : (a + 2 * b)^2 = a^2 - 2 * a * b - 2 * b * a + 4 * b^2 := by grind
+example (a b : R) : (a + 2 * b)^2 = a^2 - 2 * a * b + -b * (-2) * -a + 4 * b^2 := by grind
+
+end Ring

tests/lean/run/2461.lean

@@ -93,6 +93,17 @@ end algebra_hierarchy_morphisms
 
 section HSMul_stuff
 
+class HSMul (α : Type) (β : Type) (γ : outParam Type) where
+  hSMul : α → β → γ
+
+class SMul (M : Type) (α : Type) where
+  smul : M → α → α
+
+infixr:73 " • " => HSMul.hSMul
+
+instance instHSMul {α β : Type} [SMul α β] : HSMul α β β where
+  hSMul := SMul.smul
+
 -- note that the function `SMulZeroClass.toSMul` is what disrupts `simp` later
 class SMulZeroClass (M A : Type) extends SMul M A where
 

tests/lean/run/3807.lean

@@ -751,6 +751,19 @@ universe u v w
 
 open Function
 
+class HSMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where
+  hSMul : α → β → γ
+
+class SMul (M : Type u) (α : Type v) where
+  smul : M → α → α
+
+infixr:73 " • " => HSMul.hSMul
+
+macro_rules | `($x • $y) => `(leftact% HSMul.hSMul $x $y)
+
+instance instHSMul {α β} [SMul α β] : HSMul α β β where
+  hSMul := SMul.smul
+
 variable {G : Type _}
 
 class Semigroup (G : Type u) extends Mul G where

tests/lean/run/binop_binrel_perf_issue.lean

@@ -153,10 +153,22 @@ universe u v w
 class HVAdd (α : Type u) (β : Type v) (γ : outParam (Type w)) where
   hVAdd : α → β → γ
 
+class HSMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where
+  hSMul : α → β → γ
+
 class VAdd (G : Type u) (P : Type v) where
   vadd : G → P → P
 
+class SMul (M : Type u) (α : Type v) where
+  smul : M → α → α
+
 infixl:65 " +ᵥ " => HVAdd.hVAdd
+infixr:73 " • " => HSMul.hSMul
+
+macro_rules | `($x • $y) => `(leftact% HSMul.hSMul $x $y)
+
+instance instHSMul {α β} [SMul α β] : HSMul α β β where
+  hSMul := SMul.smul
 
 instance instHVAdd {α β} [VAdd α β] : HVAdd α β β where
   hVAdd := VAdd.vadd

tests/lean/run/dsimpNatLitIssue.lean

@@ -8,6 +8,12 @@ class Bot (α : Type) where
 /-- The bot (`⊥`, `\bot`) element -/
 notation "⊥" => Bot.bot
 
+/-- Typeclass for types with a scalar multiplication operation, denoted `•` (`\bu`) -/
+class SMul (M α : Type) where
+  smul : M → α → α
+
+infixr:73 " • " => SMul.smul
+
 structure Submodule (R : Type) (M : Type) [Zero M] [SMul R M] where
   carrier : M → Prop
   zero_mem : carrier (0 : M)

tests/lean/run/infoFromFailure.lean

@@ -16,21 +16,7 @@ info: B.foo "hello" : String × String
 ---
 trace: [Meta.synthInstance] ❌️ Add String
   [Meta.synthInstance] new goal Add String
-    [Meta.synthInstance.instances] #[@Lean.Grind.Semiring.toAdd, @Lean.Grind.NatModule.toAdd, @Lean.Grind.IntModule.toAdd]
-  [Meta.synthInstance] ✅️ apply @Lean.Grind.IntModule.toAdd to Add String
-    [Meta.synthInstance.tryResolve] ✅️ Add String ≟ Add String
-    [Meta.synthInstance] new goal Lean.Grind.IntModule String
-      [Meta.synthInstance.instances] #[@Lean.Grind.RatModule.toIntModule]
-  [Meta.synthInstance] ✅️ apply @Lean.Grind.RatModule.toIntModule to Lean.Grind.IntModule String
-    [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.IntModule String ≟ Lean.Grind.IntModule String
-    [Meta.synthInstance] no instances for Lean.Grind.RatModule String
-      [Meta.synthInstance.instances] #[]
-  [Meta.synthInstance] ✅️ apply @Lean.Grind.NatModule.toAdd to Add String
-    [Meta.synthInstance.tryResolve] ✅️ Add String ≟ Add String
-    [Meta.synthInstance] new goal Lean.Grind.NatModule String
-      [Meta.synthInstance.instances] #[Lean.Grind.IntModule.toNatModule]
-  [Meta.synthInstance] ✅️ apply Lean.Grind.IntModule.toNatModule to Lean.Grind.NatModule String
-    [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.NatModule String ≟ Lean.Grind.NatModule String
+    [Meta.synthInstance.instances] #[@Lean.Grind.Semiring.toAdd]
   [Meta.synthInstance] ✅️ apply @Lean.Grind.Semiring.toAdd to Add String
     [Meta.synthInstance.tryResolve] ✅️ Add String ≟ Add String
     [Meta.synthInstance] new goal Lean.Grind.Semiring String
@@ -61,21 +47,7 @@ trace: [Meta.synthInstance] ❌️ Add String
 /--
 trace: [Meta.synthInstance] ❌️ Add Bool
   [Meta.synthInstance] new goal Add Bool
-    [Meta.synthInstance.instances] #[@Lean.Grind.Semiring.toAdd, @Lean.Grind.NatModule.toAdd, @Lean.Grind.IntModule.toAdd]
-  [Meta.synthInstance] ✅️ apply @Lean.Grind.IntModule.toAdd to Add Bool
-    [Meta.synthInstance.tryResolve] ✅️ Add Bool ≟ Add Bool
-    [Meta.synthInstance] new goal Lean.Grind.IntModule Bool
-      [Meta.synthInstance.instances] #[@Lean.Grind.RatModule.toIntModule]
-  [Meta.synthInstance] ✅️ apply @Lean.Grind.RatModule.toIntModule to Lean.Grind.IntModule Bool
-    [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.IntModule Bool ≟ Lean.Grind.IntModule Bool
-    [Meta.synthInstance] no instances for Lean.Grind.RatModule Bool
-      [Meta.synthInstance.instances] #[]
-  [Meta.synthInstance] ✅️ apply @Lean.Grind.NatModule.toAdd to Add Bool
-    [Meta.synthInstance.tryResolve] ✅️ Add Bool ≟ Add Bool
-    [Meta.synthInstance] new goal Lean.Grind.NatModule Bool
-      [Meta.synthInstance.instances] #[Lean.Grind.IntModule.toNatModule]
-  [Meta.synthInstance] ✅️ apply Lean.Grind.IntModule.toNatModule to Lean.Grind.NatModule Bool
-    [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.NatModule Bool ≟ Lean.Grind.NatModule Bool
+    [Meta.synthInstance.instances] #[@Lean.Grind.Semiring.toAdd]
   [Meta.synthInstance] ✅️ apply @Lean.Grind.Semiring.toAdd to Add Bool
     [Meta.synthInstance.tryResolve] ✅️ Add Bool ≟ Add Bool
     [Meta.synthInstance] new goal Lean.Grind.Semiring Bool

tests/lean/run/info_trees.lean

@@ -61,7 +61,7 @@ info: • command @ ⟨82, 0⟩-⟨82, 40⟩ @ Lean.Elab.Command.elabDeclaration
                   ⊢ 0 ≤ n
                   after no goals
                   • Nat.zero_le n : 0 ≤ n @ ⟨1, 1⟩†-⟨1, 1⟩† @ Lean.Elab.Term.elabApp
-                    • [.] Nat.zero_le : some LE.le.{0} Nat instLENat (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)) _uniq.42 @ ⟨1, 0⟩†-⟨1, 0⟩†
+                    • [.] Nat.zero_le : some LE.le.{0} Nat instLENat (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)) _uniq.41 @ ⟨1, 0⟩†-⟨1, 0⟩†
                     • Nat.zero_le : ∀ (n : Nat), 0 ≤ n @ ⟨1, 0⟩†-⟨1, 0⟩†
                     • n : Nat @ ⟨1, 5⟩†-⟨1, 5⟩† @ Lean.Elab.Term.elabIdent
                       • [.] n : some Nat @ ⟨1, 5⟩†-⟨1, 5⟩†

tests/lean/run/linearCategory_perf_issue.lean

@@ -2,6 +2,19 @@ universe u v w v₁ v₂ v₃ u₁ u₂ u₃
 
 section Mathlib.Algebra.Group.Defs
 
+class HSMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where
+  hSMul : α → β → γ
+
+class SMul (M : Type u) (α : Type v) where
+  smul : M → α → α
+
+infixr:73 " • " => SMul.smul
+
+macro_rules | `($x • $y) => `(leftact% HSMul.hSMul $x $y)
+
+instance instHSMul {α β} [SMul α β] : HSMul α β β where
+  hSMul := SMul.smul
+
 class AddMonoid (M : Type u) extends Add M, Zero M where
   protected add_assoc : ∀ a b c : M, a + b + c = a + (b + c)
   protected zero_add : ∀ a : M, 0 + a = a

tests/lean/run/nestedtc.lean

@@ -3,6 +3,11 @@ variable {R : Type}
 
 class Zip (α : Type) -- represents `Zero`
 
+class SMul (R : Type) (α : Type) where
+  smul : R → α → α
+
+infixr:73 " • " => SMul.smul
+
 class MulAction (R : Type) (β : Type) extends SMul R β
 
 class SMulZeroClass (R α : Type) extends SMul R α where

tests/lean/run/structWithAlgTCSynth.lean

@@ -101,6 +101,17 @@ end Mathlib.Logic.Function.Basic
 
 section Mathlib.Algebra.Group.Defs
 
+class HSMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where
+  hSMul : α → β → γ
+
+class SMul (M : Type _) (α : Type _) where
+  smul : M → α → α
+
+infixr:73 " • " => HSMul.hSMul
+
+instance instHSMul [SMul α β] : HSMul α β β where
+  hSMul := SMul.smul
+
 class Semigroup (G : Type u) extends Mul G where
   mul_assoc : ∀ a b c : G, a * b * c = a * (b * c)
 

tests/lean/run/synthInstsIssue.lean

@@ -4,6 +4,23 @@ https://github.com/leanprover/lean4/pull/2793.
 We find that we need to either specify a named argument or use `..` in certain rewrites.
 -/
 
+section Mathlib.Algebra.Group.Defs
+
+universe u v w
+
+class HSMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where
+  hSMul : α → β → γ
+
+class SMul (M : Type u) (α : Type v) where
+  smul : M → α → α
+
+infixr:73 " • " => HSMul.hSMul
+
+instance instHSMul {α β} [SMul α β] : HSMul α β β where
+  hSMul := SMul.smul
+
+end Mathlib.Algebra.Group.Defs
+
 section Mathlib.Data.FunLike.Basic
 
 class DFunLike (F : Sort _) (α : outParam (Sort _)) (β : outParam <| α → Sort _) where