chore: remove instBEqNat, which is redundant with instBEqOfDecidableEq but not defeq (#5694)

src/Init/Data/Nat/Basic.lean

@@ -131,7 +131,7 @@ theorem or_exists_add_one : p 0 ∨ (Exists fun n => p (n + 1)) ↔ Exists p :=
 @[simp] theorem blt_eq : (Nat.blt x y = true) = (x < y) := propext <| Iff.intro Nat.le_of_ble_eq_true Nat.ble_eq_true_of_le
 
 instance : LawfulBEq Nat where
-  eq_of_beq h := Nat.eq_of_beq_eq_true h
+  eq_of_beq h := by simpa using h
   rfl := by simp [BEq.beq]
 
 theorem beq_eq_true_eq (a b : Nat) : ((a == b) = true) = (a = b) := by simp

src/Init/Prelude.lean

@@ -1592,9 +1592,6 @@ def Nat.beq : (@& Nat) → (@& Nat) → Bool
   | succ _, zero   => false
   | succ n, succ m => beq n m
 
-instance : BEq Nat where
-  beq := Nat.beq
-
 theorem Nat.eq_of_beq_eq_true : {n m : Nat} → Eq (beq n m) true → Eq n m
   | zero,   zero,   _ => rfl
   | zero,   succ _, h => Bool.noConfusion h

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean

@@ -149,11 +149,14 @@ private def mkSubNat (x y : Expr) : Expr :=
 private def mkEqNat (x y : Expr) : Expr :=
   mkAppN (mkConst ``Eq [levelOne]) #[mkConst ``Nat, x, y]
 
-private def mkBeqNat (x y : Expr) : Expr :=
-  mkAppN (mkConst ``BEq.beq [levelZero]) #[mkConst ``Nat, mkConst ``instBEqNat, x, y]
+private def mkBEqNatInstance : Expr :=
+  mkAppN (mkConst ``instBEqOfDecidableEq [levelZero]) #[mkConst ``Nat, mkConst ``instDecidableEqNat []]
+
+private def mkBEqNat (x y : Expr) : Expr :=
+  mkAppN (mkConst ``BEq.beq [levelZero]) #[mkConst ``Nat, mkBEqNatInstance, x, y]
 
 private def mkBneNat (x y : Expr) : Expr :=
-  mkAppN (mkConst ``bne [levelZero]) #[mkConst ``Nat, mkConst ``instBEqNat, x, y]
+  mkAppN (mkConst ``bne [levelZero]) #[mkConst ``Nat, mkBEqNatInstance, x, y]
 
 private def mkLENat (x y : Expr) : Expr :=
   mkAppN (.const ``LE.le [levelZero]) #[mkConst ``Nat, mkConst ``instLENat, x, y]
@@ -250,7 +253,7 @@ builtin_simproc [simp, seval] reduceBeqDiff ((_ : Nat) == _) := fun e => do
     return .done  { expr := mkConst ``false, proof? := some q, cache := true }
   | some (.eq u v p) =>
     let q := mkAppN (mkConst ``Nat.Simproc.beqEqOfEqEq) #[x, y, u, v, p]
-    return .visit { expr := mkBeqNat u v, proof? := some q, cache := true }
+    return .visit { expr := mkBEqNat u v, proof? := some q, cache := true }
 
 builtin_simproc [simp, seval] reduceBneDiff ((_ : Nat) != _) := fun e => do
   unless e.isAppOfArity ``bne 4 do

tests/lean/eagerCoeExpansion.lean.expected.out

@@ -4,9 +4,18 @@ def r : Nat → Prop :=
 fun a => if (a == 0) = true then (a != 1) = true else (a != 2) = true
 def r : Nat → Prop :=
 fun (a : Nat) =>
-  @ite.{1} Prop (@Eq.{1} Bool (@BEq.beq.{0} Nat instBEqNat a (@OfNat.ofNat.{0} Nat 0 (instOfNatNat 0))) Bool.true)
-    (instDecidableEqBool (@BEq.beq.{0} Nat instBEqNat a (@OfNat.ofNat.{0} Nat 0 (instOfNatNat 0))) Bool.true)
-    (@Eq.{1} Bool (@bne.{0} Nat instBEqNat a (@OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))) Bool.true)
-    (@Eq.{1} Bool (@bne.{0} Nat instBEqNat a (@OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))) Bool.true)
+  @ite.{1} Prop
+    (@Eq.{1} Bool
+      (@BEq.beq.{0} Nat (@instBEqOfDecidableEq.{0} Nat instDecidableEqNat) a (@OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)))
+      Bool.true)
+    (instDecidableEqBool
+      (@BEq.beq.{0} Nat (@instBEqOfDecidableEq.{0} Nat instDecidableEqNat) a (@OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)))
+      Bool.true)
+    (@Eq.{1} Bool
+      (@bne.{0} Nat (@instBEqOfDecidableEq.{0} Nat instDecidableEqNat) a (@OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)))
+      Bool.true)
+    (@Eq.{1} Bool
+      (@bne.{0} Nat (@instBEqOfDecidableEq.{0} Nat instDecidableEqNat) a (@OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)))
+      Bool.true)
 def s : Option Nat :=
 HOrElse.hOrElse (myFun.f 3) fun x => myFun.f 4

tests/lean/phashmap_inst_coherence.lean.expected.out

@@ -3,6 +3,6 @@ phashmap_inst_coherence.lean:12:53-12:54: error: application type mismatch
 argument
   m
 has type
-  @PersistentHashMap Nat Nat instBEqNat instHashableNat : Type
+  @PersistentHashMap Nat Nat instBEqOfDecidableEq instHashableNat : Type
 but is expected to have type
-  @PersistentHashMap Nat Nat instBEqNat natDiffHash : Type
+  @PersistentHashMap Nat Nat instBEqOfDecidableEq natDiffHash : Type