chore: remove duplicate instances (#8397)

This PR cleans up many duplicate instances (or, in some cases,
needlessly duplicated `def X := ...; instance Y := X`).

Author: kim-em

src/Init/Classical.lean

@@ -107,8 +107,8 @@ noncomputable def epsilon {α : Sort u} [h : Nonempty α] (p : α → Prop) : α
 theorem epsilon_spec_aux {α : Sort u} (h : Nonempty α) (p : α → Prop) : (∃ y, p y) → p (@epsilon α h p) :=
   (strongIndefiniteDescription p h).property
 
-theorem epsilon_spec {α : Sort u} {p : α → Prop} (hex : ∃ y, p y) : p (@epsilon α (nonempty_of_exists hex) p) :=
-  epsilon_spec_aux (nonempty_of_exists hex) p hex
+theorem epsilon_spec {α : Sort u} {p : α → Prop} (hex : ∃ y, p y) : p (@epsilon α hex.nonempty p) :=
+  epsilon_spec_aux hex.nonempty p hex
 
 theorem epsilon_singleton {α : Sort u} (x : α) : @epsilon α ⟨x⟩ (fun y => y = x) = x :=
   @epsilon_spec α (fun y => y = x) ⟨x, rfl⟩

src/Init/Core.lean

@@ -1212,10 +1212,7 @@ abbrev noConfusionEnum {α : Sort u} {β : Sort v} [inst : DecidableEq β] (f :
 instance : Inhabited Prop where
   default := True
 
-deriving instance Inhabited for NonScalar, PNonScalar, True, ForInStep
-
-theorem nonempty_of_exists {α : Sort u} {p : α → Prop} : Exists (fun x => p x) → Nonempty α
-  | ⟨w, _⟩ => ⟨w⟩
+deriving instance Inhabited for NonScalar, PNonScalar, True
 
 /-! # Subsingleton -/
 
@@ -1389,16 +1386,7 @@ instance Sum.nonemptyLeft [h : Nonempty α] : Nonempty (Sum α β) :=
 instance Sum.nonemptyRight [h : Nonempty β] : Nonempty (Sum α β) :=
   Nonempty.elim h (fun b => ⟨Sum.inr b⟩)
 
-instance {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] : DecidableEq (Sum α β) := fun a b =>
-  match a, b with
-  | Sum.inl a, Sum.inl b =>
-    if h : a = b then isTrue (h ▸ rfl)
-    else isFalse fun h' => Sum.noConfusion h' fun h' => absurd h' h
-  | Sum.inr a, Sum.inr b =>
-    if h : a = b then isTrue (h ▸ rfl)
-    else isFalse fun h' => Sum.noConfusion h' fun h' => absurd h' h
-  | Sum.inr _, Sum.inl _ => isFalse fun h => Sum.noConfusion h
-  | Sum.inl _, Sum.inr _ => isFalse fun h => Sum.noConfusion h
+deriving instance DecidableEq for Sum
 
 end
 

src/Init/Data/Float.lean

@@ -161,8 +161,7 @@ This function does not reduce in the kernel. It is compiled to the C inequality
   match a, b with
   | ⟨a⟩, ⟨b⟩ => floatSpec.decLe a b
 
-instance floatDecLt (a b : Float) : Decidable (a < b) := Float.decLt a b
-instance floatDecLe (a b : Float) : Decidable (a ≤ b) := Float.decLe a b
+attribute [instance] Float.decLt Float.decLe
 
 /--
 Converts a floating-point number to a string.

src/Init/Data/Float32.lean

@@ -145,7 +145,7 @@ Compares two floating point numbers for strict inequality.
 
 This function does not reduce in the kernel. It is compiled to the C inequality operator.
 -/
-@[extern "lean_float32_decLt"] opaque Float32.decLt (a b : Float32) : Decidable (a < b) :=
+@[extern "lean_float32_decLt", instance] opaque Float32.decLt (a b : Float32) : Decidable (a < b) :=
   match a, b with
   | ⟨a⟩, ⟨b⟩ => float32Spec.decLt a b
 
@@ -154,13 +154,10 @@ Compares two floating point numbers for non-strict inequality.
 
 This function does not reduce in the kernel. It is compiled to the C inequality operator.
 -/
-@[extern "lean_float32_decLe"] opaque Float32.decLe (a b : Float32) : Decidable (a ≤ b) :=
+@[extern "lean_float32_decLe", instance] opaque Float32.decLe (a b : Float32) : Decidable (a ≤ b) :=
   match a, b with
   | ⟨a⟩, ⟨b⟩ => float32Spec.decLe a b
 
-instance float32DecLt (a b : Float32) : Decidable (a < b) := Float32.decLt a b
-instance float32DecLe (a b : Float32) : Decidable (a ≤ b) := Float32.decLe a b
-
 /--
 Converts a floating-point number to a string.
 

src/Init/Data/Hashable.lean

@@ -57,9 +57,6 @@ instance : Hashable UInt64 where
 instance : Hashable USize where
   hash n := n.toUInt64
 
-instance : Hashable ByteArray where
-  hash as := as.foldl (fun r a => mixHash r (hash a)) 7
-
 instance : Hashable (Fin n) where
   hash v := v.val.toUInt64
 

src/Init/Data/Int/LemmasAux.lean

@@ -121,7 +121,7 @@ theorem toNat_lt_toNat {n m : Int} (hn : 0 < m) : n.toNat < m.toNat ↔ n < m :=
 /-! ### min and max -/
 
 @[simp] protected theorem min_assoc : ∀ (a b c : Int), min (min a b) c = min a (min b c) := by omega
-instance : Std.Associative (α := Nat) min := ⟨Nat.min_assoc⟩
+instance : Std.Associative (α := Int) min := ⟨Int.min_assoc⟩
 
 @[simp] protected theorem min_self_assoc {m n : Int} : min m (min m n) = min m n := by
   rw [← Int.min_assoc, Int.min_self]
@@ -130,7 +130,7 @@ instance : Std.Associative (α := Nat) min := ⟨Nat.min_assoc⟩
   rw [Int.min_comm m n, ← Int.min_assoc, Int.min_self]
 
 @[simp] protected theorem max_assoc (a b c : Int) : max (max a b) c = max a (max b c) := by omega
-instance : Std.Associative (α := Nat) max := ⟨Nat.max_assoc⟩
+instance : Std.Associative (α := Int) max := ⟨Int.max_assoc⟩
 
 @[simp] protected theorem max_self_assoc {m n : Int} : max m (max m n) = max m n := by
   rw [← Int.max_assoc, Int.max_self]

src/Init/Data/Ord.lean

@@ -849,13 +849,4 @@ comparisons.
 protected def lex' (ord₁ ord₂ : Ord α) : Ord α where
   compare := compareLex ord₁.compare ord₂.compare
 
-/--
-Constructs an order which compares elements of an `Array` in lexicographic order.
--/
-protected def arrayOrd [a : Ord α] : Ord (Array α) where
-  compare x y :=
-    let _ : LT α := a.toLT
-    let _ : BEq α := a.toBEq
-    if List.lex x.toList y.toList then .lt else if x == y then .eq else .gt
-
 end Ord

src/Init/Data/SInt/Basic.lean

@@ -429,8 +429,8 @@ Examples:
 def Int8.decLe (a b : Int8) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec))
 
