From 2233ac40a9f7c4bd2cdd0b79182c29abb7c984d0 Mon Sep 17 00:00:00 2001
From: Alex Keizer <alex@keizer.dev>
Date: Sat, 19 Oct 2024 13:15:34 -0500
Subject: [PATCH] simplify proof of `toInt_neg` using toInt_sub

---
 src/Init/Data/BitVec/Lemmas.lean | 16 ++++------------
 1 file changed, 4 insertions(+), 12 deletions(-)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 76420978a8cf..6cef554b1ad9 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -2006,6 +2006,8 @@ theorem ofNat_sub_ofNat {n} (x y : Nat) : BitVec.ofNat n x - BitVec.ofNat n y =
 
 @[simp] protected theorem sub_zero (x : BitVec n) : x - 0#n = x := by apply eq_of_toNat_eq ; simp
 
+@[simp] protected theorem zero_sub (x : BitVec n) : 0#n - x = -x := rfl
+
 @[simp] protected theorem sub_self (x : BitVec n) : x - x = 0#n := by
   apply eq_of_toNat_eq
   simp only [toNat_sub]
@@ -2018,18 +2020,8 @@ theorem ofNat_sub_ofNat {n} (x y : Nat) : BitVec.ofNat n x - BitVec.ofNat n y =
 
 theorem toInt_neg {x : BitVec w} :
     (-x).toInt = (-x.toInt).bmod (2 ^ w) := by
-  simp only [toInt_eq_toNat_bmod, toNat_neg, Int.ofNat_emod, Int.emod_bmod_congr]
-  rw [← Int.subNatNat_of_le (by omega), Int.subNatNat_eq_coe, Int.sub_eq_add_neg, Int.add_comm,
-    Int.bmod_add_cancel]
-  by_cases h : x.toNat < ((2 ^ w) + 1) / 2
-  · rw [Int.bmod_pos (x := x.toNat)]
-    all_goals simp only [toNat_mod_cancel']
-    norm_cast
-  · rw [Int.bmod_neg (x := x.toNat)]
-    · simp only [toNat_mod_cancel']
-      rw_mod_cast [Int.neg_sub, Int.sub_eq_add_neg, Int.add_comm, Int.bmod_add_cancel]
-    · norm_cast
-      simp_all
+  rw [← BitVec.zero_sub, toInt_sub]
+  simp [BitVec.toInt_ofNat]
 
 @[simp] theorem toFin_neg (x : BitVec n) :
     (-x).toFin = Fin.ofNat' (2^n) (2^n - x.toNat) :=