chore: more cleanup

opencompl · Jul 24, 2024 · b6e0b32 · b6e0b32
1 parent fce4987
commit b6e0b32
Showing 1 changed file with 3 additions and 11 deletions.
diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean
@@ -486,12 +486,7 @@ theorem ushiftRight_rec_eq (x : BitVec w₁) (y : BitVec w₂) (n : Nat) :
   case zero =>
     ext i
     simp only [ushiftRight_rec_zero, twoPow_zero, Nat.reduceAdd, truncate_one_eq_ofBool_getLsb]
-    have heq : (y &&& 1#w₂) = zeroExtend w₂ (ofBool (y.getLsb 0)) := by
-      ext i
-      by_cases h : (↑i : Nat) = 0
-      · simp [h, Bool.and_comm]
-      · simp [h]; omega
-    simp [heq]
+    rw [and_one]
   case succ n ih =>
     simp
     rw [ih]
@@ -584,11 +579,8 @@ theorem sshiftRightRec_eq (x : BitVec w₁) (y : BitVec w₂) (n : Nat) :
   induction n generalizing x y
   case zero =>
     ext i
-    simp only [ushiftRight_rec_zero, twoPow_zero, Nat.reduceAdd, truncate_one_eq_ofBool_getLsb]
-    have heq : (y &&& 1#w₂) = zeroExtend w₂ (ofBool (y.getLsb 0)) := by
-      ext i
-      by_cases h : (↑i : Nat) = 0 <;> simp [h, Bool.and_comm]
-    simp [heq]
+    simp  [ushiftRight_rec_zero, twoPow_zero, Nat.reduceAdd, truncate_one_eq_ofBool_getLsb]
+    rw [and_one]
   case succ n ih =>
     simp
     by_cases h : y.getLsb (n + 1) <;> simp [h]