From fee34f865f9090f5b224caadeebf5a75d21e28b3 Mon Sep 17 00:00:00 2001
From: Tobias Grosser <tobias@grosser.es>
Date: Wed, 18 Sep 2024 23:39:05 +0100
Subject: [PATCH] WIP

---
 src/Init/Data/BitVec/Lemmas.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 5a58f0623595..748417f666c8 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -1443,6 +1443,7 @@ theorem toNat_cons' {x : BitVec w} :
 
 @[simp] theorem getElem_cons (b : Bool) {n} (x : BitVec n) (i : Nat) (h : i < 1 + n):
     (cons b x)[i] = if i = n then b else getLsbD x i := by
+
   stop
   simp only [getLsbD, toNat_cons, Nat.testBit_or]
   rw [Nat.testBit_shiftLeft]