cleanup'

Rob23oba · Rob23oba · commit 2d8da68d4430 · 2025-10-25T17:31:17.000+02:00
diff --git a/tests/lean/grind/experiments/bitvec.lean b/tests/lean/grind/experiments/bitvec.lean
@@ -456,7 +456,7 @@ theorem getElem_ofBool {b : Bool} {h : i < 1}: (ofBool b)[i] = b := by
 @[simp] theorem msb_zero : (0#w).msb = false := by simp [BitVec.msb, getMsbD]
 
 @[simp] theorem msb_one : (1#w).msb = decide (w = 1) := by
-  simp only [BitVec.msb, getMsbD_one, ← Bool.decide_and, decide_eq_decide]
+  simp [BitVec.msb, getMsbD_one, ← Bool.decide_and]
   omega
 
 theorem msb_eq_getLsbD_last (x : BitVec w) :
