fixes

Author: f64u

src/Init/Data/BitVec/Folds.lean

@@ -157,7 +157,7 @@ def induction {motive : ∀ {w}, BitVec w → Prop}
     exact nil
   | succ w ih =>
     rw [←cons_msb_setWidth x]
-    exact cons w x.msb (setWidth w x) (ih (setWidth w x))
+    exact cons w _ _ (ih _)
 
 /--
 Induction principle for bitvectors, viewing them as built from `concat` (MSB to LSB).
@@ -221,7 +221,7 @@ theorem foldl_nil : foldl f a nil = a := by
 
 @[simp]
 theorem foldl_cons {x : BitVec w} : foldl f a (cons b x) = foldl f (f a b) x := by
-  simp [foldl, getElem_cons, Nat.foldRev_succ, ↓reduceDIte]
+  simp only [foldl, getElem_cons, Nat.foldRev_succ, ↓reduceDIte]
   congr
   ext
   rw [dif_neg (by omega)]
@@ -244,7 +244,7 @@ theorem foldrIdx_nil : foldrIdx f a nil = a := by
 @[simp]
 theorem foldrIdx_cons {x : BitVec w} :
     foldrIdx f a (cons b x) = f ⟨w, by omega⟩ b (foldrIdx (fun i => f ⟨i.val, by omega⟩) a x) := by
-  simp [foldrIdx, getElem_cons]
+  simp only [foldrIdx, getElem_cons, Nat.fold_succ, ↓reduceDIte]
   congr
   ext
   rw [dif_neg (by omega)]
@@ -264,7 +264,7 @@ theorem foldlIdx_nil : foldlIdx f a nil = a := by
 @[simp]
 theorem foldlIdx_cons {x : BitVec w} :
     foldlIdx f a (cons b x) = foldlIdx (fun acc i => f acc ⟨i.val, by omega⟩) (f a ⟨w, by omega⟩ b) x := by
-  simp [foldlIdx, getElem_cons, Nat.foldRev_succ, ↓reduceDIte]
+  simp only [foldlIdx, getElem_cons, Nat.foldRev_succ, ↓reduceDIte]
   congr
   ext
   rw [dif_neg (by omega)]

src/Init/Data/BitVec/Map.lean

@@ -55,7 +55,7 @@ theorem getLsbD_map (x : BitVec w) (f : Bool → Bool) (i : Nat) :
 theorem map_cons (f : Bool → Bool) (b : Bool) (x : BitVec w) :
     map (cons b x) f = cons (f b) (map x f) := by
   ext i
-  simp [getElem_cons]
+  simp only [getElem_map, getElem_cons]
   split <;> simp
 
 theorem map_map (x : BitVec w) (f g : Bool → Bool) :
@@ -153,7 +153,7 @@ theorem xor_eq_zipWith (x y : BitVec w) : x ^^^ y = zipWith xor x y := by
   simp [getElem_xor]
 
 
-theorem complement_eq_map (x : BitVec w) : ~~~x = x.map not := by
+theorem not_eq_map (x : BitVec w) : ~~~x = x.map not := by
   ext
   simp [getElem_not]
 

src/Init/Data/BitVec/OfFn.lean

@@ -172,7 +172,6 @@ theorem toListBE_inj {x y : BitVec w} : x.toListBE = y.toListBE ↔ x = y :=
 theorem toListBE_nil : toListBE nil = [] := by
   simp [toListBE]
 
-
 @[simp]
 theorem toListBE_cons (b : Bool) (x : BitVec w) :
     toListBE (cons b x) = b :: toListBE x := by
@@ -187,7 +186,7 @@ theorem toListBE_cons (b : Bool) (x : BitVec w) :
       rw [dif_neg]
       simp only [Nat.reduceSubDiff, List.getElem_cons_succ, getElem_toListBE]
       omega
-  · repeat rw [List.getElem?_eq_none (by simp; omega)]
+  · repeat rw [List.getElem?_eq_none (by simp only [List.length_cons, length_toListBE]; omega)]
 
 @[simp]
 theorem toListBE_concat (b : Bool) (x : BitVec w) :