From 7351639d858d7c943667ac91be060dda23177f31 Mon Sep 17 00:00:00 2001
From: Tobias Grosser <github@grosser.es>
Date: Sun, 11 Aug 2024 10:49:05 +0100
Subject: [PATCH] Update src/Init/Data/BitVec/Lemmas.lean
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Co-authored-by: Henrik Böving <hargonix@gmail.com>
---
 src/Init/Data/BitVec/Lemmas.lean | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index e4c2f2ed04ce..3ccdfc14013b 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -1265,9 +1265,10 @@ theorem neg_neg {x : BitVec w} : - - x = x := by
 
 theorem neg_ne_iff_ne_neg {x y : BitVec w} : -x ≠ y ↔ x ≠ -y := by
   constructor
-    <;> intro h h'
-    <;> subst h'
-    <;> simp [BitVec.neg_neg] at h
+  all_goals
+    intro h h'
+    subst h'
+    simp at h
 
 /-! ### mul -/