fix tests

cleanup

cleanup tests

cleanup tests

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 _)
 

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 _)

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 : α
 

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

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

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

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

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
 

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

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

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

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 _]

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 : α
 

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

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 α

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 : α
 

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

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)

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

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 : α
 

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 -/

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

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 :=

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
 

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

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

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 : α
 

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

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 : α