From 4616617021d72ea6fda50d1c54cef65e7d2b8d1e Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Mon, 2 Sep 2024 15:56:54 +1000
Subject: [PATCH] chore: upstream Zero and NeZero

---
 src/Init/Data.lean                            |  2 +
 src/Init/Data/Fin/Basic.lean                  |  4 +-
 src/Init/Data/Nat/Basic.lean                  |  9 +++++
 src/Init/Data/NeZero.lean                     | 38 +++++++++++++++++++
 src/Init/Data/Zero.lean                       | 17 +++++++++
 src/Init/Prelude.lean                         |  5 +++
 src/Lean/ToExpr.lean                          |  3 +-
 tests/lean/1870.lean                          |  9 -----
 tests/lean/1870.lean.expected.out             |  6 +--
 tests/lean/2178.lean                          |  2 -
 tests/lean/diamond10.lean                     |  3 --
 tests/lean/diamond7.lean                      |  6 ---
 tests/lean/diamond8.lean                      |  3 --
 tests/lean/diamond9.lean                      |  3 --
 tests/lean/isDefEqOffsetBug.lean              |  8 ----
 tests/lean/isDefEqOffsetBug.lean.expected.out |  2 +-
 tests/lean/run/2265.lean                      |  6 +--
 tests/lean/run/2461.lean                      |  3 --
 tests/lean/run/326.lean                       |  2 -
 tests/lean/run/3313.lean                      |  3 --
 tests/lean/run/3807.lean                      |  6 ---
 tests/lean/run/788.lean                       |  1 +
 tests/lean/run/KyleAlg.lean                   |  5 ---
 tests/lean/run/KyleAlgAbbrev.lean             |  2 -
 tests/lean/run/binop_binrel_perf_issue.lean   |  6 ---
 tests/lean/run/dsimpNatLitIssue.lean          |  6 ---
 tests/lean/run/fin_two_pow.lean               |  5 +++
 tests/lean/run/linearCategory_perf_issue.lean |  6 ---
 tests/lean/run/mathlibetaissue.lean           |  4 --
 tests/lean/run/matrix.lean                    |  9 -----
 tests/lean/run/ofNatNormNum.lean              |  6 ---
 tests/lean/run/ofNat_class.lean               |  2 +-
 tests/lean/run/scopedunifhint.lean            | 22 ++++++-----
 tests/lean/run/structWithAlgTCSynth.lean      |  6 ---
 tests/lean/run/synthInstsIssue.lean           | 12 ------
 tests/lean/run/unfoldPartialRegression.lean   |  6 ---
 36 files changed, 101 insertions(+), 137 deletions(-)
 create mode 100644 src/Init/Data/NeZero.lean
 create mode 100644 src/Init/Data/Zero.lean
 create mode 100644 tests/lean/run/fin_two_pow.lean

diff --git a/src/Init/Data.lean b/src/Init/Data.lean
index 8aceacd4189d..3276803b6a9c 100644
--- a/src/Init/Data.lean
+++ b/src/Init/Data.lean
@@ -39,3 +39,5 @@ import Init.Data.BEq
 import Init.Data.Subtype
 import Init.Data.ULift
 import Init.Data.PLift
+import Init.Data.Zero
+import Init.Data.NeZero
diff --git a/src/Init/Data/Fin/Basic.lean b/src/Init/Data/Fin/Basic.lean
index cab7b21a776b..31a73bc83723 100644
--- a/src/Init/Data/Fin/Basic.lean
+++ b/src/Init/Data/Fin/Basic.lean
@@ -141,8 +141,8 @@ instance : ShiftLeft (Fin n) where
 instance : ShiftRight (Fin n) where
   shiftRight := Fin.shiftRight
 
-instance instOfNat : OfNat (Fin (no_index (n+1))) i where
-  ofNat := Fin.ofNat i
+instance instOfNat {n : Nat} [NeZero n] {i : Nat} : OfNat (Fin (no_index n)) i where
+  ofNat := Fin.ofNat' i (pos_of_neZero _)
 
 instance : Inhabited (Fin (no_index (n+1))) where
   default := 0
diff --git a/src/Init/Data/Nat/Basic.lean b/src/Init/Data/Nat/Basic.lean
index 706b2a245e09..de6517016b55 100644
--- a/src/Init/Data/Nat/Basic.lean
+++ b/src/Init/Data/Nat/Basic.lean
@@ -5,6 +5,8 @@ Authors: Floris van Doorn, Leonardo de Moura
 -/
 prelude
 import Init.SimpLemmas
