diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 81abd4231d67..68fb4bab15f7 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -1353,9 +1353,8 @@ theorem toNat_udiv {x y : BitVec n} : (x / y).toNat = x.toNat / y.toNat := by
     exact Nat.lt_of_le_of_lt (Nat.div_le_self ..) (by omega)
 
 @[simp]
-theorem udiv_zero {x : BitVec n} : x.udiv 0#n = 0#n := by
-  simp only [udiv, toNat_ofNat, Nat.zero_mod, Nat.div_zero]
-  rfl
+theorem udiv_zero {x : BitVec n} : x / 0#n = 0#n := by
+  simp [udiv_def]
 
 /-! ### umod -/
 
@@ -1370,8 +1369,8 @@ theorem toNat_umod {x y : BitVec n} :
     (x % y).toNat = x.toNat % y.toNat := rfl
 
 @[simp]
-theorem umod_zero {x : BitVec n} : x.umod 0#n = x := by
-  simp [umod_eq]
+theorem umod_zero {x : BitVec n} : x % 0#n = x := by
+  simp [umod_def]
 
 /-! ### sdiv -/
 
@@ -2205,7 +2204,7 @@ protected theorem ne_of_lt {x y : BitVec n} : x < y → x ≠ y := by
   simp only [lt_def, ne_eq, toNat_eq]
   apply Nat.ne_of_lt
 
-protected theorem umod_lt (x : BitVec n) {y : BitVec n} : 0 < y → x.umod y < y := by
+protected theorem umod_lt (x : BitVec n) {y : BitVec n} : 0 < y → x % y < y := by
   simp only [ofNat_eq_ofNat, lt_def, toNat_ofNat, Nat.zero_mod, umod, toNat_ofNatLt]
   apply Nat.mod_lt