chore: finish all TODOs

src/Init/Data/BitVec/Bitblast.lean

@@ -499,8 +499,7 @@ theorem umod_eq_of_mul_add_toNat {d n q r : BitVec w} (hrd : r < d)
   rw [Nat.add_mod, Nat.mul_mod_right] at hdqnr
   simp only [Nat.zero_add, mod_mod] at hdqnr
   replace hrd : r.toNat < d.toNat := by
-    rw [BitVec.lt_def] at hrd
-    exact hrd -- TODO: golf
+    simpa [BitVec.lt_def] using hrd
   rw [Nat.mod_eq_of_lt hrd] at hdqnr
   simp [hdqnr]
 
@@ -592,13 +591,11 @@ theorem DivModState.umod_eq_of_lawful_zero {qr : DivModState w}
 
 /-! ### LawfulShiftSubtract -/
 
-/-!
+/--
 A `LawfulShiftSubtract` is a `Lawful` DivModState that is also a legal input to the shift subtractor.
 So in particular, we must have at least one dividend bit left over `(0 < wn)`
 to perform a round of shift subtraction.
--/
 
-/--
 The input to the shift subtractor is a legal input to `divrem`, and we also need to have an
 input bit to perform shift subtraction on, and thus we need `0 < wn`.
 -/
@@ -665,10 +662,7 @@ theorem toNat_shiftConcat_eq_of_lt_of_lt_two_pow {x : BitVec w} {b : Bool} {k :
         · rcases b <;> decide
         · assumption
     · ext i
-      simp only [getLsb_and, getLsb_shiftLeft, Fin.is_lt, decide_True, Bool.true_and,
-        getLsb_zeroExtend, getLsb_ofBool, getLsb_zero, and_eq_false_imp, and_eq_true, not_eq_true',
-        decide_eq_false_iff_not, Nat.not_lt, decide_eq_true_eq, and_imp]
-      intros hi _ hi'
+      simp
       omega
 
 theorem toNat_shiftConcat_lt_of_lt_of_lt_two_pow {x : BitVec w} {b : Bool} {k : Nat}
@@ -709,7 +703,6 @@ def divSubtractShift (n : BitVec w) (d : BitVec w) (wn : Nat) (qr : DivModState
     r := r' - d -- we subtract to maintain the invariant that `r < d`.
   }
 
--- TODO: find out what hypotheses I need from `qr.Lawful` so it stands alone.
 /-- The value of shifting by `wn - 1` equals shifting by `wn` and grabbing the lsb at `(wn - 1)`. -/
 theorem DivModState.toNat_n_shiftr_wl_minus_one_eq_n_shiftr_wl_plus_nmsb
     (qr : DivModState w) (h : qr.LawfulShiftSubtract wr wn n d):