chore: cleanup

src/Init/Data/BitVec/Bitblast.lean

@@ -607,7 +607,6 @@ structure DivModState.LawfulShiftSubtract (w wr wn : Nat) (n d : BitVec w) (qr :
   /-- Only perform a round of shift-subtract if we have dividend bits. -/
   hwn_lt : 0 < wn
 
-
 /--
 In the shift subtract input, the dividend is at least one bit long (`wn > 0`), so
 the remainder has bits to be computed (`wr < w`).
@@ -642,7 +641,6 @@ private theorem mul_two_add_lt_two_pow_of_lt_two_pow_of_lt_two {n b k w : Nat}
   have : 2^(k + 1) ≤ 2 ^w := Nat.pow_le_pow_of_le_right (by decide) (by assumption)
   omega
 
-
 /-- `x.shiftConcat b` does not overflow if `x < 2^k` for `k < w`, and so
 `x.shiftConcat b |>.toNat = x.toNat * 2 + b.toNat`. -/
 theorem toNat_shiftConcat_eq_of_lt_of_lt_two_pow {x : BitVec w} {b : Bool} {k : Nat}
@@ -790,32 +788,9 @@ def divSubtractShiftProof (qr : DivModState w) (h : qr.LawfulShiftSubtract  wr w
         h.hdiv, Nat.mul_add]
       bv_omega
 
-/-! ### Core divsion algorithm
-
-We have three widths at play:
-
-- `w`, the total bitwidth
-- `wr`, the effective bitwidth of the reminder
-- `wn`, the effective bitwidth of the dividend.
-
-We have the invariant that wn + wr = w.
-
-See that when `divRec` is called with a `DivModState.Lawful h`, we know that:
-
-  - r < [2^wr = 2^(w - wn)]
-    which allows us to safely shift left, since it is of length n.
-    In particular, since 'wn' decreases in the course of the recursion,
-    will will allow larger and larger values, and at the step where 'wn = 0',
-    we will have `r < 2^w`, which is no longer sufficient to allow for a shift left.
-    Thus, at this step, we will stop and return a full remainder.
-    So, the remainder is morally of length `w - wn`.
-  - d > 0
-  - r < d.
-
-TODO: link to previous definition for proof engineering notes.
--/
+/-! ### Core divsion algorithm circuit -/
 
-/-- A recursive definition of division for bitblasting, in terms of a shift-subtraction circuit.  -/
+/-- A recursive definition of division for bitblasting, in terms of a shift-subtraction circuit. -/
 def divRec (w wr wn : Nat) (n d : BitVec w) (qr : DivModState w) :
     DivModState w :=
   match wn with
@@ -912,16 +887,15 @@ theorem sshiftRightRec_eq (x : BitVec w₁) (y : BitVec w₂) (n : Nat) :
   induction n generalizing x y
   case zero =>
     ext i
-    simp only [sshiftRightRec_zero_eq, and_one_eq_zeroExtend_ofBool_getLsb, sshiftRight_eq',
-      toNat_truncate, toNat_ofBool, getLsb_sshiftRight, Nat.reduceAdd, truncate_one]
+    simp [twoPow_zero, Nat.reduceAdd, and_one_eq_zeroExtend_ofBool_getLsb, truncate_one]
   case succ n ih =>
     simp only [sshiftRightRec_succ_eq, and_twoPow, ih]
     by_cases h : y.getLsb (n + 1)
     · rw [zeroExtend_truncate_succ_eq_zeroExtend_truncate_or_twoPow_of_getLsb_true h,
         sshiftRight'_or_of_and_eq_zero (by simp), h]
       simp
     · rw [zeroExtend_truncate_succ_eq_zeroExtend_truncate_of_getLsb_false (i := n + 1)
-        (by simp only [h])]
+        (by simp [h])]
       simp [h]
 
 /--

src/Init/Data/BitVec/Lemmas.lean

@@ -1486,7 +1486,6 @@ theorem le_iff_not_lt {x y : BitVec w} : (¬ x < y) ↔ y ≤ x := by
   constructor <;>
     (intro h; simp only [lt_def, Nat.not_lt, le_def] at h ⊢; omega)
 
-
 /-! ### intMax -/
 
 /-- The bitvector of width `w` that has the largest value when interpreted as an integer. -/
@@ -1831,7 +1830,7 @@ theorem getLsb_replicate {n w : Nat} (x : BitVec w) :
 
 /-! ### Lemmas about non-overflowing computations -/
 
-/-- If `y ≤ x`, then `x - y` does not overflow, and `(x - y).toNat = x.toNat - y.toNat`. -/
+/-- If `y ≤ x`, then `x - y` does not overflow, thus `(x - y).toNat = x.toNat - y.toNat`. -/
 theorem toNat_sub_eq_toNat_sub_toNat_of_le {x y : BitVec w} (h : y ≤ x) :
     (x - y).toNat = x.toNat - y.toNat := by
   rw [BitVec.le_def] at h