chore: fix non-term simp

leanprover · Jan 16, 2025 · 6092449 · 6092449
1 parent 6537834
commit 6092449
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
@@ -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