From 751f74f13aa45c23b76337c0bab83bb441e6c731 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Tue, 21 Jan 2025 16:29:51 +0000 Subject: [PATCH] chore: cases instead of by_cases --- src/Init/Data/BitVec/Lemmas.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index c9ac8f84acc7..f7ecf22f42eb 100644 --- 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] - by_cases h' : w = 0 <;> simp [h'] <;> omega + cases w <;> simp <;> omega @[simp] theorem replicate_one {w : Nat} {x : BitVec w} (h : w = w * 1 := by rw [Nat.mul_one]) :