fix test

src/Init/Data/BitVec/Lemmas.lean

@@ -3339,6 +3339,14 @@ theorem sub_toAdd {n} (x y : BitVec n) : x - y = x + - y := by
   simp only [toNat_sub, toNat_add, toNat_neg, Nat.add_mod_mod]
   rw [Nat.add_comm]
 
+theorem add_left_neg (x : BitVec w) : -x + x = 0#w := by
+  apply toInt_inj.mp
+  simp [toInt_neg, Int.add_left_neg]
+
+theorem add_right_neg (x : BitVec w) : x + -x = 0#w := by
+  rw [BitVec.add_comm]
+  exact add_left_neg x
+
 @[simp] theorem neg_zero (n:Nat) : -BitVec.ofNat n 0 = BitVec.ofNat n 0 := by apply eq_of_toNat_eq ; simp
 
 theorem add_sub_cancel (x y : BitVec w) : x + y - y = x := by

src/Init/Data/SInt/Lemmas.lean

@@ -2393,6 +2393,17 @@ instance : Std.LawfulIdentity (α := ISize) (· + ·) 0 where
 @[simp] protected theorem Int64.sub_self (a : Int64) : a - a = 0 := Int64.toBitVec_inj.1 (BitVec.sub_self _)
 @[simp] protected theorem ISize.sub_self (a : ISize) : a - a = 0 := ISize.toBitVec_inj.1 (BitVec.sub_self _)
 
+protected theorem Int8.add_left_neg (a : Int8) : -a + a = 0 := Int8.toBitVec_inj.1 (BitVec.add_left_neg _)
+protected theorem Int8.add_right_neg (a : Int8) : a + -a = 0 := Int8.toBitVec_inj.1 (BitVec.add_right_neg _)
+protected theorem Int16.add_left_neg (a : Int16) : -a + a = 0 := Int16.toBitVec_inj.1 (BitVec.add_left_neg _)
+protected theorem Int16.add_right_neg (a : Int16) : a + -a = 0 := Int16.toBitVec_inj.1 (BitVec.add_right_neg _)
+protected theorem Int32.add_left_neg (a : Int32) : -a + a = 0 := Int32.toBitVec_inj.1 (BitVec.add_left_neg _)
+protected theorem Int32.add_right_neg (a : Int32) : a + -a = 0 := Int32.toBitVec_inj.1 (BitVec.add_right_neg _)
+protected theorem Int64.add_left_neg (a : Int64) : -a + a = 0 := Int64.toBitVec_inj.1 (BitVec.add_left_neg _)
+protected theorem Int64.add_right_neg (a : Int64) : a + -a = 0 := Int64.toBitVec_inj.1 (BitVec.add_right_neg _)
+protected theorem ISize.add_left_neg (a : ISize) : -a + a = 0 := ISize.toBitVec_inj.1 (BitVec.add_left_neg _)
+protected theorem ISize.add_right_neg (a : ISize) : a + -a = 0 := ISize.toBitVec_inj.1 (BitVec.add_right_neg _)
+
 @[simp] protected theorem Int8.sub_add_cancel (a b : Int8) : a - b + b = a :=
   Int8.toBitVec_inj.1 (BitVec.sub_add_cancel _ _)
 @[simp] protected theorem Int16.sub_add_cancel (a b : Int16) : a - b + b = a :=

src/Init/Data/UInt/Lemmas.lean

@@ -2376,6 +2376,17 @@ instance : Std.LawfulIdentity (α := USize) (· + ·) 0 where
 @[simp] protected theorem UInt64.sub_self (a : UInt64) : a - a = 0 := UInt64.toBitVec_inj.1 (BitVec.sub_self _)
 @[simp] protected theorem USize.sub_self (a : USize) : a - a = 0 := USize.toBitVec_inj.1 (BitVec.sub_self _)
 
