chore: remove @[simp] from Bool.bne_assoc

src/Init/Data/Bool.lean

@@ -233,15 +233,15 @@ due to `beq_iff_eq`.
 
 theorem not_bne_not : ∀ (x y : Bool), ((!x) != (!y)) = (x != y) := by simp
 
-@[simp] theorem bne_assoc : ∀ (x y z : Bool), ((x != y) != z) = (x != (y != z)) := by decide
+theorem bne_assoc : ∀ (x y z : Bool), ((x != y) != z) = (x != (y != z)) := by decide
 instance : Std.Associative (· != ·) := ⟨bne_assoc⟩
 
 @[simp] theorem bne_left_inj  : ∀ {x y z : Bool}, (x != y) = (x != z) ↔ y = z := by decide
 @[simp] theorem bne_right_inj : ∀ {x y z : Bool}, (x != z) = (y != z) ↔ x = y := by decide
 
 theorem eq_not_of_ne : ∀ {x y : Bool}, x ≠ y → x = !y := by decide
 
-/-! ### coercision related normal forms -/
+/-! ### coercion related normal forms -/
 
 theorem beq_eq_decide_eq [BEq α] [LawfulBEq α] [DecidableEq α] (a b : α) :
     (a == b) = decide (a = b) := by

src/Init/Data/Nat/Bitwise/Lemmas.lean

@@ -591,7 +591,7 @@ protected theorem xor_comm (x y : Nat) : x ^^^ y = y ^^^ x := by
 
 protected theorem xor_assoc (x y z : Nat) : (x ^^^ y) ^^^ z = x ^^^ (y ^^^ z) := by
    apply Nat.eq_of_testBit_eq
-   simp
+   simp [Bool.bne_assoc]
 
 instance : Std.Associative (α := Nat) (· ^^^ ·) where
   assoc := Nat.xor_assoc

tests/lean/bool_simp.lean

@@ -17,7 +17,7 @@ variable (u v w : Prop) [Decidable u] [Decidable v] [Decidable w]
 #check_simp decide (u → False) ~> !decide u
 #check_simp decide (¬u) ~> !decide u
 #check_simp (b = true) ≠ (c = false) ~> b = c
-#check_simp (b != c) != (false != d) ~> b != (c != d)
+#check_simp (b != c) != (false != d) ~> (b != c) != d
 #check_simp (b == false) ≠ (c != d) ~> b = (c != d)
 #check_simp (b = true) ≠ (c = false) ~> b = c
 #check_simp ¬b = !c ~> b = c