Update src/Init/Data/BitVec/Lemmas.lean

Co-authored-by: Henrik Böving <hargonix@gmail.com>
opencompl · Aug 11, 2024 · 7351639 · 7351639
1 parent 2d46ca2
commit 7351639
Showing 1 changed file with 4 additions and 3 deletions.
diff --git 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 -/