+protected theorem UInt8.add_left_neg (a : UInt8) : -a + a = 0 := UInt8.toBitVec_inj.1 (BitVec.add_left_neg _)
+protected theorem UInt8.add_right_neg (a : UInt8) : a + -a = 0 := UInt8.toBitVec_inj.1 (BitVec.add_right_neg _)
+protected theorem UInt16.add_left_neg (a : UInt16) : -a + a = 0 := UInt16.toBitVec_inj.1 (BitVec.add_left_neg _)
+protected theorem UInt16.add_right_neg (a : UInt16) : a + -a = 0 := UInt16.toBitVec_inj.1 (BitVec.add_right_neg _)
+protected theorem UInt32.add_left_neg (a : UInt32) : -a + a = 0 := UInt32.toBitVec_inj.1 (BitVec.add_left_neg _)
+protected theorem UInt32.add_right_neg (a : UInt32) : a + -a = 0 := UInt32.toBitVec_inj.1 (BitVec.add_right_neg _)
+protected theorem UInt64.add_left_neg (a : UInt64) : -a + a = 0 := UInt64.toBitVec_inj.1 (BitVec.add_left_neg _)
+protected theorem UInt64.add_right_neg (a : UInt64) : a + -a = 0 := UInt64.toBitVec_inj.1 (BitVec.add_right_neg _)
+protected theorem USize.add_left_neg (a : USize) : -a + a = 0 := USize.toBitVec_inj.1 (BitVec.add_left_neg _)
+protected theorem USize.add_right_neg (a : USize) : a + -a = 0 := USize.toBitVec_inj.1 (BitVec.add_right_neg _)
+
 @[simp] protected theorem UInt8.neg_zero : -(0 : UInt8) = 0 := rfl
 @[simp] protected theorem UInt16.neg_zero : -(0 : UInt16) = 0 := rfl
 @[simp] protected theorem UInt32.neg_zero : -(0 : UInt32) = 0 := rfl

src/Init/Data/Zero.lean

@@ -15,3 +15,13 @@ instance (priority := 300) Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) w
 
 instance (priority := 200) Zero.ofOfNat0 {α} [OfNat α (nat_lit 0)] : Zero α where
   zero := 0
+
+/-!
+Instances converting between `One α` and `OfNat α (nat_lit 1)`.
+-/
+
+instance (priority := 300) One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
+  ofNat := ‹One α›.1
+
+instance (priority := 200) One.ofOfNat1 {α} [OfNat α (nat_lit 1)] : One α where
+  one := 1

src/Init/Grind.lean

@@ -12,3 +12,4 @@ import Init.Grind.Propagator
 import Init.Grind.Util
 import Init.Grind.Offset
 import Init.Grind.PP
+import Init.Grind.CommRing

src/Init/Grind/CommRing.lean

@@ -0,0 +1,11 @@
+/-
+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
+-/
+prelude
+import Init.Grind.CommRing.Basic
+import Init.Grind.CommRing.Int
+import Init.Grind.CommRing.UInt
+import Init.Grind.CommRing.SInt
+import Init.Grind.CommRing.BitVec

src/Init/Grind/CommRing/Basic.lean

@@ -0,0 +1,47 @@
+/-
+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
+-/
+prelude
+import Init.Data.Zero
+
+/-!
+# A monolithic commutative ring typeclass for internal use in `grind`.
+-/
+
+namespace Lean.Grind
+
+class CommRing (α : Type u) extends Add α, Zero α, Mul α, One α, Neg α where
+  add_assoc : ∀ a b c : α, a + b + c = a + (b + c)
+  add_comm : ∀ a b : α, a + b = b + a
+  add_zero : ∀ a : α, a + 0 = a
+  neg_add_cancel : ∀ a : α, -a + a = 0
+  mul_assoc : ∀ a b c : α, a * b * c = a * (b * c)
+  mul_comm : ∀ a b : α, a * b = b * a
+  mul_one : ∀ a : α, a * 1 = a
+  left_distrib : ∀ a b c : α, a * (b + c) = a * b + a * c
+  zero_mul : ∀ a : α, 0 * a = 0
+
+namespace CommRing
+
+variable {α : Type u} [CommRing α]
+
+theorem zero_add (a : α) : 0 + a = a := by
+  rw [add_comm, add_zero]
+
+theorem add_neg_cancel (a : α) : a + -a = 0 := by
+  rw [add_comm, neg_add_cancel]
+
+theorem one_mul (a : α) : 1 * a = a := by
+  rw [mul_comm, mul_one]
+
+theorem right_distrib (a b c : α) : (a + b) * c = a * c + b * c := by
+  rw [mul_comm, left_distrib, mul_comm c, mul_comm c]
+
+theorem mul_zero (a : α) : a * 0 = 0 := by
+  rw [mul_comm, zero_mul]
+
+end CommRing
+
+end Lean.Grind

src/Init/Grind/CommRing/BitVec.lean

@@ -0,0 +1,23 @@
+/-
+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
+-/
+prelude
+import Init.Grind.CommRing.Basic
+import Init.Data.BitVec.Lemmas
+
+namespace Lean.Grind
+
+instance : CommRing (BitVec w) where
+  add_assoc := BitVec.add_assoc
+  add_comm := BitVec.add_comm
+  add_zero := BitVec.add_zero
+  neg_add_cancel := BitVec.add_left_neg
+  mul_assoc := BitVec.mul_assoc
+  mul_comm := BitVec.mul_comm
+  mul_one := BitVec.mul_one
+  left_distrib _ _ _ := BitVec.mul_add
+  zero_mul _ := BitVec.zero_mul
+
+end Lean.Grind

