chore: fixup proof after incorporating tobi suggestion

opencompl · Nov 8, 2024 · 191f36c · 191f36c
1 parent 0028f5f
commit 191f36c
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
@@ -2980,7 +2980,7 @@ theorem toInt_abs (x : BitVec w) :
     x.abs.toInt = if x = (intMin w) then (intMin w).toInt else x.toInt.abs := by
   rcases w with rfl | w 
   · simp [toInt_zero_length]
-  · simp only [gt_iff_lt, Nat.zero_lt_succ, Nat.add_one_ne_zero, ↓reduceIte]
+  · simp only [toInt_intMin_eq_ite, gt_iff_lt, Nat.zero_lt_succ, Nat.add_one_ne_zero, ↓reduceIte]
     rw [BitVec.abs_eq_ite]
     by_cases hx : x = intMin (w + 1)
     · simp only [hx, reduceIte]