From c7c9943c87e84437a8b80f157d48b3514f6b2661 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Tue, 3 Sep 2024 14:54:09 +1000
Subject: [PATCH] fix tests

cleanup

cleanup tests

cleanup tests
---
 src/Init/Data/Fin/Basic.lean                  |  3 ---
 src/Init/Data/NeZero.lean                     | 10 ---------
 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/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 -----
 29 files changed, 21 insertions(+), 141 deletions(-)

diff --git a/src/Init/Data/Fin/Basic.lean b/src/Init/Data/Fin/Basic.lean
index f64f26ad1c70..31a73bc83723 100644
--- a/src/Init/Data/Fin/Basic.lean
+++ b/src/Init/Data/Fin/Basic.lean
@@ -141,9 +141,6 @@ instance : ShiftLeft (Fin n) where
 instance : ShiftRight (Fin n) where
   shiftRight := Fin.shiftRight
 
--- instance instOfNat : OfNat (Fin (n+1)) i where
---   ofNat := Fin.ofNat' i (zero_lt_succ n)
-
 instance instOfNat {n : Nat} [NeZero n] {i : Nat} : OfNat (Fin (no_index n)) i where
   ofNat := Fin.ofNat' i (pos_of_neZero _)
 
diff --git a/src/Init/Data/NeZero.lean b/src/Init/Data/NeZero.lean
index 555d0c54bfdf..4502ccbfee19 100644
--- a/src/Init/Data/NeZero.lean
+++ b/src/Init/Data/NeZero.lean
@@ -36,13 +36,3 @@ theorem neZero_iff {n : R} : NeZero n ↔ n ≠ 0 :=
 
 @[simp] theorem neZero_zero_iff_false {α : Type _} [Zero α] : NeZero (0 : α) ↔ False :=
   ⟨fun h ↦ h.ne rfl, fun h ↦ h.elim⟩
-
--- theorem not_neZero {n : R} : ¬NeZero n ↔ n = 0 := by simp [neZero_iff]
-
--- namespace NeZero
-
--- instance succ {n : Nat} : NeZero (n + 1) := ⟨n.succ_ne_zero⟩
-
--- end NeZero
-
--- theorem Nat.pos_of_neZero (n : Nat) [NeZero n] : 0 < n := Nat.pos_of_ne_zero (NeZero.ne _)
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/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 : α