src/Init/Grind/CommRing/Int.lean

@@ -0,0 +1,23 @@
+/-
+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
+-/
+prelude
+import Init.Grind.CommRing.Basic
+import Init.Data.Int.Lemmas
+
+namespace Lean.Grind
+
+instance : CommRing Int where
+  add_assoc := Int.add_assoc
+  add_comm := Int.add_comm
+  add_zero := Int.add_zero
+  neg_add_cancel := Int.add_left_neg
+  mul_assoc := Int.mul_assoc
+  mul_comm := Int.mul_comm
+  mul_one := Int.mul_one
+  left_distrib := Int.mul_add
+  zero_mul := Int.zero_mul
+
+end Lean.Grind

src/Init/Grind/CommRing/SInt.lean

@@ -0,0 +1,67 @@
+/-
+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
+-/
+prelude
+import Init.Grind.CommRing.Basic
+import Init.Data.SInt.Lemmas
+
+namespace Lean.Grind
+
+instance : CommRing Int8 where
+  add_assoc := Int8.add_assoc
+  add_comm := Int8.add_comm
+  add_zero := Int8.add_zero
+  neg_add_cancel := Int8.add_left_neg
+  mul_assoc := Int8.mul_assoc
+  mul_comm := Int8.mul_comm
+  mul_one := Int8.mul_one
+  left_distrib _ _ _ := Int8.mul_add
+  zero_mul _ := Int8.zero_mul
+
+instance : CommRing Int16 where
+  add_assoc := Int16.add_assoc
+  add_comm := Int16.add_comm
+  add_zero := Int16.add_zero
+  neg_add_cancel := Int16.add_left_neg
+  mul_assoc := Int16.mul_assoc
+  mul_comm := Int16.mul_comm
+  mul_one := Int16.mul_one
+  left_distrib _ _ _ := Int16.mul_add
+  zero_mul _ := Int16.zero_mul
+
+instance : CommRing Int32 where
+  add_assoc := Int32.add_assoc
+  add_comm := Int32.add_comm
+  add_zero := Int32.add_zero
+  neg_add_cancel := Int32.add_left_neg
+  mul_assoc := Int32.mul_assoc
+  mul_comm := Int32.mul_comm
+  mul_one := Int32.mul_one
+  left_distrib _ _ _ := Int32.mul_add
+  zero_mul _ := Int32.zero_mul
+
+instance : CommRing Int64 where
+  add_assoc := Int64.add_assoc
+  add_comm := Int64.add_comm
+  add_zero := Int64.add_zero
+  neg_add_cancel := Int64.add_left_neg
+  mul_assoc := Int64.mul_assoc
+  mul_comm := Int64.mul_comm
+  mul_one := Int64.mul_one
+  left_distrib _ _ _ := Int64.mul_add
+  zero_mul _ := Int64.zero_mul
+
+instance : CommRing ISize where
+  add_assoc := ISize.add_assoc
+  add_comm := ISize.add_comm
+  add_zero := ISize.add_zero
+  neg_add_cancel := ISize.add_left_neg
+  mul_assoc := ISize.mul_assoc
+  mul_comm := ISize.mul_comm
+  mul_one := ISize.mul_one
+  left_distrib _ _ _ := ISize.mul_add
+  zero_mul _ := ISize.zero_mul
+
+end Lean.Grind

src/Init/Grind/CommRing/UInt.lean

