fix(data/bool): remove simp attribute from commutativity lemmas (#2027)

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

Author: gebner

src/data/bool.lean

@@ -81,23 +81,23 @@ theorem eq_tt_of_ne_ff : ∀ {a : bool}, a ≠ ff → a = tt := dec_trivial
 
 theorem eq_ff_of_ne_tt : ∀ {a : bool}, a ≠ tt → a = ff := dec_trivial
 
-@[simp] theorem bor_comm : ∀ a b, a || b = b || a := dec_trivial
+theorem bor_comm : ∀ a b, a || b = b || a := dec_trivial
 
 @[simp] theorem bor_assoc : ∀ a b c, (a || b) || c = a || (b || c) := dec_trivial
 
-@[simp] theorem bor_left_comm : ∀ a b c, a || (b || c) = b || (a || c) := dec_trivial
+theorem bor_left_comm : ∀ a b c, a || (b || c) = b || (a || c) := dec_trivial
 
 theorem bor_inl {a b : bool} (H : a) : a || b :=
 by simp [H]
 
 theorem bor_inr {a b : bool} (H : b) : a || b :=
 by simp [H]
 
-@[simp] theorem band_comm : ∀ a b, a && b = b && a := dec_trivial
+theorem band_comm : ∀ a b, a && b = b && a := dec_trivial
 
 @[simp] theorem band_assoc : ∀ a b c, (a && b) && c = a && (b && c) := dec_trivial
 
-@[simp] theorem band_left_comm : ∀ a b c, a && (b && c) = b && (a && c) := dec_trivial
+theorem band_left_comm : ∀ a b c, a && (b && c) = b && (a && c) := dec_trivial
 
 theorem band_elim_left : ∀ {a b : bool}, a && b → a := dec_trivial
 
@@ -113,9 +113,9 @@ theorem eq_tt_of_bnot_eq_ff : ∀ {a : bool}, bnot a = ff → a = tt := dec_triv
 
 theorem eq_ff_of_bnot_eq_tt : ∀ {a : bool}, bnot a = tt → a = ff := dec_trivial
 
-@[simp] theorem bxor_comm : ∀ a b, bxor a b = bxor b a := dec_trivial
+theorem bxor_comm : ∀ a b, bxor a b = bxor b a := dec_trivial
 @[simp] theorem bxor_assoc : ∀ a b c, bxor (bxor a b) c = bxor a (bxor b c) := dec_trivial
-@[simp] theorem bxor_left_comm : ∀ a b c, bxor a (bxor b c) = bxor b (bxor a c) := dec_trivial
+theorem bxor_left_comm : ∀ a b c, bxor a (bxor b c) = bxor b (bxor a c) := dec_trivial
 @[simp] theorem bxor_bnot_left : ∀ a, bxor (!a) a = tt := dec_trivial
 @[simp] theorem bxor_bnot_right : ∀ a, bxor a (!a) = tt := dec_trivial
 @[simp] theorem bxor_bnot_bnot : ∀ a b, bxor (!a) (!b) = bxor a b := dec_trivial

src/data/int/basic.lean

@@ -19,7 +19,7 @@ meta instance : has_to_format ℤ := ⟨λ z, to_string z⟩
 meta instance : has_reflect ℤ := by tactic.mk_has_reflect_instance
 
 attribute [simp] int.coe_nat_add int.coe_nat_mul int.coe_nat_zero int.coe_nat_one int.coe_nat_succ
-attribute [simp] int.of_nat_eq_coe
+attribute [simp] int.of_nat_eq_coe int.bodd
 
 @[simp] theorem add_def {a b : ℤ} : int.add a b = a + b := rfl
 @[simp] theorem mul_def {a b : ℤ} : int.mul a b = a * b := rfl
@@ -810,9 +810,11 @@ lemma units_inv_eq_self (u : units ℤ) : u⁻¹ = u :=
 @[simp] lemma bodd_one : bodd 1 = tt := rfl
 @[simp] lemma bodd_two : bodd 2 = ff := rfl
 
+@[simp, elim_cast] lemma bodd_coe (n : ℕ) : int.bodd n = nat.bodd n := rfl
+
 @[simp] lemma bodd_sub_nat_nat (m n : ℕ) : bodd (sub_nat_nat m n) = bxor m.bodd n.bodd :=
 by apply sub_nat_nat_elim m n (λ m n i, bodd i = bxor m.bodd n.bodd); intros;
-  simp [bodd, -of_nat_eq_coe]
+  simp; cases i.bodd; simp
 
 @[simp] lemma bodd_neg_of_nat (n : ℕ) : bodd (neg_of_nat n) = n.bodd :=
 by cases n; simp; refl
@@ -821,10 +823,12 @@ by cases n; simp; refl
 by cases n; simp [has_neg.neg, int.coe_nat_eq, int.neg, bodd, -of_nat_eq_coe]
 
 @[simp] lemma bodd_add (m n : ℤ) : bodd (m + n) = bxor (bodd m) (bodd n) :=
-by cases m with m m; cases n with n n; unfold has_add.add; simp [int.add, bodd, -of_nat_eq_coe]
+by cases m with m m; cases n with n n; unfold has_add.add;
+  simp [int.add, -of_nat_eq_coe, bool.bxor_comm]
 
 @[simp] lemma bodd_mul (m n : ℤ) : bodd (m * n) = bodd m && bodd n :=
-by cases m with m m; cases n with n n; unfold has_mul.mul; simp [int.mul, bodd, -of_nat_eq_coe]
+by cases m with m m; cases n with n n; unfold has_mul.mul;
+  simp [int.mul, -of_nat_eq_coe, bool.bxor_comm]
 
 theorem bodd_add_div2 : ∀ n, cond (bodd n) 1 0 + 2 * div2 n = n
 | (n : ℕ) :=