Add @[simp]

leanprover · Jan 28, 2025 · d118f7c · d118f7c
1 parent 421a0a7
commit d118f7c
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 1 deletion.
diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
@@ -2634,7 +2634,7 @@ theorem mul_eq_and {a b : BitVec 1} : a * b = a &&& b := by
 
 @[simp] protected theorem neg_mul (x y : BitVec w) : -x * y = -(x * y) := by
   apply eq_of_toInt_eq
-  simp [toInt_mul, toInt_neg, Int.bmod_neg_bmod]
+  simp [toInt_neg]
 
 @[simp] protected theorem mul_neg (x y : BitVec w) : x * -y = -(x * y) := by
   rw [BitVec.mul_comm, BitVec.neg_mul, BitVec.mul_comm]

diff --git a/src/Init/Data/Int/DivModLemmas.lean b/src/Init/Data/Int/DivModLemmas.lean
@@ -1359,6 +1359,7 @@ theorem bmod_natAbs_plus_one (x : Int) (w : 1 < x.natAbs) : bmod x (x.natAbs + 1
     · exact ofNat_nonneg x
     · exact succ_ofNat_pos (x + 1)
 
+@[simp]
 theorem bmod_neg_bmod : bmod (-(bmod x n)) n = bmod (-x) n := by
   apply (bmod_add_cancel_right x).mp
   rw [Int.add_left_neg, ← add_bmod_bmod, Int.add_left_neg]