@@ -0,0 +1,67 @@
+/-
+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
+-/
+prelude
+import Init.Grind.CommRing.Basic
+import Init.Data.UInt.Lemmas
+
+namespace Lean.Grind
+
+instance : CommRing UInt8 where
+  add_assoc := UInt8.add_assoc
+  add_comm := UInt8.add_comm
+  add_zero := UInt8.add_zero
+  neg_add_cancel := UInt8.add_left_neg
+  mul_assoc := UInt8.mul_assoc
+  mul_comm := UInt8.mul_comm
+  mul_one := UInt8.mul_one
+  left_distrib _ _ _ := UInt8.mul_add
+  zero_mul _ := UInt8.zero_mul
+
+instance : CommRing UInt16 where
+  add_assoc := UInt16.add_assoc
+  add_comm := UInt16.add_comm
+  add_zero := UInt16.add_zero
+  neg_add_cancel := UInt16.add_left_neg
+  mul_assoc := UInt16.mul_assoc
+  mul_comm := UInt16.mul_comm
+  mul_one := UInt16.mul_one
+  left_distrib _ _ _ := UInt16.mul_add
+  zero_mul _ := UInt16.zero_mul
+
+instance : CommRing UInt32 where
+  add_assoc := UInt32.add_assoc
+  add_comm := UInt32.add_comm
+  add_zero := UInt32.add_zero
+  neg_add_cancel := UInt32.add_left_neg
+  mul_assoc := UInt32.mul_assoc
+  mul_comm := UInt32.mul_comm
+  mul_one := UInt32.mul_one
+  left_distrib _ _ _ := UInt32.mul_add
+  zero_mul _ := UInt32.zero_mul
+
+instance : CommRing UInt64 where
+  add_assoc := UInt64.add_assoc
+  add_comm := UInt64.add_comm
+  add_zero := UInt64.add_zero
+  neg_add_cancel := UInt64.add_left_neg
+  mul_assoc := UInt64.mul_assoc
+  mul_comm := UInt64.mul_comm
+  mul_one := UInt64.mul_one
+  left_distrib _ _ _ := UInt64.mul_add
+  zero_mul _ := UInt64.zero_mul
+
+instance : CommRing USize where
+  add_assoc := USize.add_assoc
+  add_comm := USize.add_comm
+  add_zero := USize.add_zero
+  neg_add_cancel := USize.add_left_neg
+  mul_assoc := USize.mul_assoc
+  mul_comm := USize.mul_comm
+  mul_one := USize.mul_one
+  left_distrib _ _ _ := USize.mul_add
+  zero_mul _ := USize.zero_mul
+
+end Lean.Grind

src/Init/Prelude.lean

@@ -1415,6 +1415,11 @@ class Zero (α : Type u) where
   /-- The zero element of the type. -/
   zero : α
 
+/-- A type with a "one" element. -/
+class One (α : Type u) where
+  /-- The "one" element of the type. -/
+  one : α
+
 /-- The homogeneous version of `HAdd`: `a + b : α` where `a b : α`. -/
 class Add (α : Type u) where
   /-- `a + b` computes the sum of `a` and `b`. See `HAdd`. -/

tests/lean/1018unknowMVarIssue.lean.expected.out

@@ -60,8 +60,8 @@ a : α
         • Fam2.any : Fam2 α α @ ⟨9, 4⟩†-⟨9, 12⟩†
           • α : Type @ ⟨9, 4⟩†-⟨9, 12⟩†
         • a (isBinder := true) : α @ ⟨8, 2⟩†-⟨10, 19⟩†
-        • FVarAlias a: _uniq.592 -> _uniq.319
-        • FVarAlias α: _uniq.591 -> _uniq.317
+        • FVarAlias a: _uniq.596 -> _uniq.323
+        • FVarAlias α: _uniq.595 -> _uniq.321
         • ?m x α a : α @ ⟨9, 18⟩-⟨9, 19⟩ @ Lean.Elab.Term.elabHole
         • [.] Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩
         • Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
@@ -75,8 +75,8 @@ a : α
         • Fam2.nat n : Fam2 Nat Nat @ ⟨10, 4⟩†-⟨10, 14⟩
           • n (isBinder := true) : Nat @ ⟨10, 13⟩-⟨10, 14⟩
         • a (isBinder := true) : Nat @ ⟨8, 2⟩†-⟨10, 19⟩†
-        • FVarAlias a: _uniq.623 -> _uniq.319
-        • FVarAlias n: _uniq.622 -> _uniq.317
+        • FVarAlias a: _uniq.627 -> _uniq.323
+        • FVarAlias n: _uniq.626 -> _uniq.321
         • n : Nat @ ⟨10, 18⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabIdent
           • [.] n : some Nat @ ⟨10, 18⟩-⟨10, 19⟩
           • n : Nat @ ⟨10, 18⟩-⟨10, 19⟩

tests/lean/1870.lean

@@ -1,23 +0,0 @@
-class One (α : Type u) where
-  one : α
-
-instance One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
-  ofNat := ‹One α›.1
-
-instance One.ofOfNat1 {α} [OfNat α (nat_lit 1)] : One α where
-  one := 1
-
-set_option pp.mvars false in
-theorem ex1 : (@OfNat.ofNat Nat 0 Zero.toOfNat0) = @OfNat.ofNat Nat 1 One.toOfNat1 := by
-  refine congrArg _ (congrArg _ ?_)
-  rfl
-
-example : (@OfNat.ofNat Nat 0 Zero.toOfNat0) = @OfNat.ofNat Nat 1 One.toOfNat1 := by
-  apply congrArg
-  apply congrArg
-  apply rfl
-
-theorem ex2 : (@OfNat.ofNat Nat 0 Zero.toOfNat0) = @OfNat.ofNat Nat 1 One.toOfNat1 := by
-  apply congrArg
-  apply congrArg
-  apply rfl