+import Init.Data.NeZero
+
 set_option linter.missingDocs true -- keep it documented
 universe u
 
@@ -356,6 +358,8 @@ theorem eq_zero_or_pos : ∀ (n : Nat), n = 0 ∨ n > 0
 
 protected theorem pos_of_ne_zero {n : Nat} : n ≠ 0 → 0 < n := (eq_zero_or_pos n).resolve_left
 
+theorem pos_of_neZero (n : Nat) [NeZero n] : 0 < n := Nat.pos_of_ne_zero (NeZero.ne _)
+
 theorem lt.base (n : Nat) : n < succ n := Nat.le_refl (succ n)
 
 theorem lt_succ_self (n : Nat) : n < succ n := lt.base n
@@ -714,6 +718,8 @@ protected theorem zero_ne_one : 0 ≠ (1 : Nat) :=
 
 theorem succ_ne_zero (n : Nat) : succ n ≠ 0 := by simp
 
+instance {n : Nat} : NeZero (succ n) := ⟨succ_ne_zero n⟩
+
 /-! # mul + order -/
 
 theorem mul_le_mul_left {n m : Nat} (k : Nat) (h : n ≤ m) : k * n ≤ k * m :=
@@ -784,6 +790,9 @@ theorem pos_pow_of_pos {n : Nat} (m : Nat) (h : 0 < n) : 0 < n^m :=
   | zero => cases h
   | succ n => simp [Nat.pow_succ]
 
+instance {n m : Nat} [NeZero n] : NeZero (n^m) :=
+  ⟨Nat.ne_zero_iff_zero_lt.mpr (Nat.pos_pow_of_pos m (pos_of_neZero _))⟩
+
 /-! # min/max -/
 
 /--
diff --git a/src/Init/Data/NeZero.lean b/src/Init/Data/NeZero.lean
new file mode 100644
index 000000000000..4502ccbfee19
--- /dev/null
+++ b/src/Init/Data/NeZero.lean
@@ -0,0 +1,38 @@
+/-
+Copyright (c) 2021 Eric Rodriguez. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Rodriguez
+-/
+prelude
+import Init.Data.Zero
+
+
+/-!
+# `NeZero` typeclass
+
+We create a typeclass `NeZero n` which carries around the fact that `(n : R) ≠ 0`.
+
+## Main declarations
+
+* `NeZero`: `n ≠ 0` as a typeclass.
+-/
+
+
+variable {R : Type _} [Zero R]
+
+/-- A type-class version of `n ≠ 0`.  -/
+class NeZero (n : R) : Prop where
+  /-- The proposition that `n` is not zero. -/
+  out : n ≠ 0
+
+theorem NeZero.ne (n : R) [h : NeZero n] : n ≠ 0 :=
+  h.out
+
+theorem NeZero.ne' (n : R) [h : NeZero n] : 0 ≠ n :=
+  h.out.symm
+
+theorem neZero_iff {n : R} : NeZero n ↔ n ≠ 0 :=
+  ⟨fun h ↦ h.out, NeZero.mk⟩
+
+@[simp] theorem neZero_zero_iff_false {α : Type _} [Zero α] : NeZero (0 : α) ↔ False :=
+  ⟨fun h ↦ h.ne rfl, fun h ↦ h.elim⟩
diff --git a/src/Init/Data/Zero.lean b/src/Init/Data/Zero.lean
new file mode 100644
index 000000000000..36a13fe0ba1e
--- /dev/null
+++ b/src/Init/Data/Zero.lean
@@ -0,0 +1,17 @@
+/-
+Copyright (c) 2021 Gabriel Ebner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gabriel Ebner, Mario Carneiro
+-/
+prelude
+import Init.Core
+
+/-!
+Instances converting between `Zero α` and `OfNat α (nat_lit 0)`.
+-/
+
+instance (priority := 300) Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) where
+  ofNat := ‹Zero α›.1
+
+instance (priority := 200) Zero.ofOfNat0 {α} [OfNat α (nat_lit 0)] : Zero α where
+  zero := 0
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index a690c5c3990d..6cfe43786bd9 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -1304,6 +1304,11 @@ class HShiftRight (α : Type u) (β : Type v) (γ : outParam (Type w)) where
     this is equivalent to `a / 2 ^ b`. -/
   hShiftRight : α → β → γ
 
