merge upstream_hsmul

src/Init/Grind.lean

@@ -15,4 +15,5 @@ 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

@@ -0,0 +1,10 @@
+/-
+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

@@ -0,0 +1,72 @@
+/-
+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

@@ -0,0 +1,48 @@
+/-
+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,6 +295,7 @@ 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.
@@ -312,6 +313,40 @@ 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_^^^_»]
@@ -323,6 +358,7 @@ 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,6 +1348,23 @@ 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 : β`.
@@ -1510,6 +1527,12 @@ 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`. -/
@@ -1601,6 +1624,13 @@ 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

tests/lean/grind/module_normalization.lean

@@ -0,0 +1,32 @@
+-- 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

@@ -0,0 +1,27 @@
+-- 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

@@ -0,0 +1,64 @@
+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/run/2461.lean

@@ -93,17 +93,6 @@ 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,19 +751,6 @@ 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,22 +153,10 @@ 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,12 +8,6 @@ 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,7 +16,21 @@ info: B.foo "hello" : String × String
 ---
 trace: [Meta.synthInstance] ❌️ Add String
   [Meta.synthInstance] new goal Add String
-    [Meta.synthInstance.instances] #[@Lean.Grind.Semiring.toAdd]
+    [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] ✅️ apply @Lean.Grind.Semiring.toAdd to Add String
     [Meta.synthInstance.tryResolve] ✅️ Add String ≟ Add String
     [Meta.synthInstance] new goal Lean.Grind.Semiring String
@@ -47,7 +61,21 @@ trace: [Meta.synthInstance] ❌️ Add String
 /--
 trace: [Meta.synthInstance] ❌️ Add Bool
   [Meta.synthInstance] new goal Add Bool
-    [Meta.synthInstance.instances] #[@Lean.Grind.Semiring.toAdd]
+    [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] ✅️ 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.41 @ ⟨1, 0⟩†-⟨1, 0⟩†
+                    • [.] 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 : ∀ (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,19 +2,6 @@ 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,11 +3,6 @@ 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,17 +101,6 @@ 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,23 +4,6 @@ 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