tests/lean/1870.lean.expected.out

@@ -1,16 +0,0 @@
-1870.lean:12:2-12:35: error: type mismatch
-  congrArg ?_ (congrArg ?_ ?_)
-has type
-  ?_ (?_ ?_) = ?_ (?_ ?_) : Prop
-but is expected to have type
-  OfNat.ofNat 0 = OfNat.ofNat 1 : Prop
-1870.lean:16:2-16:16: error: tactic 'apply' failed, failed to unify
-  ?f ?a₁ = ?f ?a₂
-with
-  OfNat.ofNat 0 = OfNat.ofNat 1
-⊢ OfNat.ofNat 0 = OfNat.ofNat 1
-1870.lean:21:2-21:16: error: tactic 'apply' failed, failed to unify
-  ?f ?a₁ = ?f ?a₂
-with
-  OfNat.ofNat 0 = OfNat.ofNat 1
-⊢ OfNat.ofNat 0 = OfNat.ofNat 1

tests/lean/948.lean

@@ -1,9 +1,6 @@
 class Trait (X : Type) where
   R : Type
 
-class One (R : Type) where
-  one : R
-
 attribute [reducible] Trait.R
 
 def add_one {X} [Trait X] [One (Trait.R X)] [HAdd X (Trait.R X) X] (x : X) : X := x + (One.one : (Trait.R X))

tests/lean/diamond7.lean

@@ -4,12 +4,6 @@ class Semigroup (α : Type u) extends Mul α where
 class CommSemigroup (α : Type u) extends Semigroup α where
   mul_comm (a b : α) : a * b = b * a
 
-class One (α : Type u) where
-  one : α
-
-instance [One α] : OfNat α (nat_lit 1) where
-  ofNat := One.one
-
 class Monoid (α : Type u) extends Semigroup α, One α where
   one_mul (a : α) : 1 * a = a
   mul_one (a : α) : a * 1 = a

tests/lean/diamond8.lean

@@ -1,6 +1,3 @@
-class One (M : Type u) where one : M
-instance {M} [One M] : OfNat M (nat_lit 1) := ⟨One.one⟩
-
 class Monoid (M : Type u) extends Mul M, One M where
   mul_one (m : M) : m * 1 = m
 

tests/lean/infoFromFailure.lean

@@ -1,18 +0,0 @@
-
-
-def A.foo {α : Type} [Add α] (a : α) : α × α :=
-(a, a + a)
-
-def B.foo {α : Type} (a : α) : α × α :=
-(a, a)
-
-open A
-open B
-
-set_option trace.Meta.synthInstance true
--- `foo` is overloaded, the case `A.foo` is discarded because we don't have an instance `[Add String]`.
--- However, we still want to see the trace since we used trace.Meta.synthInstance
-#check foo "hello"
-
-theorem ex : foo true = (true, true) :=
-rfl

tests/lean/infoFromFailure.lean.expected.out

@@ -1,9 +0,0 @@
-B.foo "hello" : String × String
-[Meta.synthInstance] ❌️ Add String
-  [Meta.synthInstance] no instances for Add String
-    [Meta.synthInstance.instances] #[]
-  [Meta.synthInstance] result <not-available>
-[Meta.synthInstance] ❌️ Add Bool
-  [Meta.synthInstance] no instances for Add Bool
-    [Meta.synthInstance.instances] #[]
-  [Meta.synthInstance] result <not-available>

tests/lean/interactive/completionPrefixIssue.lean.expected.out

