chore: simpler getElem proof

leanprover · Jan 21, 2025 · f8f584f · f8f584f
1 parent 751f74f
commit f8f584f
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
@@ -3793,7 +3793,7 @@ theorem getLsbD_replicate {n w : Nat} {x : BitVec w} :
 theorem getElem_replicate {n w : Nat} {x : BitVec w} (h : i < w * n) :
     (x.replicate n)[i] = if h' : w = 0 then false else x[i % w]'(@Nat.mod_lt i w (by omega)) := by
   simp only [← getLsbD_eq_getElem, getLsbD_replicate]
-  cases w <;> simp <;> omega
+  cases w <;> simp; omega
 
 @[simp]
 theorem replicate_one {w : Nat} {x : BitVec w} (h : w = w * 1 := by rw [Nat.mul_one]) :