From 6092449223415d757e2846cc5a1118ad6b182c22 Mon Sep 17 00:00:00 2001
From: luisacicolini <lc985@cam.ac.uk>
Date: Thu, 16 Jan 2025 18:24:03 +0000
Subject: [PATCH] chore: fix non-term simp

---
 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 b34ebd1581c4..c3c023d2ac6d 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -3459,7 +3459,7 @@ theorem replicate_append_self {x : BitVec w} :
   | succ n ih =>
     rw [replicate_succ]
     conv => lhs; rw [ih]
-    simp [cast_cast, cast_eq]
+    simp only [cast_cast, cast_eq]
     rw [← cast_append_left]
     · rw [append_assoc]; congr
     · rw [Nat.add_comm, Nat.mul_add, Nat.mul_one]; omega