+/-- A type with a zero element. -/
+class Zero (α : Type u) where
+  /-- The zero element of the type. -/
+  zero : α
+
 /-- 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`. -/
diff --git a/src/Lean/ToExpr.lean b/src/Lean/ToExpr.lean
index 65498ca93889..6e0ee722dd32 100644
--- a/src/Lean/ToExpr.lean
+++ b/src/Lean/ToExpr.lean
@@ -48,7 +48,8 @@ instance : ToExpr (Fin n) where
   toExpr a :=
     let r := mkRawNatLit a.val
     mkApp3 (.const ``OfNat.ofNat [0]) (.app (mkConst ``Fin) (toExpr n)) r
-      (mkApp2 (.const ``Fin.instOfNat []) (mkNatLit (n-1)) r)
+      (mkApp3 (.const ``Fin.instOfNat []) (toExpr n)
+        (.app (.const ``Nat.instNeZeroSucc []) (mkNatLit (n-1))) r)
 
 instance : ToExpr (BitVec n) where
   toTypeExpr := .app (mkConst ``BitVec) (toExpr n)
diff --git a/tests/lean/1870.lean b/tests/lean/1870.lean
index fdd27cdda8d4..734365b486d7 100644
--- a/tests/lean/1870.lean
+++ b/tests/lean/1870.lean
@@ -1,12 +1,3 @@
-class Zero.{u} (α : Type u) where
-  zero : α
-
-instance Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) where
-  ofNat := ‹Zero α›.1
-
-instance Zero.ofOfNat0 {α} [OfNat α (nat_lit 0)] : Zero α where
-  zero := 0
-
 class One (α : Type u) where
   one : α
 
diff --git a/tests/lean/1870.lean.expected.out b/tests/lean/1870.lean.expected.out
index 133830702147..a6f2f8e7561c 100644
--- a/tests/lean/1870.lean.expected.out
+++ b/tests/lean/1870.lean.expected.out
@@ -1,15 +1,15 @@
-1870.lean:21:2-21:35: error: type mismatch
+1870.lean:12:2-12:35: error: type mismatch
   congrArg (@OfNat.ofNat Nat 0) (congrArg (@Zero.toOfNat0 Nat) ?_)
 has type
   OfNat.ofNat 0 = OfNat.ofNat 0 : Prop
 but is expected to have type
   OfNat.ofNat 0 = OfNat.ofNat 1 : Prop
-1870.lean:25:2-25:16: error: tactic 'apply' failed, failed to unify
+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:30:2-30:16: error: tactic 'apply' failed, failed to unify
+1870.lean:21:2-21:16: error: tactic 'apply' failed, failed to unify
   ?f ?a₁ = ?f ?a₂
 with
   OfNat.ofNat 0 = OfNat.ofNat 1
diff --git a/tests/lean/2178.lean b/tests/lean/2178.lean
index 0d6d253690eb..9bfc09da9076 100644
--- a/tests/lean/2178.lean
+++ b/tests/lean/2178.lean
@@ -1,5 +1,3 @@
-class Zero (α : Type u) where
-  zero : α
 class AddZeroClass (M : Type u) extends Zero M, Add M
 class AddMonoid (M : Type u) extends AddZeroClass M where
   nsmul : Nat → M → M := fun _ _ => Zero.zero
diff --git a/tests/lean/diamond10.lean b/tests/lean/diamond10.lean
index 414e51885634..08f658532487 100644
--- a/tests/lean/diamond10.lean
+++ b/tests/lean/diamond10.lean
@@ -1,6 +1,3 @@
-class Zero (A : Type u) where zero : A
-instance {A} [Zero A] : OfNat A (nat_lit 0) := ⟨Zero.zero⟩
-
 class AddMonoid (A : Type u) extends Add A, Zero A
 class Semiring (R : Type u) extends AddMonoid R
 class SubNegMonoid (A : Type u) extends AddMonoid A, Neg A
diff --git a/tests/lean/diamond7.lean b/tests/lean/diamond7.lean
index df96abc8dca1..00a943e3b934 100644
--- a/tests/lean/diamond7.lean
+++ b/tests/lean/diamond7.lean
@@ -39,12 +39,6 @@ class AddSemigroup (α : Type u) extends Add α where
 class AddCommSemigroup (α : Type u) extends AddSemigroup α where
   add_comm (a b : α) : a + b = b + a
 
-class Zero (α : Type u) where
-  zero : α
-
-instance [Zero α] : OfNat α (nat_lit 0) where
-  ofNat := Zero.zero
-
 class AddMonoid (α : Type u) extends AddSemigroup α, Zero α where
   zero_add (a : α) : 0 + a = a
   add_zero (a : α) : a + 0 = a
diff --git a/tests/lean/diamond8.lean b/tests/lean/diamond8.lean
index 790fbfe3edd6..e63af7a241a7 100644
--- a/tests/lean/diamond8.lean
+++ b/tests/lean/diamond8.lean
@@ -1,9 +1,6 @@
 class One (M : Type u) where one : M
 instance {M} [One M] : OfNat M (nat_lit 1) := ⟨One.one⟩
 
-class Zero (A : Type u) where zero : A
-instance {A} [Zero A] : OfNat A (nat_lit 0) := ⟨Zero.zero⟩
-
 class Monoid (M : Type u) extends Mul M, One M where
   mul_one (m : M) : m * 1 = m
 
diff --git a/tests/lean/diamond9.lean b/tests/lean/diamond9.lean
index b7cb4b912f50..990dab58f8db 100644
--- a/tests/lean/diamond9.lean
+++ b/tests/lean/diamond9.lean
@@ -1,6 +1,3 @@
-class Zero (A : Type u) where zero : A
-instance {A} [Zero A] : OfNat A (nat_lit 0) := ⟨Zero.zero⟩
-
 class AddGroup (A : Type u) extends Zero A where
   gsmul : Int → A → A
   gsmul_zero' : ∀ a, gsmul 0 a = 0
diff --git a/tests/lean/isDefEqOffsetBug.lean b/tests/lean/isDefEqOffsetBug.lean
index 5a6a0f200d01..5880c3a3a496 100644
--- a/tests/lean/isDefEqOffsetBug.lean
+++ b/tests/lean/isDefEqOffsetBug.lean
@@ -1,11 +1,3 @@
-class Zero (α : Type u) where
-  zero : α
-
-export Zero (zero)
-
-instance [Zero α] : OfNat α (nat_lit 0) where
-  ofNat := zero
-
 class AddGroup (α : Type u) extends Add α, Zero α, Neg α where
   addAssoc : {a b c : α} → a + b + c = a + (b + c)
   zeroAdd  : {a : α} → 0 + a = a
diff --git a/tests/lean/isDefEqOffsetBug.lean.expected.out b/tests/lean/isDefEqOffsetBug.lean.expected.out
index 1f3153cf0743..14aea3e05373 100644
--- a/tests/lean/isDefEqOffsetBug.lean.expected.out
+++ b/tests/lean/isDefEqOffsetBug.lean.expected.out
@@ -1,4 +1,4 @@
-isDefEqOffsetBug.lean:27:2-27:5: error: type mismatch
+isDefEqOffsetBug.lean:19:2-19:5: error: type mismatch
   rfl
 has type
   0 + 0 = 0 + 0 : Prop
diff --git a/tests/lean/run/2265.lean b/tests/lean/run/2265.lean
index d58eb752cd12..80c93c2fe1e3 100644
--- a/tests/lean/run/2265.lean
+++ b/tests/lean/run/2265.lean
@@ -1,3 +1,3 @@
-class NeZero (n : Nat) : Prop
-theorem mul_div (m n : Nat) [NeZero n] : (m * n) / n = m := sorry
-example [NeZero n] : (m * n) / n = m := by simp [mul_div m _]
+class NeZero' (n : Nat) : Prop
+theorem mul_div (m n : Nat) [NeZero' n] : (m * n) / n = m := sorry
+example [NeZero' n] : (m * n) / n = m := by simp [mul_div m _]
diff --git a/tests/lean/run/2461.lean b/tests/lean/run/2461.lean
index 8863363583cc..70e31d12b8bf 100644
--- a/tests/lean/run/2461.lean
+++ b/tests/lean/run/2461.lean
@@ -1,8 +1,5 @@
 section algebra_hierarchy_classes_to_comm_ring
 
-class Zero (α : Type) where
-  zero : α
-
 class One (α : Type) where
   one : α
 
diff --git a/tests/lean/run/326.lean b/tests/lean/run/326.lean
index 081f1b7e2e99..f10ff6cb815c 100644
--- a/tests/lean/run/326.lean
+++ b/tests/lean/run/326.lean
@@ -1,5 +1,3 @@
-abbrev Zero α := OfNat α (nat_lit 0)
-
 class Monoid (α : Type u) [Zero α] extends Add α where
   zero_add (a : α) : 0 + a = a
   add_zero (a : α) : a + 0 = a
diff --git a/tests/lean/run/3313.lean b/tests/lean/run/3313.lean
index bf2aece65a96..b379cd31a9a6 100644
--- a/tests/lean/run/3313.lean
+++ b/tests/lean/run/3313.lean
@@ -1,6 +1,3 @@
-class Zero (α : Type) where
-  zero : α
-
 class AddCommGroup (α : Type) extends Zero α where
 
 class Ring (α : Type) extends Zero α, AddCommGroup α
diff --git a/tests/lean/run/3807.lean b/tests/lean/run/3807.lean
index d0ef82b39351..7447a7d2b80c 100644
--- a/tests/lean/run/3807.lean
+++ b/tests/lean/run/3807.lean
@@ -93,12 +93,6 @@ section Mathlib.Init.ZeroOne
 
 set_option autoImplicit true
 
-class Zero.{u} (α : Type u) where
-  zero : α
-
-instance (priority := 300) Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) where
-  ofNat := ‹Zero α›.1
-
 class One (α : Type u) where
   one : α
 
diff --git a/tests/lean/run/788.lean b/tests/lean/run/788.lean
index a536bb22a24d..c8c0e749ecae 100644
--- a/tests/lean/run/788.lean
+++ b/tests/lean/run/788.lean
@@ -3,3 +3,4 @@ example : (0 : Nat) = Nat.zero := by
 
 example : (0 : Fin 9) = (Fin.ofNat 0) := by
   simp only [OfNat.ofNat]
+  rfl
diff --git a/tests/lean/run/KyleAlg.lean b/tests/lean/run/KyleAlg.lean
index 9cbff2e761fe..7992c5b69aa1 100644
--- a/tests/lean/run/KyleAlg.lean
+++ b/tests/lean/run/KyleAlg.lean
@@ -21,13 +21,8 @@ export One (one)
 instance [One α] : OfNat α (nat_lit 1) where
     ofNat := one
 
-class Zero (α : Type u) where
-    zero : α
 export Zero (zero)
 
-instance [Zero α] : OfNat α (nat_lit 0) where
-    ofNat := zero
-
 class MulComm (α : Type u) [Mul α] : Prop where
     mulComm : {a b : α} → a * b = b * a
 export MulComm (mulComm)
diff --git a/tests/lean/run/KyleAlgAbbrev.lean b/tests/lean/run/KyleAlgAbbrev.lean
index a8cb2a7a2f2e..0add04690f59 100644
--- a/tests/lean/run/KyleAlgAbbrev.lean
+++ b/tests/lean/run/KyleAlgAbbrev.lean
@@ -21,8 +21,6 @@ export One (one)
 instance [One α] : OfNat α (nat_lit 1) where
     ofNat := one
 
-class Zero (α : Type u) where
-    zero : α
 export Zero (zero)
 
 instance [Zero α] : OfNat α (nat_lit 0) where
diff --git a/tests/lean/run/binop_binrel_perf_issue.lean b/tests/lean/run/binop_binrel_perf_issue.lean
index baacef00b0d8..2aef4272ddba 100644
--- a/tests/lean/run/binop_binrel_perf_issue.lean
+++ b/tests/lean/run/binop_binrel_perf_issue.lean
@@ -26,12 +26,6 @@ section Mathlib.Init.ZeroOne
 
 set_option autoImplicit true
 
-class Zero.{u} (α : Type u) where
-  zero : α
-
-instance (priority := 300) Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) where
-  ofNat := ‹Zero α›.1
-
 class One (α : Type u) where
   one : α
 
diff --git a/tests/lean/run/dsimpNatLitIssue.lean b/tests/lean/run/dsimpNatLitIssue.lean
index 806659a8aece..542c5e3df1e8 100644
--- a/tests/lean/run/dsimpNatLitIssue.lean
+++ b/tests/lean/run/dsimpNatLitIssue.lean
@@ -1,11 +1,5 @@
 variable {R M : Type}
 
-class Zero (α : Type) where
-  zero : α
-
-instance (priority := 300) Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) where
-  ofNat := ‹Zero α›.1
-
 /-- Typeclass for the `⊥` (`\bot`) notation -/
 class Bot (α : Type) where
   /-- The bot (`⊥`, `\bot`) element -/
diff --git a/tests/lean/run/fin_two_pow.lean b/tests/lean/run/fin_two_pow.lean
new file mode 100644
index 000000000000..7d70002e99c0
--- /dev/null
+++ b/tests/lean/run/fin_two_pow.lean
@@ -0,0 +1,5 @@
+-- Check that we can write numerals in `Fin (2^n)`
+-- even though `2^n` is not a definitionally a successor,
+-- via the `NeZero (2^n)` instance.
+
+example {n : Nat} : Fin (2^n) := 0
diff --git a/tests/lean/run/linearCategory_perf_issue.lean b/tests/lean/run/linearCategory_perf_issue.lean
index 7b7c994f91fb..087b6e37f27f 100644
--- a/tests/lean/run/linearCategory_perf_issue.lean
+++ b/tests/lean/run/linearCategory_perf_issue.lean
@@ -2,12 +2,6 @@ universe u v w v₁ v₂ v₃ u₁ u₂ u₃
 
 section Mathlib.Algebra.Group.ZeroOne
 
-class Zero (α : Type u) where
-  zero : α
-
-instance (priority := 300) Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) where
-  ofNat := ‹Zero α›.1
-
 class One (α : Type u) where
   one : α
 
diff --git a/tests/lean/run/mathlibetaissue.lean b/tests/lean/run/mathlibetaissue.lean
index 3c14e6cb7178..ce88e1772377 100644
--- a/tests/lean/run/mathlibetaissue.lean
+++ b/tests/lean/run/mathlibetaissue.lean
@@ -44,10 +44,6 @@ end Std.Classes.RatCast
 
 section Mathlib.Init.ZeroOne
 
-class Zero.{u} (α : Type u) where
-  zero : α
-instance Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) where
-  ofNat := ‹Zero α›.1
 class One (α : Type u) where
   one : α
 instance One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
diff --git a/tests/lean/run/matrix.lean b/tests/lean/run/matrix.lean
index d56b4279769d..74673198a06a 100644
--- a/tests/lean/run/matrix.lean
+++ b/tests/lean/run/matrix.lean
@@ -10,15 +10,6 @@ instance [OfNat α (nat_lit 1)] : One α where
 instance [One α] : OfNat α (nat_lit 1) where
   ofNat := One.one
 
-class Zero (α : Type u) where
-  zero : α
-
-instance [OfNat α (nat_lit 0)] : Zero α where
-  zero := 0
-
-instance [Zero α] : OfNat α (nat_lit 0) where
-  ofNat := Zero.zero
-
 /- Simple Matrix -/
 
 def Matrix (m n : Nat) (α : Type u) : Type u :=
diff --git a/tests/lean/run/ofNatNormNum.lean b/tests/lean/run/ofNatNormNum.lean
index 0ffbf5305065..46629f4b8680 100644
--- a/tests/lean/run/ofNatNormNum.lean
+++ b/tests/lean/run/ofNatNormNum.lean
@@ -6,15 +6,9 @@ export OfNatSound (ofNat_add)
 theorem ex1 {α : Type u} [Add α] [(n : Nat) → OfNat α n] [OfNatSound α] : (10000000 : α) + 10000000 = 20000000 :=
   ofNat_add ..
 
-class Zero (α : Type u) where
-  zero : α
-
 class One (α : Type u) where
   one : α
 
-instance [Zero α] : OfNat α (nat_lit 0) where
-  ofNat := Zero.zero
-
 instance [One α] : OfNat α (nat_lit 1) where
   ofNat := One.one
 
diff --git a/tests/lean/run/ofNat_class.lean b/tests/lean/run/ofNat_class.lean
index 9a925079e274..8e782a1cb96f 100644
--- a/tests/lean/run/ofNat_class.lean
+++ b/tests/lean/run/ofNat_class.lean
@@ -12,4 +12,4 @@ local macro "ofNat_class" Class:ident n:num : command =>
   instance {α} [OfNat α (nat_lit $n)] : $Class α where
     $field:ident := $n)
 
-ofNat_class Zero 0
+ofNat_class Zero' 0
diff --git a/tests/lean/run/scopedunifhint.lean b/tests/lean/run/scopedunifhint.lean
index 0b8cba92ce24..bb8fdd5c9a2e 100644
--- a/tests/lean/run/scopedunifhint.lean
+++ b/tests/lean/run/scopedunifhint.lean
@@ -23,30 +23,32 @@ scoped unif_hint (s : Magma) where
 
 end Algebra
 
+set_option pp.mvars false
+
 def x : Nat := 10
 
 /--
 error: application type mismatch
-  mul ?m.742 x
+  mul ?_ x
 argument
   x
 has type
   Nat : Type
 but is expected to have type
-  ?m.730.α : Type ?u.729
+  ?_.α : Type _
 -/
 #guard_msgs in
 #check mul x x           -- Error: unification hint is not active
 
 /--
 error: application type mismatch
-  mul ?m.833 (x, x)
+  mul ?_ (x, x)
 argument
   (x, x)
 has type
   Nat × Nat : Type
 but is expected to have type
-  ?m.817.α : Type ?u.816
+  ?_.α : Type _
 -/
 #guard_msgs in
 #check mul (x, x) (x, x) -- Error: no unification hint
@@ -55,13 +57,13 @@ local infix:65 (priority := high) "*" => mul
 
 /--
 error: application type mismatch
-  ?m.2484*x
+  ?_*x
 argument
   x
 has type
   Nat : Type
 but is expected to have type
-  ?m.2472.α : Type ?u.2471
+  ?_.α : Type _
 -/
 #guard_msgs in
 #check x*x -- Error: unification hint is not active
@@ -73,13 +75,13 @@ open Algebra -- activate unification hints
 
 /--
 error: application type mismatch
-  ?m.2585*(x, x)
+  ?_*(x, x)
 argument
   (x, x)
 has type
   Nat × Nat : Type
 but is expected to have type
-  ?m.2565.α : Type ?u.2564
+  ?_.α : Type _
 -/
 #guard_msgs in
 #check mul (x, x) (x, x) -- still error
@@ -101,13 +103,13 @@ end Sec1
 
 /--
 error: application type mismatch
-  ?m.2832*(x, x)
+  ?_*(x, x)
 argument
   (x, x)
 has type
   Nat × Nat : Type
 but is expected to have type
-  ?m.2812.α : Type ?u.2811
+  ?_.α : Type _
 -/
 #guard_msgs in
 #check (x, x) * (x, x) -- error, local hint is not active after end of section anymore
diff --git a/tests/lean/run/structWithAlgTCSynth.lean b/tests/lean/run/structWithAlgTCSynth.lean
index d4d16c39d4d6..4fae68c94cf6 100644
--- a/tests/lean/run/structWithAlgTCSynth.lean
+++ b/tests/lean/run/structWithAlgTCSynth.lean
@@ -87,12 +87,6 @@ end Mathlib.Data.Quot
 
 section Mathlib.Init.ZeroOne
 
-class Zero.{u} (α : Type u) where
-  zero : α
-
-instance Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) where
-  ofNat := ‹Zero α›.1
-
 class One (α : Type u) where
   one : α
 
diff --git a/tests/lean/run/synthInstsIssue.lean b/tests/lean/run/synthInstsIssue.lean
index 6681cdb9b6ed..b64601231646 100644
--- a/tests/lean/run/synthInstsIssue.lean
+++ b/tests/lean/run/synthInstsIssue.lean
@@ -4,18 +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.Init.ZeroOne
-
-set_option autoImplicit true
-
-class Zero.{u} (α : Type u) where
-  zero : α
-
-instance (priority := 300) Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) where
-  ofNat := ‹Zero α›.1
-
-end Mathlib.Init.ZeroOne
-
 section Mathlib.Algebra.Group.Defs
 
 universe u v w
diff --git a/tests/lean/run/unfoldPartialRegression.lean b/tests/lean/run/unfoldPartialRegression.lean
index 4e0c0d3bde67..43c71d3ed9c1 100644
--- a/tests/lean/run/unfoldPartialRegression.lean
+++ b/tests/lean/run/unfoldPartialRegression.lean
@@ -1,11 +1,5 @@
 universe u
 
-class Zero (α : Type u) where
-  zero : α
-
-instance (priority := 300) Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) where
-  ofNat := ‹Zero α›.1
-
 class One (α : Type u) where
   one : α