Apply suggestions from code review

Co-authored-by: Tobias Grosser <[email protected]>
opencompl · Sep 5, 2024 · 29acadb · 29acadb
1 parent 4404af4
commit 29acadb
Showing 1 changed file with 2 additions and 4 deletions.
diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean
@@ -743,11 +743,9 @@ def divSubtractShiftProof (qr : DivModState w) (h : qr.LawfulShiftSubtract  wr w
     case pos.hrWidth => apply toNat_shiftConcat_lt_of_lt_of_lt_two_pow <;> omega
     case pos.hqWidth => apply toNat_shiftConcat_lt_of_lt_of_lt_two_pow <;> omega
     case pos.hdiv =>
-      simp [qr.toNat_shiftRight_sub_one_eq h,
+      simp [qr.toNat_shiftRight_sub_one_eq h, h.hdiv, this,
         toNat_shiftConcat_eq_of_lt_of_lt_two_pow (qr.wr_lt_w h) h.hrWidth,
-        h.hdiv,
-        toNat_shiftConcat_eq_of_lt_of_lt_two_pow (qr.wr_lt_w h) h.hqWidth,
-        this]
+        toNat_shiftConcat_eq_of_lt_of_lt_two_pow (qr.wr_lt_w h) h.hqWidth]
       omega
   · simp only [rltd, ↓reduceIte]
     constructor <;> try bv_omega