@@ -7,7 +7,7 @@
    {"params":
     {"textDocument": {"uri": "file:///completionPrefixIssue.lean"},
      "position": {"line": 1, "character": 64}},
-    "id": {"fvar": {"id": "_uniq.29"}},
+    "id": {"fvar": {"id": "_uniq.32"}},
     "cPos": 0}},
   {"label": "veryLongDefinitionNameVeryLongDefinitionName",
    "kind": 21,

tests/lean/run/1711.lean

@@ -1,9 +1,3 @@
-class One (α : Type u) where
-  one : α
-
-instance One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
-  ofNat := ‹One α›.1
-
 class MulOneClass (M : Type u) extends One M, Mul M where
   one_mul : ∀ a : M, 1 * a = a
   mul_one : ∀ a : M, a * 1 = a

tests/lean/run/1870.lean

@@ -0,0 +1,40 @@
+set_option pp.mvars false
+
+/--
+error: type mismatch
+  congrArg ?_ (congrArg ?_ ?_)
+has type
+  ?_ (?_ ?_) = ?_ (?_ ?_) : Prop
+but is expected to have type
+  OfNat.ofNat 0 = OfNat.ofNat 1 : Prop
+-/
+#guard_msgs in
+theorem ex1 : (@OfNat.ofNat Nat 0 Zero.toOfNat0) = @OfNat.ofNat Nat 1 One.toOfNat1 := by
+  refine congrArg _ (congrArg _ ?_)
+  rfl
+
+/--
+error: tactic 'apply' failed, failed to unify
+  ?_ ?_ = ?_ ?_
+with
+  OfNat.ofNat 0 = OfNat.ofNat 1
+⊢ OfNat.ofNat 0 = OfNat.ofNat 1
+-/
+#guard_msgs in
+example : (@OfNat.ofNat Nat 0 Zero.toOfNat0) = @OfNat.ofNat Nat 1 One.toOfNat1 := by
+  apply congrArg
+  apply congrArg
+  apply rfl
+
+/--
+error: tactic 'apply' failed, failed to unify
+  ?_ ?_ = ?_ ?_
+with
+  OfNat.ofNat 0 = OfNat.ofNat 1
+⊢ OfNat.ofNat 0 = OfNat.ofNat 1
+-/
+#guard_msgs in
+theorem ex2 : (@OfNat.ofNat Nat 0 Zero.toOfNat0) = @OfNat.ofNat Nat 1 One.toOfNat1 := by
+  apply congrArg
+  apply congrArg
+  apply rfl

tests/lean/run/1907.lean

@@ -1,9 +1,3 @@
-class One (α : Type u) where
-  one : α
-
-instance One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
-  ofNat := ‹One α›.1
-
 class MulOneClass (M : Type u) extends One M, Mul M
 
 class FunLike (F : Sort _) (α : outParam (Sort _)) (β : outParam <| α → Sort _) where

tests/lean/run/1907orig.lean

@@ -1,9 +1,3 @@
-class One (α : Type u) where
-  one : α
-
-instance One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
-  ofNat := ‹One α›.1
-
 class MulOneClass (M : Type u) extends One M, Mul M
 
 class FunLike (F : Sort _) (α : outParam (Sort _)) (β : outParam <| α → Sort _) where

tests/lean/run/1951.lean

@@ -1,7 +1,5 @@
 class FunLike (F : Type _) (A : outParam (Type _)) (B : outParam (A → Type _)) where toFun : F → ∀ a, B a
 instance [FunLike F A B] : CoeFun F fun _ => ∀ a, B a where coe := FunLike.toFun
-class One (M) where one : M
-instance [One M] : OfNat M (nat_lit 1) where ofNat := One.one
 class OneHomClass (F) (A B : outParam _) [One A] [One B] extends FunLike F A fun _ => B where
   map_one (f : F) : f 1 = 1
 class MulHomClass (F) (A B : outParam _) [Mul A] [Mul B] extends FunLike F A fun _ => B

tests/lean/run/2461.lean

@@ -1,8 +1,5 @@
 section algebra_hierarchy_classes_to_comm_ring
 
-class One (α : Type) where
-  one : α
-
 class Semiring (α : Type) extends Add α, Mul α, Zero α, One α
 
 class CommSemiring (R : Type) extends Semiring R

tests/lean/run/2736.lean

@@ -1,15 +1,5 @@
 set_option autoImplicit true
 
-section Mathlib.Init.ZeroOne
-
-class One (α : Type) where
-  one : α
-
-instance One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
-  ofNat := ‹One α›.1
-
-end Mathlib.Init.ZeroOne
-
 section Mathlib.Algebra.Group.Defs
 
 class MulOneClass (M : Type) extends One M, Mul M where

tests/lean/run/3150.lean

@@ -1,6 +1,3 @@
-class One (α : Type) where
-  one : α
-
 variable (R A : Type) [One R] [One A]
 
 class OneHom where

tests/lean/run/3807.lean

@@ -87,18 +87,6 @@ class PartialOrder (α : Type u) extends Preorder α where
 
 end Mathlib.Init.Order.Defs
 
-section Mathlib.Init.ZeroOne
-
-set_option autoImplicit true
-
-class One (α : Type u) where
-  one : α
-
-instance (priority := 300) One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
-  ofNat := ‹One α›.1
-
-end Mathlib.Init.ZeroOne
-
 section Mathlib.Init.Function
 
 universe u₁ u₂

tests/lean/run/KyleAlg.lean

@@ -14,13 +14,7 @@ class Inv (α : Type u) where
 
 postfix:max "⁻¹" => Inv.inv
 
-class One (α : Type u) where
-    one : α
 export One (one)
-
-instance [One α] : OfNat α (nat_lit 1) where
-    ofNat := one
-
 export Zero (zero)
 
 class MulComm (α : Type u) [Mul α] : Prop where

tests/lean/run/KyleAlgAbbrev.lean

@@ -14,13 +14,6 @@ class Inv (α : Type u) where
 
 postfix:max "⁻¹" => Inv.inv
 
-class One (α : Type u) where
-    one : α
-export One (one)
-
-instance [One α] : OfNat α (nat_lit 1) where
-    ofNat := one
-
 export Zero (zero)
 
 instance [Zero α] : OfNat α (nat_lit 0) where

tests/lean/run/alg.lean

@@ -14,12 +14,6 @@ class CommSemigroup (α : Type u) extends Semigroup α where
 instance [CommSemigroup α] : MulComm α where
   mul_comm := CommSemigroup.mul_comm
 
-class One (α : Type u) where
-  one : α
-
-instance [One α] : OfNat α (nat_lit 1) where
-  ofNat := One.one
-
 class Monoid (α : Type u) extends Semigroup α, One α where
   one_mul (a : α) : 1 * a = a
   mul_one (a : α) : a * 1 = a

tests/lean/run/binop_binrel_perf_issue.lean

@@ -22,18 +22,6 @@ end Set
 
 end Mathlib.Init.Set
 
-section Mathlib.Init.ZeroOne
-
-set_option autoImplicit true
-
-class One (α : Type u) where
-  one : α
-
-instance (priority := 300) One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
-  ofNat := ‹One α›.1
-
-end Mathlib.Init.ZeroOne
-
 section Mathlib.Init.Function
 
 universe u₁ u₂

tests/lean/run/grind_canon_insts.lean

@@ -18,12 +18,6 @@ class CommSemigroup (α : Type u) extends Semigroup α where
 instance [CommSemigroup α] : MulComm α where
   mul_comm := CommSemigroup.mul_comm
 
-class One (α : Type u) where
-  one : α
-
-instance [One α] : OfNat α (nat_lit 1) where
-  ofNat := One.one
-
 class Monoid (α : Type u) extends Semigroup α, One α where
   one_mul (a : α) : 1 * a = a
   mul_one (a : α) : a * 1 = a

tests/lean/run/grind_regression.lean

@@ -640,9 +640,6 @@ end
 
 section
 
-class One (α) where one : α
-instance [One α] : OfNat α 1 where ofNat := One.one
-
 class Inv (α) where inv : α → α
 postfix:max "⁻¹" => Inv.inv
 

tests/lean/run/grind_shelf.lean

@@ -1,9 +1,3 @@
-class One (α : Type u) where
-  one : α
-
-instance (priority := 300) One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
-  ofNat := ‹One α›.1
-
 class Shelf (α : Type u) where
   act : α → α → α
   self_distrib : ∀ {x y z : α}, act x (act y z) = act (act x y) (act x z)

tests/lean/run/infoFromFailure.lean

@@ -0,0 +1,43 @@
+
+
+def A.foo {α : Type} [Add α] (a : α) : α × α :=
+(a, a + a)
+
+def B.foo {α : Type} (a : α) : α × α :=
+(a, a)
+
+open A
+open B
+
+set_option trace.Meta.synthInstance true
+
+/--
+info: B.foo "hello" : String × String
+---
+info: [Meta.synthInstance] ❌️ Add String
+  [Meta.synthInstance] new goal Add String
+    [Meta.synthInstance.instances] #[@Lean.Grind.CommRing.toAdd]
+  [Meta.synthInstance] ✅️ apply @Lean.Grind.CommRing.toAdd to Add String
+    [Meta.synthInstance.tryResolve] ✅️ Add String ≟ Add String
+    [Meta.synthInstance] no instances for Lean.Grind.CommRing String
+      [Meta.synthInstance.instances] #[]
+  [Meta.synthInstance] result <not-available>
+-/
+#guard_msgs in
+-- `foo` is overloaded, the case `A.foo` is discarded because we don't have an instance `[Add String]`.
+-- However, we still want to see the trace since we used trace.Meta.synthInstance
+#check foo "hello"
+
+/--
+info: [Meta.synthInstance] ❌️ Add Bool
+  [Meta.synthInstance] new goal Add Bool
+    [Meta.synthInstance.instances] #[@Lean.Grind.CommRing.toAdd]
+  [Meta.synthInstance] ✅️ apply @Lean.Grind.CommRing.toAdd to Add Bool
+    [Meta.synthInstance.tryResolve] ✅️ Add Bool ≟ Add Bool
+    [Meta.synthInstance] no instances for Lean.Grind.CommRing Bool
+      [Meta.synthInstance.instances] #[]
+  [Meta.synthInstance] result <not-available>
+-/
+#guard_msgs in
+theorem ex : foo true = (true, true) :=
+rfl

tests/lean/run/linearCategory_perf_issue.lean

@@ -1,15 +1,5 @@
 universe u v w v₁ v₂ v₃ u₁ u₂ u₃
 
-section Mathlib.Algebra.Group.ZeroOne
-
-class One (α : Type u) where
-  one : α
-
-instance (priority := 300) One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
-  ofNat := ‹One α›.1
-
-end Mathlib.Algebra.Group.ZeroOne
-
 section Mathlib.Algebra.Group.Defs
 
 class HSMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where

tests/lean/run/mathlibetaissue.lean

@@ -42,15 +42,6 @@ class RatCast (K : Type u) where
 
 end Std.Classes.RatCast
 
-section Mathlib.Init.ZeroOne
-
-class One (α : Type u) where
-  one : α
-instance One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
-  ofNat := ‹One α›.1
-
-end Mathlib.Init.ZeroOne
-
 section Mathlib.Algebra.Group.Defs
 
 class Inv (α : Type u) where

tests/lean/run/matrix.lean

@@ -1,14 +1,3 @@
-/-
-Helper classes for Lean 3 users
--/
-class One (α : Type u) where
-  one : α
-
-instance [OfNat α (nat_lit 1)] : One α where
-  one := 1
-
-instance [One α] : OfNat α (nat_lit 1) where
-  ofNat := One.one
 
 /- Simple Matrix -/
 

tests/lean/run/ofNatNormNum.lean

@@ -6,12 +6,6 @@ export OfNatSound (ofNat_add)
 theorem ex1 {α : Type u} [Add α] [(n : Nat) → OfNat α n] [OfNatSound α] : (10000000 : α) + 10000000 = 20000000 :=
   ofNat_add ..
 
-class One (α : Type u) where
-  one : α
-
-instance [One α] : OfNat α (nat_lit 1) where
-  ofNat := One.one
-
 -- Some example structure
 class S (α : Type u) extends Add α, Mul α, Zero α, One α where
   add_assoc (a b c : α)    : a + b + c = a + (b + c)

tests/lean/run/proofAsSorry.lean

@@ -1,10 +1,11 @@
 set_option debug.proofAsSorry true
+set_option pp.mvars false
 
 /--
 error: type mismatch
   rfl
 has type
-  ?m.156 = ?m.156 : Prop
+  ?_ = ?_ : Prop
 but is expected to have type
   2 + 2 = 5 : Prop
 -/

tests/lean/run/regressions3210.lean

@@ -5,14 +5,6 @@ example : ¬1 % 2 = 0 := by
 
 universe u
 
-class One (α : Type u) where
-  one : α
-
-instance One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
-  ofNat := ‹One α›.1
-instance One.ofOfNat1 {α} [OfNat α (nat_lit 1)] : One α where
-  one := 1
-
 example : Not
   (@Eq.{1} Nat
     (@HMod.hMod.{0, 0, 0} Nat Nat Nat (@instHMod.{0} Nat Nat.instMod)

tests/lean/run/structWithAlgTCSynth.lean

@@ -85,16 +85,6 @@ end Quotient
 
 end Mathlib.Data.Quot
 
-section Mathlib.Init.ZeroOne
-
-class One (α : Type u) where
-  one : α
-
-instance One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
-  ofNat := ‹One α›.1
-
-section Mathlib.Init.ZeroOne
-
 section Mathlib.Logic.Function.Basic
 
 namespace Function

tests/lean/run/unfoldPartialRegression.lean

@@ -1,13 +1,5 @@
 universe u
 
-class One (α : Type u) where
-  one : α
-
-instance (priority := 300) One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
-  ofNat := ‹One α›.1
-instance (priority := 200) One.ofOfNat1 {α} [OfNat α (nat_lit 1)] : One α where
-  one := 1
-
 @[match_pattern] def bit0 {α : Type u} [Add α] (a : α) : α := a + a
 
 @[match_pattern] def bit1 {α : Type u} [One α] [Add α] (a : α) : α := bit0 a + 1

tests/lean/synthorder.lean

@@ -17,7 +17,6 @@ instance : Foo (Option A) A where
 
 
 
-class One (α : Type)
 class Two (α) [One α]
 class TwoHalf (α) [One α] extends Two α
 class Three (α : Type) (β : outParam Type) [One β] [Two β]