-instance (a b : Int8) : Decidable (a < b) := Int8.decLt a b
-instance (a b : Int8) : Decidable (a ≤ b) := Int8.decLe a b
+attribute [instance] Int8.decLt Int8.decLe
+
 instance : Max Int8 := maxOfLe
 instance : Min Int8 := minOfLe
 
@@ -800,8 +800,8 @@ Examples:
 def Int16.decLe (a b : Int16) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec))
 
-instance (a b : Int16) : Decidable (a < b) := Int16.decLt a b
-instance (a b : Int16) : Decidable (a ≤ b) := Int16.decLe a b
+attribute [instance] Int16.decLt Int16.decLe
+
 instance : Max Int16 := maxOfLe
 instance : Min Int16 := minOfLe
 
@@ -1187,8 +1187,8 @@ Examples:
 def Int32.decLe (a b : Int32) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec))
 
-instance (a b : Int32) : Decidable (a < b) := Int32.decLt a b
-instance (a b : Int32) : Decidable (a ≤ b) := Int32.decLe a b
+attribute [instance] Int32.decLt Int32.decLe
+
 instance : Max Int32 := maxOfLe
 instance : Min Int32 := minOfLe
 
@@ -1593,8 +1593,8 @@ Examples:
 def Int64.decLe (a b : Int64) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec))
 
-instance (a b : Int64) : Decidable (a < b) := Int64.decLt a b
-instance (a b : Int64) : Decidable (a ≤ b) := Int64.decLe a b
+attribute [instance] Int64.decLt Int64.decLe
+
 instance : Max Int64 := maxOfLe
 instance : Min Int64 := minOfLe
 
@@ -1986,7 +1986,7 @@ Examples:
 def ISize.decLe (a b : ISize) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (a.toBitVec.sle b.toBitVec))
 
-instance (a b : ISize) : Decidable (a < b) := ISize.decLt a b
-instance (a b : ISize) : Decidable (a ≤ b) := ISize.decLe a b
+attribute [instance] ISize.decLt ISize.decLe
+
 instance : Max ISize := maxOfLe
 instance : Min ISize := minOfLe

src/Init/Data/String/Lemmas.lean

@@ -32,22 +32,4 @@ protected theorem ne_of_lt {a b : String} (h : a < b) : a ≠ b := by
   have := String.lt_irrefl a
   intro h; subst h; contradiction
 
-instance ltIrrefl : Std.Irrefl (· < · : Char → Char → Prop) where
-  irrefl := Char.lt_irrefl
-
-instance leRefl : Std.Refl (· ≤ · : Char → Char → Prop) where
-  refl := Char.le_refl
-
-instance leTrans : Trans (· ≤ · : Char → Char → Prop) (· ≤ ·) (· ≤ ·) where
-  trans := Char.le_trans
-
-instance leAntisymm : Std.Antisymm (· ≤ · : Char → Char → Prop) where
-  antisymm _ _ := Char.le_antisymm
-
-instance ltAsymm : Std.Asymm (· < · : Char → Char → Prop) where
-  asymm _ _ := Char.lt_asymm
-
-instance leTotal : Std.Total (· ≤ · : Char → Char → Prop) where
-  total := Char.le_total
-
 end String

src/Init/Data/Sum/Basic.lean

@@ -44,7 +44,6 @@ universe signature in consequence. The `Prop` version is `Or`.
 
 namespace Sum
 
-deriving instance DecidableEq for Sum
 deriving instance BEq for Sum
 
 section get