diff --git a/src/Init/Data/BitVec/Basic.lean b/src/Init/Data/BitVec/Basic.lean
index 6cb0e28f8a..91e1ae9d34 100644
--- a/src/Init/Data/BitVec/Basic.lean
+++ b/src/Init/Data/BitVec/Basic.lean
@@ -116,17 +116,62 @@ end zero_allOnes
 
 section getXsb
 
+/--
+Return the `i`-th least significant bit.
+
+This will be renamed `getLsb` after the existing deprecated alias is removed.
+-/
+@[inline] def getLsb' (x : BitVec w) (i : Fin w) : Bool := x.toNat.testBit i
+
+/-- Return the `i`-th least significant bit or `none` if `i ≥ w`. -/
+@[inline] def getLsb? (x : BitVec w) (i : Nat) : Option Bool :=
+  if h : i < w then some (getLsb' x ⟨i, h⟩) else none
+
+/--
+Return the `i`-th most significant bit.
+
+This will be renamed `getMsb` after the existing deprecated alias is removed.
+-/
+@[inline] def getMsb' (x : BitVec w) (i : Fin w) : Bool := x.getLsb' ⟨w-1-i, by omega⟩
+
+/-- Return the `i`-th most significant bit or `none` if `i ≥ w`. -/
+@[inline] def getMsb? (x : BitVec w) (i : Nat) : Option Bool :=
+  if h : i < w then some (getMsb' x ⟨i, h⟩) else none
+
 /-- Return the `i`-th least significant bit or `false` if `i ≥ w`. -/
-@[inline] def getLsb (x : BitVec w) (i : Nat) : Bool := x.toNat.testBit i
+@[inline] def getLsbD (x : BitVec w) (i : Nat) : Bool :=
+  x.toNat.testBit i
+
+@[deprecated getLsbD (since := "2024-08-29"), inherit_doc getLsbD]
+def getLsb (x : BitVec w) (i : Nat) : Bool := x.getLsbD i
 
 /-- Return the `i`-th most significant bit or `false` if `i ≥ w`. -/
-@[inline] def getMsb (x : BitVec w) (i : Nat) : Bool := i < w && getLsb x (w-1-i)
+@[inline] def getMsbD (x : BitVec w) (i : Nat) : Bool :=
+  i < w && x.getLsbD (w-1-i)
+
+@[deprecated getMsbD (since := "2024-08-29"), inherit_doc getMsbD]
+def getMsb (x : BitVec w) (i : Nat) : Bool := x.getMsbD i
 
 /-- Return most-significant bit in bitvector. -/
-@[inline] protected def msb (x : BitVec n) : Bool := getMsb x 0
+@[inline] protected def msb (x : BitVec n) : Bool := getMsbD x 0
 
 end getXsb
 
+section getElem
+
+instance : GetElem (BitVec w) Nat Bool fun _ i => i < w where
+  getElem xs i h := xs.getLsb' ⟨i, h⟩
+
+/-- We prefer `x[i]` as the simp normal form for `getLsb'` -/
+@[simp] theorem getLsb'_eq_getElem (x : BitVec w) (i : Fin w) :
+    x.getLsb' i = x[i] := rfl
+
+/-- We prefer `x[i]?` as the simp normal form for `getLsb?` -/
+@[simp] theorem getLsb?_eq_getElem? (x : BitVec w) (i : Nat) :
+    x.getLsb? i = x[i]? := rfl
+
+end getElem
+
 section Int
 
 /-- Interpret the bitvector as an integer stored in two's complement form. -/
diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean
index 18b0b8c85c..35f8d4d407 100644
--- a/src/Init/Data/BitVec/Bitblast.lean
+++ b/src/Init/Data/BitVec/Bitblast.lean
@@ -92,8 +92,8 @@ def carry (i : Nat) (x y : BitVec w) (c : Bool) : Bool :=
   cases c <;> simp [carry, mod_one]
 
 theorem carry_succ (i : Nat) (x y : BitVec w) (c : Bool) :
-    carry (i+1) x y c = atLeastTwo (x.getLsb i) (y.getLsb i) (carry i x y c) := by
-  simp only [carry, mod_two_pow_succ, atLeastTwo, getLsb]
+    carry (i+1) x y c = atLeastTwo (x.getLsbD i) (y.getLsbD i) (carry i x y c) := by
+  simp only [carry, mod_two_pow_succ, atLeastTwo, getLsbD]
   simp only [Nat.pow_succ']
   have sum_bnd : x.toNat%2^i + (y.toNat%2^i + c.toNat) < 2*2^i := by
     simp only [← Nat.pow_succ']
@@ -110,7 +110,7 @@ theorem carry_of_and_eq_zero {x y : BitVec w} (h : x &&& y = 0#w) : carry i x y
   induction i with
   | zero => simp
   | succ i ih =>
-    replace h := congrArg (·.getLsb i) h
+    replace h := congrArg (·.getLsbD i) h
     simp_all [carry_succ]
 
 /-- The final carry bit when computing `x + y + c` is `true` iff `x.toNat + y.toNat + c.toNat ≥ 2^w`. -/
@@ -136,14 +136,14 @@ def adcb (x y c : Bool) : Bool × Bool := (atLeastTwo x y c, Bool.xor x (Bool.xo
 
 /-- Bitwise addition implemented via a ripple carry adder. -/
 def adc (x y : BitVec w) : Bool → Bool × BitVec w :=
-  iunfoldr fun (i : Fin w) c => adcb (x.getLsb i) (y.getLsb i) c
+  iunfoldr fun (i : Fin w) c => adcb (x.getLsbD i) (y.getLsbD i) c
 
-theorem getLsb_add_add_bool {i : Nat} (i_lt : i < w) (x y : BitVec w) (c : Bool) :
-    getLsb (x + y + zeroExtend w (ofBool c)) i =
-      Bool.xor (getLsb x i) (Bool.xor (getLsb y i) (carry i x y c)) := by
+theorem getLsbD_add_add_bool {i : Nat} (i_lt : i < w) (x y : BitVec w) (c : Bool) :
+    getLsbD (x + y + zeroExtend w (ofBool c)) i =
+      Bool.xor (getLsbD x i) (Bool.xor (getLsbD y i) (carry i x y c)) := by
   let ⟨x, x_lt⟩ := x
   let ⟨y, y_lt⟩ := y
-  simp only [getLsb, toNat_add, toNat_zeroExtend, i_lt, toNat_ofFin, toNat_ofBool,
+  simp only [getLsbD, toNat_add, toNat_zeroExtend, i_lt, toNat_ofFin, toNat_ofBool,
     Nat.mod_add_mod, Nat.add_mod_mod]
   apply Eq.trans
   rw [← Nat.div_add_mod x (2^i), ← Nat.div_add_mod y (2^i)]
@@ -159,10 +159,10 @@ theorem getLsb_add_add_bool {i : Nat} (i_lt : i < w) (x y : BitVec w) (c : Bool)
     ]
   simp [testBit_to_div_mod, carry, Nat.add_assoc]
 
-theorem getLsb_add {i : Nat} (i_lt : i < w) (x y : BitVec w) :
-    getLsb (x + y) i =
-      Bool.xor (getLsb x i) (Bool.xor (getLsb y i) (carry i x y false)) := by
-  simpa using getLsb_add_add_bool i_lt x y false
+theorem getLsbD_add {i : Nat} (i_lt : i < w) (x y : BitVec w) :
+    getLsbD (x + y) i =
+      Bool.xor (getLsbD x i) (Bool.xor (getLsbD y i) (carry i x y false)) := by
+  simpa using getLsbD_add_add_bool i_lt x y false
 
 theorem adc_spec (x y : BitVec w) (c : Bool) :
     adc x y c = (carry w x y c, x + y + zeroExtend w (ofBool c)) := by
@@ -175,7 +175,7 @@ theorem adc_spec (x y : BitVec w) (c : Bool) :
     simp [carry, Nat.mod_one]
     cases c <;> rfl
   case step =>
-    simp [adcb, Prod.mk.injEq, carry_succ, getLsb_add_add_bool]
+    simp [adcb, Prod.mk.injEq, carry_succ, getLsbD_add_add_bool]
 
 theorem add_eq_adc (w : Nat) (x y : BitVec w) : x + y = (adc x y false).snd := by
   simp [adc_spec]
@@ -197,37 +197,37 @@ theorem add_eq_or_of_and_eq_zero {w : Nat} (x y : BitVec w)
     (h : x &&& y = 0#w) : x + y = x ||| y := by
   rw [add_eq_adc, adc, iunfoldr_replace (fun _ => false) (x ||| y)]
   · rfl
-  · simp only [adcb, atLeastTwo, Bool.and_false, Bool.or_false, bne_false, getLsb_or,
+  · simp only [adcb, atLeastTwo, Bool.and_false, Bool.or_false, bne_false, getLsbD_or,
     Prod.mk.injEq, and_eq_false_imp]
     intros i
-    replace h : (x &&& y).getLsb i = (0#w).getLsb i := by rw [h]
-    simp only [getLsb_and, getLsb_zero, and_eq_false_imp] at h
+    replace h : (x &&& y).getLsbD i = (0#w).getLsbD i := by rw [h]
+    simp only [getLsbD_and, getLsbD_zero, and_eq_false_imp] at h
     constructor
     · intros hx
       simp_all [hx]
-    · by_cases hx : x.getLsb i <;> simp_all [hx]
+    · by_cases hx : x.getLsbD i <;> simp_all [hx]
 
 /-! ### Negation -/
 
 theorem bit_not_testBit (x : BitVec w) (i : Fin w) :
-  getLsb (((iunfoldr (fun (i : Fin w) c => (c, !(x.getLsb i)))) ()).snd) i.val = !(getLsb x i.val) := by
-  apply iunfoldr_getLsb (fun _ => ()) i (by simp)
+  getLsbD (((iunfoldr (fun (i : Fin w) c => (c, !(x.getLsbD i)))) ()).snd) i.val = !(getLsbD x i.val) := by
+  apply iunfoldr_getLsbD (fun _ => ()) i (by simp)
 
 theorem bit_not_add_self (x : BitVec w) :
-  ((iunfoldr (fun (i : Fin w) c => (c, !(x.getLsb i)))) ()).snd + x  = -1 := by
+  ((iunfoldr (fun (i : Fin w) c => (c, !(x.getLsbD i)))) ()).snd + x  = -1 := by
   simp only [add_eq_adc]
   apply iunfoldr_replace_snd (fun _ => false) (-1) false rfl
   intro i; simp only [ BitVec.not, adcb, testBit_toNat]
-  rw [iunfoldr_replace_snd (fun _ => ()) (((iunfoldr (fun i c => (c, !(x.getLsb i)))) ()).snd)]
-  <;> simp [bit_not_testBit, negOne_eq_allOnes, getLsb_allOnes]
+  rw [iunfoldr_replace_snd (fun _ => ()) (((iunfoldr (fun i c => (c, !(x.getLsbD i)))) ()).snd)]
+  <;> simp [bit_not_testBit, negOne_eq_allOnes, getLsbD_allOnes]
 
 theorem bit_not_eq_not (x : BitVec w) :
-  ((iunfoldr (fun i c => (c, !(x.getLsb i)))) ()).snd = ~~~ x := by
+  ((iunfoldr (fun i c => (c, !(x.getLsbD i)))) ()).snd = ~~~ x := by
   simp [←allOnes_sub_eq_not, BitVec.eq_sub_iff_add_eq.mpr (bit_not_add_self x), ←negOne_eq_allOnes]
 
-theorem bit_neg_eq_neg (x : BitVec w) : -x = (adc (((iunfoldr (fun (i : Fin w) c => (c, !(x.getLsb i)))) ()).snd) (BitVec.ofNat w 1) false).snd:= by
+theorem bit_neg_eq_neg (x : BitVec w) : -x = (adc (((iunfoldr (fun (i : Fin w) c => (c, !(x.getLsbD i)))) ()).snd) (BitVec.ofNat w 1) false).snd:= by
   simp only [← add_eq_adc]
-  rw [iunfoldr_replace_snd ((fun _ => ())) (((iunfoldr (fun (i : Fin w) c => (c, !(x.getLsb i)))) ()).snd) _ rfl]
+  rw [iunfoldr_replace_snd ((fun _ => ())) (((iunfoldr (fun (i : Fin w) c => (c, !(x.getLsbD i)))) ()).snd) _ rfl]
   · rw [BitVec.eq_sub_iff_add_eq.mpr (bit_not_add_self x), sub_toAdd, BitVec.add_comm _ (-x)]
     simp [← sub_toAdd, BitVec.sub_add_cancel]
   · simp [bit_not_testBit x _]
@@ -290,17 +290,17 @@ A recurrence that describes multiplication as repeated addition.
 Is useful for bitblasting multiplication.
 -/
 def mulRec (x y : BitVec w) (s : Nat) : BitVec w :=
-  let cur := if y.getLsb s then (x <<< s) else 0
+  let cur := if y.getLsbD s then (x <<< s) else 0
   match s with
   | 0 => cur
   | s + 1 => mulRec x y s + cur
 
 theorem mulRec_zero_eq (x y : BitVec w) :
-    mulRec x y 0 = if y.getLsb 0 then x else 0 := by
+    mulRec x y 0 = if y.getLsbD 0 then x else 0 := by
   simp [mulRec]
 
 theorem mulRec_succ_eq (x y : BitVec w) (s : Nat) :
-    mulRec x y (s + 1) = mulRec x y s + if y.getLsb (s + 1) then (x <<< (s + 1)) else 0 := rfl
+    mulRec x y (s + 1) = mulRec x y s + if y.getLsbD (s + 1) then (x <<< (s + 1)) else 0 := rfl
 
 /--
 Recurrence lemma: truncating to `i+1` bits and then zero extending to `w`
@@ -311,11 +311,11 @@ theorem zeroExtend_truncate_succ_eq_zeroExtend_truncate_add_twoPow (x : BitVec w
       zeroExtend w (x.truncate i) + (x &&& twoPow w i) := by
   rw [add_eq_or_of_and_eq_zero]
   · ext k
-    simp only [getLsb_zeroExtend, Fin.is_lt, decide_True, Bool.true_and, getLsb_or, getLsb_and]
+    simp only [getLsbD_zeroExtend, Fin.is_lt, decide_True, Bool.true_and, getLsbD_or, getLsbD_and]
     by_cases hik : i = k
     · subst hik
       simp
-    · simp only [getLsb_twoPow, hik, decide_False, Bool.and_false, Bool.or_false]
+    · simp only [getLsbD_twoPow, hik, decide_False, Bool.and_false, Bool.or_false]
       by_cases hik' : k < (i + 1)
       · have hik'' : k < i := by omega
         simp [hik', hik'']
@@ -323,7 +323,7 @@ theorem zeroExtend_truncate_succ_eq_zeroExtend_truncate_add_twoPow (x : BitVec w
         simp [hik', hik'']
   · ext k
     simp
-    by_cases hi : x.getLsb i <;> simp [hi] <;> omega
+    by_cases hi : x.getLsbD i <;> simp [hi] <;> omega
 
 /--
 Recurrence lemma: multiplying `x` with the first `s` bits of `y` is the
@@ -334,7 +334,7 @@ theorem mulRec_eq_mul_signExtend_truncate (x y : BitVec w) (s : Nat) :
   induction s
   case zero =>
     simp only [mulRec_zero_eq, ofNat_eq_ofNat, Nat.reduceAdd]
-    by_cases y.getLsb 0
+    by_cases y.getLsbD 0
     case pos hy =>
       simp only [hy, ↓reduceIte, truncate, zeroExtend_one_eq_ofBool_getLsb_zero,
         ofBool_true, ofNat_eq_ofNat]
@@ -345,14 +345,14 @@ theorem mulRec_eq_mul_signExtend_truncate (x y : BitVec w) (s : Nat) :
   case succ s' hs =>
     rw [mulRec_succ_eq, hs]
     have heq :
-      (if y.getLsb (s' + 1) = true then x <<< (s' + 1) else 0) =
+      (if y.getLsbD (s' + 1) = true then x <<< (s' + 1) else 0) =
         (x * (y &&& (BitVec.twoPow w (s' + 1)))) := by
       simp only [ofNat_eq_ofNat, and_twoPow]
-      by_cases hy : y.getLsb (s' + 1) <;> simp [hy]
+      by_cases hy : y.getLsbD (s' + 1) <;> simp [hy]
     rw [heq, ← BitVec.mul_add, ← zeroExtend_truncate_succ_eq_zeroExtend_truncate_add_twoPow]
 
-theorem getLsb_mul (x y : BitVec w) (i : Nat) :
-    (x * y).getLsb i = (mulRec x y w).getLsb i := by
+theorem getLsbD_mul (x y : BitVec w) (i : Nat) :
+    (x * y).getLsbD i = (mulRec x y w).getLsbD i := by
   simp only [mulRec_eq_mul_signExtend_truncate]
   rw [truncate, ← truncate_eq_zeroExtend, ← truncate_eq_zeroExtend,
     truncate_truncate_of_le]
@@ -406,17 +406,17 @@ theorem shiftLeftRec_eq {x : BitVec w₁} {y : BitVec w₂} {n : Nat} :
   case zero =>
     ext i
     simp only [shiftLeftRec_zero, twoPow_zero, Nat.reduceAdd, truncate_one,
-      and_one_eq_zeroExtend_ofBool_getLsb]
+      and_one_eq_zeroExtend_ofBool_getLsbD]
   case succ n ih =>
     simp only [shiftLeftRec_succ, and_twoPow]
     rw [ih]
-    by_cases h : y.getLsb (n + 1)
+    by_cases h : y.getLsbD (n + 1)
     · simp only [h, ↓reduceIte]
-      rw [zeroExtend_truncate_succ_eq_zeroExtend_truncate_or_twoPow_of_getLsb_true h,
+      rw [zeroExtend_truncate_succ_eq_zeroExtend_truncate_or_twoPow_of_getLsbD_true h,
         shiftLeft_or_of_and_eq_zero]
       simp
     · simp only [h, false_eq_true, ↓reduceIte, shiftLeft_zero']
-      rw [zeroExtend_truncate_succ_eq_zeroExtend_truncate_of_getLsb_false (i := n + 1)]
+      rw [zeroExtend_truncate_succ_eq_zeroExtend_truncate_of_getLsbD_false (i := n + 1)]
       simp [h]
 
 /--
@@ -469,14 +469,14 @@ theorem sshiftRightRec_eq (x : BitVec w₁) (y : BitVec w₂) (n : Nat) :
   induction n generalizing x y
   case zero =>
     ext i
-    simp [twoPow_zero, Nat.reduceAdd, and_one_eq_zeroExtend_ofBool_getLsb, truncate_one]
+    simp [twoPow_zero, Nat.reduceAdd, and_one_eq_zeroExtend_ofBool_getLsbD, truncate_one]
   case succ n ih =>
     simp only [sshiftRightRec_succ_eq, and_twoPow, ih]
-    by_cases h : y.getLsb (n + 1)
-    · rw [zeroExtend_truncate_succ_eq_zeroExtend_truncate_or_twoPow_of_getLsb_true h,
+    by_cases h : y.getLsbD (n + 1)
+    · rw [zeroExtend_truncate_succ_eq_zeroExtend_truncate_or_twoPow_of_getLsbD_true h,
         sshiftRight'_or_of_and_eq_zero (by simp), h]
       simp
-    · rw [zeroExtend_truncate_succ_eq_zeroExtend_truncate_of_getLsb_false (i := n + 1)
+    · rw [zeroExtend_truncate_succ_eq_zeroExtend_truncate_of_getLsbD_false (i := n + 1)
         (by simp [h])]
       simp [h]
 
@@ -485,7 +485,7 @@ Show that `x.sshiftRight y` can be written in terms of `sshiftRightRec`.
 This can be unfolded in terms of `sshiftRightRec_zero_eq`, `sshiftRightRec_succ_eq` for bitblasting.
 -/
 theorem sshiftRight_eq_sshiftRightRec (x : BitVec w₁) (y : BitVec w₂) :
-    (x.sshiftRight' y).getLsb i = (sshiftRightRec x y (w₂ - 1)).getLsb i := by
+    (x.sshiftRight' y).getLsbD i = (sshiftRightRec x y (w₂ - 1)).getLsbD i := by
   rcases w₂ with rfl | w₂
   · simp [of_length_zero]
   · simp [sshiftRightRec_eq]
@@ -533,15 +533,15 @@ theorem ushiftRightRec_eq (x : BitVec w₁) (y : BitVec w₂) (n : Nat) :
   case zero =>
     ext i
     simp only [ushiftRightRec_zero, twoPow_zero, Nat.reduceAdd,
-      and_one_eq_zeroExtend_ofBool_getLsb, truncate_one]
+      and_one_eq_zeroExtend_ofBool_getLsbD, truncate_one]
   case succ n ih =>
     simp only [ushiftRightRec_succ, and_twoPow]
     rw [ih]
-    by_cases h : y.getLsb (n + 1) <;> simp only [h, ↓reduceIte]
-    · rw [zeroExtend_truncate_succ_eq_zeroExtend_truncate_or_twoPow_of_getLsb_true h,
+    by_cases h : y.getLsbD (n + 1) <;> simp only [h, ↓reduceIte]
+    · rw [zeroExtend_truncate_succ_eq_zeroExtend_truncate_or_twoPow_of_getLsbD_true h,
         ushiftRight'_or_of_and_eq_zero]
       simp
-    · simp [zeroExtend_truncate_succ_eq_zeroExtend_truncate_of_getLsb_false, h]
+    · simp [zeroExtend_truncate_succ_eq_zeroExtend_truncate_of_getLsbD_false, h]
 
 /--
 Show that `x >>> y` can be written in terms of `ushiftRightRec`.
diff --git a/src/Init/Data/BitVec/Folds.lean b/src/Init/Data/BitVec/Folds.lean
index 3dddf614e0..4b2cb84f2d 100644
--- a/src/Init/Data/BitVec/Folds.lean
+++ b/src/Init/Data/BitVec/Folds.lean
@@ -41,7 +41,7 @@ theorem iunfoldr.fst_eq
 private theorem iunfoldr.eq_test
     {f : Fin w → α → α × Bool} (state : Nat → α) (value : BitVec w) (a : α)
     (init : state 0 = a)
-    (step : ∀(i : Fin w), f i (state i.val) = (state (i.val+1), value.getLsb i.val)) :
+    (step : ∀(i : Fin w), f i (state i.val) = (state (i.val+1), value.getLsbD i.val)) :
     iunfoldr f a = (state w, BitVec.truncate w value) := by
   apply Fin.hIterate_eq (fun i => ((state i, BitVec.truncate i value) : α × BitVec i))
   case init =>
@@ -50,15 +50,15 @@ private theorem iunfoldr.eq_test
     intro i
     simp_all [truncate_succ]
 
-theorem iunfoldr_getLsb' {f : Fin w → α → α × Bool} (state : Nat → α)
+theorem iunfoldr_getLsbD' {f : Fin w → α → α × Bool} (state : Nat → α)
     (ind : ∀(i : Fin w), (f i (state i.val)).fst = state (i.val+1)) :
-  (∀ i : Fin w, getLsb (iunfoldr f (state 0)).snd i.val = (f i (state i.val)).snd)
+  (∀ i : Fin w, getLsbD (iunfoldr f (state 0)).snd i.val = (f i (state i.val)).snd)
   ∧ (iunfoldr f (state 0)).fst = state w := by
   unfold iunfoldr
   simp
   apply Fin.hIterate_elim
         (fun j (p : α × BitVec j) => (hj : j ≤ w) →
-         (∀ i : Fin j,  getLsb p.snd i.val = (f ⟨i.val, Nat.lt_of_lt_of_le i.isLt hj⟩ (state i.val)).snd)
+         (∀ i : Fin j,  getLsbD p.snd i.val = (f ⟨i.val, Nat.lt_of_lt_of_le i.isLt hj⟩ (state i.val)).snd)
           ∧ p.fst = state j)
   case hj => simp
   case init =>
@@ -73,7 +73,7 @@ theorem iunfoldr_getLsb' {f : Fin w → α → α × Bool} (state : Nat → α)
     apply And.intro
     case left =>
       intro i
-      simp only [getLsb_cons]
+      simp only [getLsbD_cons]
       have hj2 : j.val ≤ w := by simp
       cases (Nat.lt_or_eq_of_le (Nat.lt_succ.mp i.isLt)) with
       | inl h3 => simp [if_neg, (Nat.ne_of_lt h3)]
@@ -90,10 +90,10 @@ theorem iunfoldr_getLsb' {f : Fin w → α → α × Bool} (state : Nat → α)
       rw [← ind j, ← (ih hj2).2]
 
 
-theorem iunfoldr_getLsb {f : Fin w → α → α × Bool} (state : Nat → α) (i : Fin w)
+theorem iunfoldr_getLsbD {f : Fin w → α → α × Bool} (state : Nat → α) (i : Fin w)
     (ind : ∀(i : Fin w), (f i (state i.val)).fst = state (i.val+1)) :
-  getLsb (iunfoldr f (state 0)).snd i.val = (f i (state i.val)).snd := by
-  exact (iunfoldr_getLsb' state ind).1 i
+  getLsbD (iunfoldr f (state 0)).snd i.val = (f i (state i.val)).snd := by
+  exact (iunfoldr_getLsbD' state ind).1 i
 
 /--
 Correctness theorem for `iunfoldr`.
@@ -101,14 +101,14 @@ Correctness theorem for `iunfoldr`.
 theorem iunfoldr_replace
     {f : Fin w → α → α × Bool} (state : Nat → α) (value : BitVec w) (a : α)
     (init : state 0 = a)
-    (step : ∀(i : Fin w), f i (state i.val) = (state (i.val+1), value.getLsb i.val)) :
+    (step : ∀(i : Fin w), f i (state i.val) = (state (i.val+1), value.getLsbD i.val)) :
     iunfoldr f a = (state w, value) := by
   simp [iunfoldr.eq_test state value a init step]
 
 theorem iunfoldr_replace_snd
   {f : Fin w → α → α × Bool} (state : Nat → α) (value : BitVec w) (a : α)
     (init : state 0 = a)
-    (step : ∀(i : Fin w), f i (state i.val) = (state (i.val+1), value.getLsb i.val)) :
+    (step : ∀(i : Fin w), f i (state i.val) = (state (i.val+1), value.getLsbD i.val)) :
     (iunfoldr f a).snd = value := by
   simp [iunfoldr.eq_test state value a init step]
 
diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index b43d1e4360..234df0166a 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -16,6 +16,77 @@ set_option linter.missingDocs true
 
 namespace BitVec
 
+@[simp] theorem getLsbD_ofFin (x : Fin (2^n)) (i : Nat) :
+    getLsbD (BitVec.ofFin x) i = x.val.testBit i := rfl
+
+@[simp] theorem getLsbD_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : getLsbD x i = false := by
+  let ⟨x, x_lt⟩ := x
+  simp only [getLsbD_ofFin]
+  apply Nat.testBit_lt_two_pow
+  have p : 2^w ≤ 2^i := Nat.pow_le_pow_of_le_right (by omega) ge
+  omega
+
+@[simp] theorem getMsbD_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : getMsbD x i = false := by
+  rw [getMsbD]
+  simp only [Bool.and_eq_false_imp, decide_eq_true_eq]
+  omega
+
+theorem lt_of_getLsbD (x : BitVec w) (i : Nat) : getLsbD x i = true → i < w := by
+  if h : i < w then
+    simp [h]
+  else
+    simp [Nat.ge_of_not_lt h]
+
+theorem lt_of_getMsbD (x : BitVec w) (i : Nat) : getMsbD x i = true → i < w := by
+  if h : i < w then
+    simp [h]
+  else
+    simp [Nat.ge_of_not_lt h]
+
+@[simp] theorem getElem?_eq_getElem {l : BitVec w} {n} (h : n < w) : l[n]? = some l[n] := by
+  simp only [getElem?_def, h, ↓reduceDIte]
+
+theorem getElem?_eq_some {l : BitVec w} : l[n]? = some a ↔ ∃ h : n < w, l[n] = a := by
+  simp only [getElem?_def]
+  split
+  · simp_all
+  · simp; omega
+
+@[simp] theorem getElem?_eq_none_iff {l : BitVec w} : l[n]? = none ↔ w ≤ n := by
+  simp only [getElem?_def]
+  split
+  · simp_all
+  · simp; omega
+
+theorem getElem?_eq_none {l : BitVec w} (h : w ≤ n) : l[n]? = none := getElem?_eq_none_iff.mpr h
+
+theorem getElem?_eq (l : BitVec w) (i : Nat) :
+    l[i]? = if h : i < w then some l[i] else none := by
+  split <;> simp_all
+
+@[simp] theorem some_getElem_eq_getElem? (l : BitVec w) (i : Nat) (h : i < w) :
+    (some l[i] = l[i]?) ↔ True := by
+  simp [h]
+
+@[simp] theorem getElem?_eq_some_getElem (l : BitVec w) (i : Nat) (h : i < w) :
+    (l[i]? = some l[i]) ↔ True := by
+  simp [h]
+
+theorem getElem_eq_iff {l : BitVec w} {n : Nat} {h : n < w} : l[n] = x ↔ l[n]? = some x := by
+  simp only [getElem?_eq_some]
+  exact ⟨fun w => ⟨h, w⟩, fun h => h.2⟩
+
+theorem getElem_eq_getElem? (l : BitVec w) (i : Nat) (h : i < w) :
+    l[i] = l[i]?.get (by simp [getElem?_eq_getElem, h]) := by
+  simp [getElem_eq_iff]
+
+theorem getLsbD_eq_getElem?_getD {x : BitVec w} {i : Nat} :
+    x.getLsbD i = x[i]?.getD false := by
+  rw [getElem?_def]
+  split
+  · rfl
+  · simp_all
+
 /--
 This normalized a bitvec using `ofFin` to `ofNat`.
 -/
@@ -34,52 +105,73 @@ theorem eq_of_toNat_eq {n} : ∀ {x y : BitVec n}, x.toNat = y.toNat → x = y
 @[bv_toNat] theorem toNat_ne (x y : BitVec n) : x ≠ y ↔ x.toNat ≠ y.toNat := by
   rw [Ne, toNat_eq]
 
-theorem testBit_toNat (x : BitVec w) : x.toNat.testBit i = x.getLsb i := rfl
+theorem testBit_toNat (x : BitVec w) : x.toNat.testBit i = x.getLsbD i := rfl
 
-@[simp] theorem getLsb_ofFin (x : Fin (2^n)) (i : Nat) :
-  getLsb (BitVec.ofFin x) i = x.val.testBit i := rfl
+theorem getMsb'_eq_getLsb' (x : BitVec w) (i : Fin w) :
+    x.getMsb' i = x.getLsb' ⟨w - 1 - i, by omega⟩ := by
+  simp only [getMsb', getLsb']
 
-@[simp] theorem getLsb_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : getLsb x i = false := by
-  let ⟨x, x_lt⟩ := x
-  simp
-  apply Nat.testBit_lt_two_pow
-  have p : 2^w ≤ 2^i := Nat.pow_le_pow_of_le_right (by omega) ge
-  omega
+theorem getMsb?_eq_getLsb? (x : BitVec w) (i : Nat) :
+    x.getMsb? i = if i < w then x.getLsb? (w - 1 - i) else none := by
+  simp only [getMsb?, getLsb?_eq_getElem?]
+  split <;> simp [getMsb'_eq_getLsb']
 
-@[simp] theorem getMsb_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : getMsb x i = false := by
-  rw [getMsb]
-  simp only [Bool.and_eq_false_imp, decide_eq_true_eq]
-  omega
+theorem getMsbD_eq_getLsbD (x : BitVec w) (i : Nat) : x.getMsbD i = (decide (i < w) && x.getLsbD (w - 1 - i)) := by
+  rw [getMsbD, getLsbD]
 
-theorem lt_of_getLsb (x : BitVec w) (i : Nat) : getLsb x i = true → i < w := by
-  if h : i < w then
-    simp [h]
-  else
-    simp [Nat.ge_of_not_lt h]
-
-theorem lt_of_getMsb (x : BitVec w) (i : Nat) : getMsb x i = true → i < w := by
-  if h : i < w then
-    simp [h]
-  else
-    simp [Nat.ge_of_not_lt h]
-
-theorem getMsb_eq_getLsb (x : BitVec w) (i : Nat) : x.getMsb i = (decide (i < w) && x.getLsb (w - 1 - i)) := by
-  rw [getMsb]
-
-theorem getLsb_eq_getMsb (x : BitVec w) (i : Nat) : x.getLsb i = (decide (i < w) && x.getMsb (w - 1 - i)) := by
-  rw [getMsb]
+theorem getLsbD_eq_getMsbD (x : BitVec w) (i : Nat) : x.getLsbD i = (decide (i < w) && x.getMsbD (w - 1 - i)) := by
+  rw [getMsbD]
   by_cases h₁ : i < w <;> by_cases h₂ : w - 1 - i < w <;>
     simp only [h₁, h₂] <;> simp only [decide_True, decide_False, Bool.false_and, Bool.and_false, Bool.true_and, Bool.and_true]
   · congr
     omega
   all_goals
-    apply getLsb_ge
+    apply getLsbD_ge
     omega
 
--- We choose `eq_of_getLsb_eq` as the `@[ext]` theorem for `BitVec`
--- somewhat arbitrarily over `eq_of_getMsg_eq`.
-@[ext] theorem eq_of_getLsb_eq {x y : BitVec w}
-    (pred : ∀(i : Fin w), x.getLsb i.val = y.getLsb i.val) : x = y := by
+@[simp] theorem getLsb?_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : x[i]? = none := by
+  simp [ge]
+
+@[simp] theorem getMsb?_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : getMsb? x i = none := by
+  simp [getMsb?_eq_getLsb?]; omega
+
+theorem lt_of_getLsb?_eq_some (x : BitVec w) (i : Nat) : x[i]? = some b → i < w := by
+  cases h : x[i]? with
+  | none => simp
+  | some => by_cases i < w <;> simp_all
+
+theorem lt_of_getMsb?_eq_some (x : BitVec w) (i : Nat) : getMsb? x i = some b → i < w := by
+  if h : i < w then
+    simp [h]
+  else
+    simp [Nat.ge_of_not_lt h]
+
+theorem lt_of_getLsb?_isSome (x : BitVec w) (i : Nat) : x[i]?.isSome → i < w := by
+  cases h : x[i]? with
+  | none => simp
+  | some => by_cases i < w <;> simp_all
+
+theorem lt_of_getMsb?_isSome (x : BitVec w) (i : Nat) : (getMsb? x i).isSome → i < w := by
+  if h : i < w then
+    simp [h]
+  else
+    simp [Nat.ge_of_not_lt h]
+
+theorem getMsbD_eq_getMsb?_getD (x : BitVec w) (i : Nat) :
+    x.getMsbD i = (x.getMsb? i).getD false := by
+  rw [getMsbD_eq_getLsbD]
+  by_cases h : w = 0
+  · simp [getMsb?, h]
+  · rw [getLsbD_eq_getElem?_getD, getMsb?_eq_getLsb?]
+    split <;>
+    · simp
+      intros
+      omega
+
+-- We choose `eq_of_getLsbD_eq` as the `@[ext]` theorem for `BitVec`
+-- somewhat arbitrarily over `eq_of_getMsbD_eq`.
+@[ext] theorem eq_of_getLsbD_eq {x y : BitVec w}
+    (pred : ∀(i : Fin w), x.getLsbD i.val = y.getLsbD i.val) : x = y := by
   apply eq_of_toNat_eq
   apply Nat.eq_of_testBit_eq
   intro i
@@ -87,12 +179,12 @@ theorem getLsb_eq_getMsb (x : BitVec w) (i : Nat) : x.getLsb i = (decide (i < w)
     exact pred ⟨i, i_lt⟩
   else
     have p : i ≥ w := Nat.le_of_not_gt i_lt
-    simp [testBit_toNat, getLsb_ge _ _ p]
+    simp [testBit_toNat, getLsbD_ge _ _ p]
 
-theorem eq_of_getMsb_eq {x y : BitVec w}
-    (pred : ∀(i : Fin w), x.getMsb i = y.getMsb i.val) : x = y := by
-  simp only [getMsb] at pred
-  apply eq_of_getLsb_eq
+theorem eq_of_getMsbD_eq {x y : BitVec w}
+    (pred : ∀(i : Fin w), x.getMsbD i.val = y.getMsbD i.val) : x = y := by
+  simp only [getMsbD] at pred
+  apply eq_of_getLsbD_eq
   intro ⟨i, i_lt⟩
   if w_zero : w = 0 then
     simp [w_zero]
@@ -112,8 +204,8 @@ theorem eq_of_getMsb_eq {x y : BitVec w}
 theorem of_length_zero {x : BitVec 0} : x = 0#0 := by ext; simp
 
 @[simp] theorem toNat_zero_length (x : BitVec 0) : x.toNat = 0 := by simp [of_length_zero]
-theorem getLsb_zero_length (x : BitVec 0) : x.getLsb i = false := by simp
-theorem getMsb_zero_length (x : BitVec 0) : x.getMsb i = false := by simp
+theorem getLsbD_zero_length (x : BitVec 0) : x.getLsbD i = false := by simp
+theorem getMsbD_zero_length (x : BitVec 0) : x.getMsbD i = false := by simp
 @[simp] theorem msb_zero_length (x : BitVec 0) : x.msb = false := by simp [BitVec.msb, of_length_zero]
 
 theorem eq_of_toFin_eq : ∀ {x y : BitVec w}, x.toFin = y.toFin → x = y
@@ -123,7 +215,7 @@ theorem eq_of_toFin_eq : ∀ {x y : BitVec w}, x.toFin = y.toFin → x = y
   cases b <;> rfl
 
 @[simp] theorem msb_ofBool (b : Bool) : (ofBool b).msb = b := by
-  cases b <;> simp [BitVec.msb]
+  cases b <;> simp [BitVec.msb, getMsbD, getLsbD]
 
 theorem ofNat_one (n : Nat) : BitVec.ofNat 1 n = BitVec.ofBool (n % 2 = 1) :=  by
   rcases (Nat.mod_two_eq_zero_or_one n) with h | h <;> simp [h, BitVec.ofNat, Fin.ofNat']
@@ -137,9 +229,9 @@ theorem ofBool_eq_iff_eq : ∀(b b' : Bool), BitVec.ofBool b = BitVec.ofBool b'
 
 @[simp] theorem toNat_ofNatLt (x : Nat) (p : x < 2^w) : (x#'p).toNat = x := rfl
 
-@[simp] theorem getLsb_ofNatLt {n : Nat} (x : Nat) (lt : x < 2^n) (i : Nat) :
-  getLsb (x#'lt) i = x.testBit i := by
-  simp [getLsb, BitVec.ofNatLt]
+@[simp] theorem getLsbD_ofNatLt {n : Nat} (x : Nat) (lt : x < 2^n) (i : Nat) :
+  getLsbD (x#'lt) i = x.testBit i := by
+  simp [getLsbD, BitVec.ofNatLt]
 
 @[simp, bv_toNat] theorem toNat_ofNat (x w : Nat) : (BitVec.ofNat w x).toNat = x % 2^w := by
   simp [BitVec.toNat, BitVec.ofNat, Fin.ofNat']
@@ -148,13 +240,13 @@ theorem ofBool_eq_iff_eq : ∀(b b' : Bool), BitVec.ofBool b = BitVec.ofBool b'
 
 -- Remark: we don't use `[simp]` here because simproc` subsumes it for literals.
 -- If `x` and `n` are not literals, applying this theorem eagerly may not be a good idea.
-theorem getLsb_ofNat (n : Nat) (x : Nat) (i : Nat) :
-  getLsb (BitVec.ofNat n x) i = (i < n && x.testBit i) := by
-  simp [getLsb, BitVec.ofNat, Fin.val_ofNat']
+theorem getLsbD_ofNat (n : Nat) (x : Nat) (i : Nat) :
+  getLsbD (BitVec.ofNat n x) i = (i < n && x.testBit i) := by
+  simp [getLsbD, BitVec.ofNat, Fin.val_ofNat']
 
-@[simp] theorem getLsb_zero : (0#w).getLsb i = false := by simp [getLsb]
+@[simp] theorem getLsbD_zero : (0#w).getLsbD i = false := by simp [getLsbD]
 
-@[simp] theorem getMsb_zero : (0#w).getMsb i = false := by simp [getMsb]
+@[simp] theorem getMsbD_zero : (0#w).getMsbD i = false := by simp [getMsbD]
 
 @[simp] theorem toNat_mod_cancel (x : BitVec n) : x.toNat % (2^n) = x.toNat :=
   Nat.mod_eq_of_lt x.isLt
@@ -173,28 +265,28 @@ private theorem lt_two_pow_of_le {x m n : Nat} (lt : x < 2 ^ m) (le : m ≤ n) :
   Nat.lt_of_lt_of_le lt (Nat.pow_le_pow_of_le_right (by trivial : 0 < 2) le)
 
 @[simp]
-theorem getLsb_ofBool (b : Bool) (i : Nat) : (BitVec.ofBool b).getLsb i = ((i = 0) && b) := by
+theorem getLsbD_ofBool (b : Bool) (i : Nat) : (BitVec.ofBool b).getLsbD i = ((i = 0) && b) := by
   rcases b with rfl | rfl
   · simp [ofBool]
-  · simp only [ofBool, ofNat_eq_ofNat, cond_true, getLsb_ofNat, Bool.and_true]
+  · simp only [ofBool, ofNat_eq_ofNat, cond_true, getLsbD_ofNat, Bool.and_true]
     by_cases hi : i = 0 <;> simp [hi] <;> omega
 
 /-! ### msb -/
 
-@[simp] theorem msb_zero : (0#w).msb = false := by simp [BitVec.msb, getMsb]
+@[simp] theorem msb_zero : (0#w).msb = false := by simp [BitVec.msb, getMsbD]
 
-theorem msb_eq_getLsb_last (x : BitVec w) :
-    x.msb = x.getLsb (w - 1) := by
-  simp [BitVec.msb, getMsb, getLsb]
+theorem msb_eq_getLsbD_last (x : BitVec w) :
+    x.msb = x.getLsbD (w - 1) := by
+  simp [BitVec.msb, getMsbD, getLsbD]
   rcases w  with rfl | w
   · simp [BitVec.eq_nil x]
   · simp
 
-@[bv_toNat] theorem getLsb_last (x : BitVec w) :
-    x.getLsb (w-1) = decide (2 ^ (w-1) ≤ x.toNat) := by
+@[bv_toNat] theorem getLsbD_last (x : BitVec w) :
+    x.getLsbD (w-1) = decide (2 ^ (w-1) ≤ x.toNat) := by
   rcases w with rfl | w
   · simp
-  · simp only [getLsb, Nat.testBit_to_div_mod, Nat.succ_sub_succ_eq_sub, Nat.sub_zero]
+  · simp only [getLsbD, Nat.testBit_to_div_mod, Nat.succ_sub_succ_eq_sub, Nat.sub_zero]
     rcases (Nat.lt_or_ge (BitVec.toNat x) (2 ^ w)) with h | h
     · simp [Nat.div_eq_of_lt h, h]
     · simp only [h]
@@ -202,16 +294,16 @@ theorem msb_eq_getLsb_last (x : BitVec w) :
       · decide
       · omega
 
-@[bv_toNat] theorem getLsb_succ_last (x : BitVec (w + 1)) :
-    x.getLsb w = decide (2 ^ w ≤ x.toNat) := getLsb_last x
+@[bv_toNat] theorem getLsbD_succ_last (x : BitVec (w + 1)) :
+    x.getLsbD w = decide (2 ^ w ≤ x.toNat) := getLsbD_last x
 
 @[bv_toNat] theorem msb_eq_decide (x : BitVec w) : BitVec.msb x = decide (2 ^ (w-1) ≤ x.toNat) := by
-  simp [msb_eq_getLsb_last, getLsb_last]
+  simp [msb_eq_getLsbD_last, getLsbD_last]
 
 theorem toNat_ge_of_msb_true {x : BitVec n} (p : BitVec.msb x = true) : x.toNat ≥ 2^(n-1) := by
   match n with
   | 0 =>
-    simp [BitVec.msb, BitVec.getMsb] at p
+    simp [BitVec.msb, BitVec.getMsbD] at p
   | n + 1 =>
     simp [BitVec.msb_eq_decide] at p
     simp only [Nat.add_sub_cancel]
@@ -224,10 +316,10 @@ theorem toNat_ge_of_msb_true {x : BitVec n} (p : BitVec.msb x = true) : x.toNat
     (cast h x).toFin = x.toFin.cast (by rw [h]) :=
   rfl
 
-@[simp] theorem getLsb_cast (h : w = v) (x : BitVec w) : (cast h x).getLsb i = x.getLsb i := by
+@[simp] theorem getLsbD_cast (h : w = v) (x : BitVec w) : (cast h x).getLsbD i = x.getLsbD i := by
   subst h; simp
 
-@[simp] theorem getMsb_cast (h : w = v) (x : BitVec w) : (cast h x).getMsb i = x.getMsb i := by
+@[simp] theorem getMsbD_cast (h : w = v) (x : BitVec w) : (cast h x).getMsbD i = x.getMsbD i := by
   subst h; simp
 @[simp] theorem msb_cast (h : w = v) (x : BitVec w) : (cast h x).msb = x.msb := by
   simp [BitVec.msb]
@@ -369,53 +461,53 @@ theorem nat_eq_toNat (x : BitVec w) (y : Nat)
   rw [@eq_comm _ _ x.toNat]
   apply toNat_eq_nat
 
-@[simp] theorem getLsb_zeroExtend' (ge : m ≥ n) (x : BitVec n) (i : Nat) :
-    getLsb (zeroExtend' ge x) i = getLsb x i := by
-  simp [getLsb, toNat_zeroExtend']
+@[simp] theorem getLsbD_zeroExtend' (ge : m ≥ n) (x : BitVec n) (i : Nat) :
+    getLsbD (zeroExtend' ge x) i = getLsbD x i := by
+  simp [getLsbD, toNat_zeroExtend']
 
-@[simp] theorem getMsb_zeroExtend' (ge : m ≥ n) (x : BitVec n) (i : Nat) :
-    getMsb (zeroExtend' ge x) i = (decide (i ≥ m - n) && getMsb x (i - (m - n))) := by
-  simp only [getMsb, getLsb_zeroExtend', gt_iff_lt]
+@[simp] theorem getMsbD_zeroExtend' (ge : m ≥ n) (x : BitVec n) (i : Nat) :
+    getMsbD (zeroExtend' ge x) i = (decide (i ≥ m - n) && getMsbD x (i - (m - n))) := by
+  simp only [getMsbD, getLsbD_zeroExtend', gt_iff_lt]
   by_cases h₁ : decide (i < m) <;> by_cases h₂ : decide (i ≥ m - n) <;> by_cases h₃ : decide (i - (m - n) < n) <;>
     by_cases h₄ : n - 1 - (i - (m - n)) = m - 1 - i
   all_goals
     simp only [h₁, h₂, h₃, h₄]
     simp_all only [ge_iff_le, decide_eq_true_eq, Nat.not_le, Nat.not_lt, Bool.true_and,
       Bool.false_and, Bool.and_self] <;>
-    (try apply getLsb_ge) <;>
-    (try apply (getLsb_ge _ _ _).symm) <;>
+    (try apply getLsbD_ge) <;>
+    (try apply (getLsbD_ge _ _ _).symm) <;>
     omega
 
-@[simp] theorem getLsb_zeroExtend (m : Nat) (x : BitVec n) (i : Nat) :
-    getLsb (zeroExtend m x) i = (decide (i < m) && getLsb x i) := by
-  simp [getLsb, toNat_zeroExtend, Nat.testBit_mod_two_pow]
+@[simp] theorem getLsbD_zeroExtend (m : Nat) (x : BitVec n) (i : Nat) :
+    getLsbD (zeroExtend m x) i = (decide (i < m) && getLsbD x i) := by
+  simp [getLsbD, toNat_zeroExtend, Nat.testBit_mod_two_pow]
 
-@[simp] theorem getMsb_zeroExtend_add {x : BitVec w} (h : k ≤ i) :
-    (x.zeroExtend (w + k)).getMsb i = x.getMsb (i - k) := by
+@[simp] theorem getMsbD_zeroExtend_add {x : BitVec w} (h : k ≤ i) :
+    (x.zeroExtend (w + k)).getMsbD i = x.getMsbD (i - k) := by
   by_cases h : w = 0
   · subst h; simp [of_length_zero]
-  simp only [getMsb, getLsb_zeroExtend]
+  simp only [getMsbD, getLsbD_zeroExtend]
   by_cases h₁ : i < w + k <;> by_cases h₂ : i - k < w <;> by_cases h₃ : w + k - 1 - i < w + k
     <;> simp [h₁, h₂, h₃]
   · congr 1
     omega
-  all_goals (first | apply getLsb_ge | apply Eq.symm; apply getLsb_ge)
+  all_goals (first | apply getLsbD_ge | apply Eq.symm; apply getLsbD_ge)
     <;> omega
 
-theorem getLsb_truncate (m : Nat) (x : BitVec n) (i : Nat) :
-    getLsb (truncate m x) i = (decide (i < m) && getLsb x i) :=
-  getLsb_zeroExtend m x i
+theorem getLsbD_truncate (m : Nat) (x : BitVec n) (i : Nat) :
+    getLsbD (truncate m x) i = (decide (i < m) && getLsbD x i) :=
+  getLsbD_zeroExtend m x i
 
-theorem msb_truncate (x : BitVec w) : (x.truncate (k + 1)).msb = x.getLsb k := by
-  simp [BitVec.msb, getMsb]
+theorem msb_truncate (x : BitVec w) : (x.truncate (k + 1)).msb = x.getLsbD k := by
+  simp [BitVec.msb, getMsbD]
 
 @[simp] theorem zeroExtend_zeroExtend_of_le (x : BitVec w) (h : k ≤ l) :
     (x.zeroExtend l).zeroExtend k = x.zeroExtend k := by
   ext i
-  simp only [getLsb_zeroExtend, Fin.is_lt, decide_True, Bool.true_and]
-  have p := lt_of_getLsb x i
+  simp only [getLsbD_zeroExtend, Fin.is_lt, decide_True, Bool.true_and]
+  have p := lt_of_getLsbD x i
   revert p
-  cases getLsb x i <;> simp; omega
+  cases getLsbD x i <;> simp; omega
 
 @[simp] theorem truncate_truncate_of_le (x : BitVec w) (h : k ≤ l) :
     (x.truncate l).truncate k = x.truncate k :=
@@ -426,28 +518,28 @@ theorem msb_truncate (x : BitVec w) : (x.truncate (k + 1)).msb = x.getLsb k := b
 theorem truncate_eq_self {x : BitVec w} : x.truncate w = x := zeroExtend_eq _
 
 @[simp] theorem truncate_cast {h : w = v} : (cast h x).truncate k = x.truncate k := by
-  apply eq_of_getLsb_eq
+  apply eq_of_getLsbD_eq
   simp
 
-theorem msb_zeroExtend (x : BitVec w) : (x.zeroExtend v).msb = (decide (0 < v) && x.getLsb (v - 1)) := by
-  rw [msb_eq_getLsb_last]
-  simp only [getLsb_zeroExtend]
-  cases getLsb x (v - 1) <;> simp; omega
+theorem msb_zeroExtend (x : BitVec w) : (x.zeroExtend v).msb = (decide (0 < v) && x.getLsbD (v - 1)) := by
+  rw [msb_eq_getLsbD_last]
+  simp only [getLsbD_zeroExtend]
+  cases getLsbD x (v - 1) <;> simp; omega
 
-theorem msb_zeroExtend' (x : BitVec w) (h : w ≤ v) : (x.zeroExtend' h).msb = (decide (0 < v) && x.getLsb (v - 1)) := by
+theorem msb_zeroExtend' (x : BitVec w) (h : w ≤ v) : (x.zeroExtend' h).msb = (decide (0 < v) && x.getLsbD (v - 1)) := by
   rw [zeroExtend'_eq, msb_zeroExtend]
 
 /-- zero extending a bitvector to width 1 equals the boolean of the lsb. -/
 theorem zeroExtend_one_eq_ofBool_getLsb_zero (x : BitVec w) :
-    x.zeroExtend 1 = BitVec.ofBool (x.getLsb 0) := by
+    x.zeroExtend 1 = BitVec.ofBool (x.getLsbD 0) := by
   ext i
-  simp [getLsb_zeroExtend, Fin.fin_one_eq_zero i]
+  simp [getLsbD_zeroExtend, Fin.fin_one_eq_zero i]
 
 /-- Zero extending `1#v` to `1#w` equals `1#w` when `v > 0`. -/
 theorem zeroExtend_ofNat_one_eq_ofNat_one_of_lt {v w : Nat} (hv : 0 < v) :
     (BitVec.ofNat v 1).zeroExtend w = BitVec.ofNat w 1 := by
   ext ⟨i, hilt⟩
-  simp only [getLsb_zeroExtend, hilt, decide_True, getLsb_ofNat, Bool.true_and,
+  simp only [getLsbD_zeroExtend, hilt, decide_True, getLsbD_ofNat, Bool.true_and,
     Bool.and_iff_right_iff_imp, decide_eq_true_eq]
   intros hi₁
   have hv := Nat.testBit_one_eq_true_iff_self_eq_zero.mp hi₁
@@ -455,7 +547,7 @@ theorem zeroExtend_ofNat_one_eq_ofNat_one_of_lt {v w : Nat} (hv : 0 < v) :
 
 /-- Truncating to width 1 produces a bitvector equal to the least significant bit. -/
 theorem truncate_one {x : BitVec w} :
-    x.truncate 1 = ofBool (x.getLsb 0) := by
+    x.truncate 1 = ofBool (x.getLsbD 0) := by
   ext i
   simp [show i = 0 by omega]
 
@@ -468,7 +560,7 @@ protected theorem extractLsb_ofFin {n} (x : Fin (2^n)) (hi lo : Nat) :
 @[simp]
 protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
   extractLsb hi lo (BitVec.ofNat n x) = .ofNat (hi - lo + 1) ((x % 2^n) >>> lo) := by
-  apply eq_of_getLsb_eq
+  apply eq_of_getLsbD_eq
   intro ⟨i, _lt⟩
   simp [BitVec.ofNat]
 
@@ -478,13 +570,13 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
 @[simp] theorem extractLsb_toNat (hi lo : Nat) (x : BitVec n) :
   (extractLsb hi lo x).toNat = (x.toNat >>> lo) % 2^(hi-lo+1) := rfl
 
-@[simp] theorem getLsb_extractLsb' (start len : Nat) (x : BitVec n) (i : Nat) :
-    (extractLsb' start len x).getLsb i = (i < len && x.getLsb (start+i)) := by
-  simp [getLsb, Nat.lt_succ]
+@[simp] theorem getLsbD_extractLsb' (start len : Nat) (x : BitVec n) (i : Nat) :
+    (extractLsb' start len x).getLsbD i = (i < len && x.getLsbD (start+i)) := by
+  simp [getLsbD, Nat.lt_succ]
 
-@[simp] theorem getLsb_extract (hi lo : Nat) (x : BitVec n) (i : Nat) :
-    getLsb (extractLsb hi lo x) i = (i ≤ (hi-lo) && getLsb x (lo+i)) := by
-  simp [getLsb, Nat.lt_succ]
+@[simp] theorem getLsbD_extract (hi lo : Nat) (x : BitVec n) (i : Nat) :
+    getLsbD (extractLsb hi lo x) i = (i ≤ (hi-lo) && getLsbD x (lo+i)) := by
+  simp [getLsbD, Nat.lt_succ]
 
 theorem extractLsb'_eq_extractLsb {w : Nat} (x : BitVec w) (start len : Nat) (h : len > 0) :
     x.extractLsb' start len = (x.extractLsb (len - 1 + start) start).cast (by omega) := by
@@ -497,7 +589,7 @@ theorem extractLsb'_eq_extractLsb {w : Nat} (x : BitVec w) (start len : Nat) (h
   unfold allOnes
   simp
 
-@[simp] theorem getLsb_allOnes : (allOnes v).getLsb i = decide (i < v) := by
+@[simp] theorem getLsbD_allOnes : (allOnes v).getLsbD i = decide (i < v) := by
   simp [allOnes]
 
 /-! ### or -/
@@ -510,12 +602,12 @@ theorem extractLsb'_eq_extractLsb {w : Nat} (x : BitVec w) (start len : Nat) (h
   apply Fin.eq_of_val_eq
   exact (Nat.mod_eq_of_lt <| Nat.or_lt_two_pow x.isLt y.isLt).symm
 
-@[simp] theorem getLsb_or {x y : BitVec v} : (x ||| y).getLsb i = (x.getLsb i || y.getLsb i) := by
-  rw [← testBit_toNat, getLsb, getLsb]
+@[simp] theorem getLsbD_or {x y : BitVec v} : (x ||| y).getLsbD i = (x.getLsbD i || y.getLsbD i) := by
+  rw [← testBit_toNat, getLsbD, getLsbD]
   simp
 
-@[simp] theorem getMsb_or {x y : BitVec w} : (x ||| y).getMsb i = (x.getMsb i || y.getMsb i) := by
-  simp only [getMsb]
+@[simp] theorem getMsbD_or {x y : BitVec w} : (x ||| y).getMsbD i = (x.getMsbD i || y.getMsbD i) := by
+  simp only [getMsbD]
   by_cases h : i < w <;> simp [h]
 
 @[simp] theorem msb_or {x y : BitVec w} : (x ||| y).msb = (x.msb || y.msb) := by
@@ -548,12 +640,12 @@ instance : Std.Commutative (fun (x y : BitVec w) => x ||| y) := ⟨BitVec.or_com
   apply Fin.eq_of_val_eq
   exact (Nat.mod_eq_of_lt <| Nat.and_lt_two_pow _ y.isLt).symm
 
-@[simp] theorem getLsb_and {x y : BitVec v} : (x &&& y).getLsb i = (x.getLsb i && y.getLsb i) := by
-  rw [← testBit_toNat, getLsb, getLsb]
+@[simp] theorem getLsbD_and {x y : BitVec v} : (x &&& y).getLsbD i = (x.getLsbD i && y.getLsbD i) := by
+  rw [← testBit_toNat, getLsbD, getLsbD]
   simp
 
-@[simp] theorem getMsb_and {x y : BitVec w} : (x &&& y).getMsb i = (x.getMsb i && y.getMsb i) := by
-  simp only [getMsb]
+@[simp] theorem getMsbD_and {x y : BitVec w} : (x &&& y).getMsbD i = (x.getMsbD i && y.getMsbD i) := by
+  simp only [getMsbD]
   by_cases h : i < w <;> simp [h]
 
 @[simp] theorem msb_and {x y : BitVec w} : (x &&& y).msb = (x.msb && y.msb) := by
@@ -586,14 +678,14 @@ instance : Std.Commutative (fun (x y : BitVec w) => x &&& y) := ⟨BitVec.and_co
   apply Fin.eq_of_val_eq
   exact (Nat.mod_eq_of_lt <| Nat.xor_lt_two_pow x.isLt y.isLt).symm
 
-@[simp] theorem getLsb_xor {x y : BitVec v} :
-    (x ^^^ y).getLsb i = (xor (x.getLsb i) (y.getLsb i)) := by
-  rw [← testBit_toNat, getLsb, getLsb]
+@[simp] theorem getLsbD_xor {x y : BitVec v} :
+    (x ^^^ y).getLsbD i = (xor (x.getLsbD i) (y.getLsbD i)) := by
+  rw [← testBit_toNat, getLsbD, getLsbD]
   simp
 
-@[simp] theorem getMsb_xor {x y : BitVec w} :
-    (x ^^^ y).getMsb i = (xor (x.getMsb i) (y.getMsb i)) := by
-  simp only [getMsb]
+@[simp] theorem getMsbD_xor {x y : BitVec w} :
+    (x ^^^ y).getMsbD i = (xor (x.getMsbD i) (y.getMsbD i)) := by
+  simp only [getMsbD]
   by_cases h : i < w <;> simp [h]
 
 @[simp] theorem msb_xor {x y : BitVec w} :
@@ -646,7 +738,7 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
   simp only [val_toFin, toNat_not, Fin.val_rev]
   omega
 
-@[simp] theorem getLsb_not {x : BitVec v} : (~~~x).getLsb i = (decide (i < v) && ! x.getLsb i) := by
+@[simp] theorem getLsbD_not {x : BitVec v} : (~~~x).getLsbD i = (decide (i < v) && ! x.getLsbD i) := by
   by_cases h' : i < v <;> simp_all [not_def]
 
 @[simp] theorem truncate_not {x : BitVec w} (h : k ≤ w) :
@@ -659,19 +751,19 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
 
 @[simp] theorem not_cast {x : BitVec w} (h : w = w') : ~~~(cast h x) = cast h (~~~x) := by
   ext
-  simp_all [lt_of_getLsb]
+  simp_all [lt_of_getLsbD]
 
 @[simp] theorem and_cast {x y : BitVec w} (h : w = w') : cast h x &&& cast h y = cast h (x &&& y) := by
   ext
-  simp_all [lt_of_getLsb]
+  simp_all [lt_of_getLsbD]
 
 @[simp] theorem or_cast {x y : BitVec w} (h : w = w') : cast h x ||| cast h y = cast h (x ||| y) := by
   ext
-  simp_all [lt_of_getLsb]
+  simp_all [lt_of_getLsbD]
 
 @[simp] theorem xor_cast {x y : BitVec w} (h : w = w') : cast h x ^^^ cast h y = cast h (x ^^^ y) := by
   ext
-  simp_all [lt_of_getLsb]
+  simp_all [lt_of_getLsbD]
 
 /-! ### shiftLeft -/
 
@@ -691,9 +783,9 @@ theorem shiftLeft_zero_eq (x : BitVec w) : x <<< 0 = x := by
 theorem zero_shiftLeft (n : Nat) : 0#w <<< n = 0#w := by
   simp [bv_toNat]
 
-@[simp] theorem getLsb_shiftLeft (x : BitVec m) (n) :
-    getLsb (x <<< n) i = (decide (i < m) && !decide (i < n) && getLsb x (i - n)) := by
-  rw [← testBit_toNat, getLsb]
+@[simp] theorem getLsbD_shiftLeft (x : BitVec m) (n) :
+    getLsbD (x <<< n) i = (decide (i < m) && !decide (i < n) && getLsbD x (i - n)) := by
+  rw [← testBit_toNat, getLsbD]
   simp only [toNat_shiftLeft, Nat.testBit_mod_two_pow, Nat.testBit_shiftLeft, ge_iff_le]
   -- This step could be a case bashing tactic.
   cases h₁ : decide (i < m) <;> cases h₂ : decide (n ≤ i) <;> cases h₃ : decide (i < n)
@@ -702,27 +794,27 @@ theorem zero_shiftLeft (n : Nat) : 0#w <<< n = 0#w := by
 theorem shiftLeft_xor_distrib (x y : BitVec w) (n : Nat) :
     (x ^^^ y) <<< n = (x <<< n) ^^^ (y <<< n) := by
   ext i
-  simp only [getLsb_shiftLeft, Fin.is_lt, decide_True, Bool.true_and, getLsb_xor]
+  simp only [getLsbD_shiftLeft, Fin.is_lt, decide_True, Bool.true_and, getLsbD_xor]
   by_cases h : i < n
     <;> simp [h]
 
 theorem shiftLeft_and_distrib (x y : BitVec w) (n : Nat) :
     (x &&& y) <<< n = (x <<< n) &&& (y <<< n) := by
   ext i
-  simp only [getLsb_shiftLeft, Fin.is_lt, decide_True, Bool.true_and, getLsb_and]
+  simp only [getLsbD_shiftLeft, Fin.is_lt, decide_True, Bool.true_and, getLsbD_and]
   by_cases h : i < n
     <;> simp [h]
 
 theorem shiftLeft_or_distrib (x y : BitVec w) (n : Nat) :
     (x ||| y) <<< n = (x <<< n) ||| (y <<< n) := by
   ext i
-  simp only [getLsb_shiftLeft, Fin.is_lt, decide_True, Bool.true_and, getLsb_or]
+  simp only [getLsbD_shiftLeft, Fin.is_lt, decide_True, Bool.true_and, getLsbD_or]
   by_cases h : i < n
     <;> simp [h]
 
-@[simp] theorem getMsb_shiftLeft (x : BitVec w) (i) :
-    (x <<< i).getMsb k = x.getMsb (k + i) := by
-  simp only [getMsb, getLsb_shiftLeft]
+@[simp] theorem getMsbD_shiftLeft (x : BitVec w) (i) :
+    (x <<< i).getMsbD k = x.getMsbD (k + i) := by
+  simp only [getMsbD, getLsbD_shiftLeft]
   by_cases h : w = 0
   · subst h; simp
   have t : w - 1 - k < w := by omega
@@ -730,7 +822,7 @@ theorem shiftLeft_or_distrib (x y : BitVec w) (n : Nat) :
   simp only [decide_True, Nat.sub_sub, Bool.true_and, Nat.add_assoc]
   by_cases h₁ : k < w <;> by_cases h₂ : w - (1 + k) < i <;> by_cases h₃ : k + i < w
     <;> simp [h₁, h₂, h₃]
-    <;> (first | apply getLsb_ge | apply Eq.symm; apply getLsb_ge)
+    <;> (first | apply getLsbD_ge | apply Eq.symm; apply getLsbD_ge)
     <;> omega
 
 theorem shiftLeftZeroExtend_eq {x : BitVec w} :
@@ -744,16 +836,16 @@ theorem shiftLeftZeroExtend_eq {x : BitVec w} :
     exact Nat.mul_lt_mul_of_pos_right x.isLt (Nat.two_pow_pos _)
   · omega
 
-@[simp] theorem getLsb_shiftLeftZeroExtend (x : BitVec m) (n : Nat) :
-    getLsb (shiftLeftZeroExtend x n) i = ((! decide (i < n)) && getLsb x (i - n)) := by
+@[simp] theorem getLsbD_shiftLeftZeroExtend (x : BitVec m) (n : Nat) :
+    getLsbD (shiftLeftZeroExtend x n) i = ((! decide (i < n)) && getLsbD x (i - n)) := by
   rw [shiftLeftZeroExtend_eq]
-  simp only [getLsb_shiftLeft, getLsb_zeroExtend]
+  simp only [getLsbD_shiftLeft, getLsbD_zeroExtend]
   cases h₁ : decide (i < n) <;> cases h₂ : decide (i - n < m + n) <;> cases h₃ : decide (i < m + n)
     <;> simp_all
-    <;> (rw [getLsb_ge]; omega)
+    <;> (rw [getLsbD_ge]; omega)
 
-@[simp] theorem getMsb_shiftLeftZeroExtend (x : BitVec m) (n : Nat) :
-    getMsb (shiftLeftZeroExtend x n) i = getMsb x i := by
+@[simp] theorem getMsbD_shiftLeftZeroExtend (x : BitVec m) (n : Nat) :
+    getMsbD (shiftLeftZeroExtend x n) i = getMsbD x i := by
   have : n ≤ i + n := by omega
   simp_all [shiftLeftZeroExtend_eq]
 
@@ -764,7 +856,7 @@ theorem shiftLeftZeroExtend_eq {x : BitVec w} :
 theorem shiftLeft_add {w : Nat} (x : BitVec w) (n m : Nat) :
     x <<< (n + m) = (x <<< n) <<< m := by
   ext i
-  simp only [getLsb_shiftLeft, Fin.is_lt, decide_True, Bool.true_and]
+  simp only [getLsbD_shiftLeft, Fin.is_lt, decide_True, Bool.true_and]
   rw [show i - (n + m) = (i - m - n) by omega]
   cases h₂ : decide (i < m) <;>
   cases h₃ : decide (i - m < w) <;>
@@ -788,18 +880,18 @@ theorem shiftLeft_shiftLeft' {x : BitVec w₁} {y : BitVec w₂} {z : BitVec w
     x <<< y <<< z = x <<< (y.toNat + z.toNat) := by
   simp [shiftLeft_add]
 
-theorem getLsb_shiftLeft' {x : BitVec w₁} {y : BitVec w₂} {i : Nat} :
-    (x <<< y).getLsb i = (decide (i < w₁) && !decide (i < y.toNat) && x.getLsb (i - y.toNat)) := by
-  simp [shiftLeft_eq', getLsb_shiftLeft]
+theorem getLsbD_shiftLeft' {x : BitVec w₁} {y : BitVec w₂} {i : Nat} :
+    (x <<< y).getLsbD i = (decide (i < w₁) && !decide (i < y.toNat) && x.getLsbD (i - y.toNat)) := by
+  simp [shiftLeft_eq', getLsbD_shiftLeft]
 
 /-! ### ushiftRight -/
 
 @[simp, bv_toNat] theorem toNat_ushiftRight (x : BitVec n) (i : Nat) :
     (x >>> i).toNat = x.toNat >>> i := rfl
 
-@[simp] theorem getLsb_ushiftRight (x : BitVec n) (i j : Nat) :
-    getLsb (x >>> i) j = getLsb x (i+j) := by
-  unfold getLsb ; simp
+@[simp] theorem getLsbD_ushiftRight (x : BitVec n) (i j : Nat) :
+    getLsbD (x >>> i) j = getLsbD x (i+j) := by
+  unfold getLsbD ; simp
 
 theorem ushiftRight_xor_distrib (x y : BitVec w) (n : Nat) :
     (x ^^^ y) >>> n = (x >>> n) ^^^ (y >>> n) := by
@@ -869,22 +961,22 @@ theorem sshiftRight_eq_of_msb_true {x : BitVec w} {s : Nat} (h : x.msb = true) :
     · rw [Nat.shiftRight_eq_div_pow]
       apply Nat.lt_of_le_of_lt (Nat.div_le_self _ _) (by omega)
 
-@[simp] theorem getLsb_sshiftRight (x : BitVec w) (s i : Nat) :
-    getLsb (x.sshiftRight s) i =
-      (!decide (w ≤ i) && if s + i < w then x.getLsb (s + i) else x.msb) := by
+@[simp] theorem getLsbD_sshiftRight (x : BitVec w) (s i : Nat) :
+    getLsbD (x.sshiftRight s) i =
+      (!decide (w ≤ i) && if s + i < w then x.getLsbD (s + i) else x.msb) := by
   rcases hmsb : x.msb with rfl | rfl
-  · simp only [sshiftRight_eq_of_msb_false hmsb, getLsb_ushiftRight, Bool.if_false_right]
+  · simp only [sshiftRight_eq_of_msb_false hmsb, getLsbD_ushiftRight, Bool.if_false_right]
     by_cases hi : i ≥ w
     · simp only [hi, decide_True, Bool.not_true, Bool.false_and]
-      apply getLsb_ge
+      apply getLsbD_ge
       omega
     · simp only [hi, decide_False, Bool.not_false, Bool.true_and, Bool.iff_and_self,
         decide_eq_true_eq]
       intros hlsb
-      apply BitVec.lt_of_getLsb _ _ hlsb
+      apply BitVec.lt_of_getLsbD _ _ hlsb
   · by_cases hi : i ≥ w
     · simp [hi]
-    · simp only [sshiftRight_eq_of_msb_true hmsb, getLsb_not, getLsb_ushiftRight, Bool.not_and,
+    · simp only [sshiftRight_eq_of_msb_true hmsb, getLsbD_not, getLsbD_ushiftRight, Bool.not_and,
         Bool.not_not, hi, decide_False, Bool.not_false, Bool.if_true_right, Bool.true_and,
         Bool.and_iff_right_iff_imp, Bool.or_eq_true, Bool.not_eq_true', decide_eq_false_iff_not,
         Nat.not_lt, decide_eq_true_eq]
@@ -893,7 +985,7 @@ theorem sshiftRight_eq_of_msb_true {x : BitVec w} {s : Nat} (h : x.msb = true) :
 theorem sshiftRight_xor_distrib (x y : BitVec w) (n : Nat) :
     (x ^^^ y).sshiftRight n = (x.sshiftRight n) ^^^ (y.sshiftRight n) := by
   ext i
-  simp only [getLsb_sshiftRight, getLsb_xor, msb_xor]
+  simp only [getLsbD_sshiftRight, getLsbD_xor, msb_xor]
   split
     <;> by_cases w ≤ i
     <;> simp [*]
@@ -901,7 +993,7 @@ theorem sshiftRight_xor_distrib (x y : BitVec w) (n : Nat) :
 theorem sshiftRight_and_distrib (x y : BitVec w) (n : Nat) :
     (x &&& y).sshiftRight n = (x.sshiftRight n) &&& (y.sshiftRight n) := by
   ext i
-  simp only [getLsb_sshiftRight, getLsb_and, msb_and]
+  simp only [getLsbD_sshiftRight, getLsbD_and, msb_and]
   split
     <;> by_cases w ≤ i
     <;> simp [*]
@@ -909,7 +1001,7 @@ theorem sshiftRight_and_distrib (x y : BitVec w) (n : Nat) :
 theorem sshiftRight_or_distrib (x y : BitVec w) (n : Nat) :
     (x ||| y).sshiftRight n = (x.sshiftRight n) ||| (y.sshiftRight n) := by
   ext i
-  simp only [getLsb_sshiftRight, getLsb_or, msb_or]
+  simp only [getLsbD_sshiftRight, getLsbD_or, msb_or]
   split
     <;> by_cases w ≤ i
     <;> simp [*]
@@ -917,7 +1009,7 @@ theorem sshiftRight_or_distrib (x y : BitVec w) (n : Nat) :
 /-- The msb after arithmetic shifting right equals the original msb. -/
 theorem sshiftRight_msb_eq_msb {n : Nat} {x : BitVec w} :
     (x.sshiftRight n).msb = x.msb := by
-  rw [msb_eq_getLsb_last, getLsb_sshiftRight, msb_eq_getLsb_last]
+  rw [msb_eq_getLsbD_last, getLsbD_sshiftRight, msb_eq_getLsbD_last]
   by_cases hw₀ : w = 0
   · simp [hw₀]
   · simp only [show ¬(w ≤ w - 1) by omega, decide_False, Bool.not_false, Bool.true_and,
@@ -932,7 +1024,7 @@ theorem sshiftRight_msb_eq_msb {n : Nat} {x : BitVec w} :
 theorem sshiftRight_add {x : BitVec w} {m n : Nat} :
     x.sshiftRight (m + n) = (x.sshiftRight m).sshiftRight n := by
   ext i
-  simp only [getLsb_sshiftRight, Nat.add_assoc]
+  simp only [getLsbD_sshiftRight, Nat.add_assoc]
   by_cases h₁ : w ≤ (i : Nat)
   · simp [h₁]
   · simp only [h₁, decide_False, Bool.not_false, Bool.true_and]
@@ -990,12 +1082,12 @@ theorem signExtend_eq_not_zeroExtend_not_of_msb_false {x : BitVec w} {v : Nat} (
     x.signExtend v = x.zeroExtend v := by
   ext i
   by_cases hv : i < v
-  · simp only [signExtend, getLsb, getLsb_zeroExtend, hv, decide_True, Bool.true_and, toNat_ofInt,
+  · simp only [signExtend, getLsbD, getLsbD_zeroExtend, hv, decide_True, Bool.true_and, toNat_ofInt,
       BitVec.toInt_eq_msb_cond, hmsb, ↓reduceIte, reduceCtorEq]
     rw [Int.ofNat_mod_ofNat, Int.toNat_ofNat, Nat.testBit_mod_two_pow]
     simp [BitVec.testBit_toNat]
-  · simp only [getLsb_zeroExtend, hv, decide_False, Bool.false_and]
-    apply getLsb_ge
+  · simp only [getLsbD_zeroExtend, hv, decide_False, Bool.false_and]
+    apply getLsbD_ge
     omega
 
 /--
@@ -1019,8 +1111,8 @@ theorem signExtend_eq_not_zeroExtend_not_of_msb_true {x : BitVec w} {v : Nat} (h
     · apply Nat.le_refl
   · omega
 
-@[simp] theorem getLsb_signExtend (x  : BitVec w) {v i : Nat} :
-    (x.signExtend v).getLsb i = (decide (i < v) && if i < w then x.getLsb i else x.msb) := by
+@[simp] theorem getLsbD_signExtend (x  : BitVec w) {v i : Nat} :
+    (x.signExtend v).getLsbD i = (decide (i < v) && if i < w then x.getLsbD i else x.msb) := by
   rcases hmsb : x.msb with rfl | rfl
   · rw [signExtend_eq_not_zeroExtend_not_of_msb_false hmsb]
     by_cases (i < v) <;> by_cases (i < w) <;> simp_all <;> omega
@@ -1031,7 +1123,7 @@ theorem signExtend_eq_not_zeroExtend_not_of_msb_true {x : BitVec w} {v : Nat} (h
 theorem signExtend_eq_truncate_of_lt (x : BitVec w) {v : Nat} (hv : v ≤ w):
   x.signExtend v = x.truncate v := by
   ext i
-  simp only [getLsb_signExtend, Fin.is_lt, decide_True, Bool.true_and, getLsb_zeroExtend,
+  simp only [getLsbD_signExtend, Fin.is_lt, decide_True, Bool.true_and, getLsbD_zeroExtend,
     ite_eq_left_iff, Nat.not_lt]
   omega
 
@@ -1048,15 +1140,15 @@ theorem append_def (x : BitVec v) (y : BitVec w) :
     (x ++ y).toNat = x.toNat <<< n ||| y.toNat :=
   rfl
 
-@[simp] theorem getLsb_append {x : BitVec n} {y : BitVec m} :
-    getLsb (x ++ y) i = bif i < m then getLsb y i else getLsb x (i - m) := by
-  simp only [append_def, getLsb_or, getLsb_shiftLeftZeroExtend, getLsb_zeroExtend']
+@[simp] theorem getLsbD_append {x : BitVec n} {y : BitVec m} :
+    getLsbD (x ++ y) i = bif i < m then getLsbD y i else getLsbD x (i - m) := by
+  simp only [append_def, getLsbD_or, getLsbD_shiftLeftZeroExtend, getLsbD_zeroExtend']
   by_cases h : i < m
   · simp [h]
   · simp [h]; simp_all
 
-@[simp] theorem getMsb_append {x : BitVec n} {y : BitVec m} :
-    getMsb (x ++ y) i = bif n ≤ i then getMsb y (i - n) else getMsb x i := by
+@[simp] theorem getMsbD_append {x : BitVec n} {y : BitVec m} :
+    getMsbD (x ++ y) i = bif n ≤ i then getMsbD y (i - n) else getMsbD x i := by
   simp [append_def]
   by_cases h : n ≤ i
   · simp [h]
@@ -1068,17 +1160,17 @@ theorem msb_append {x : BitVec w} {y : BitVec v} :
   simp [msb_zeroExtend']
   by_cases h : w = 0
   · subst h
-    simp [BitVec.msb, getMsb]
+    simp [BitVec.msb, getMsbD]
   · rw [cond_eq_if]
     have q : 0 < w + v := by omega
-    have t : y.getLsb (w + v - 1) = false := getLsb_ge _ _ (by omega)
-    simp [h, q, t, BitVec.msb, getMsb]
+    have t : y.getLsbD (w + v - 1) = false := getLsbD_ge _ _ (by omega)
+    simp [h, q, t, BitVec.msb, getMsbD]
 
 @[simp] theorem truncate_append {x : BitVec w} {y : BitVec v} :
     (x ++ y).truncate k = if h : k ≤ v then y.truncate k else (x.truncate (k - v) ++ y).cast (by omega) := by
-  apply eq_of_getLsb_eq
+  apply eq_of_getLsbD_eq
   intro i
-  simp only [getLsb_zeroExtend, Fin.is_lt, decide_True, getLsb_append, Bool.true_and]
+  simp only [getLsbD_zeroExtend, Fin.is_lt, decide_True, getLsbD_append, Bool.true_and]
   split
   · have t : i < v := by omega
     simp [t]
@@ -1092,7 +1184,7 @@ theorem msb_append {x : BitVec w} {y : BitVec v} :
 
 @[simp] theorem not_append {x : BitVec w} {y : BitVec v} : ~~~ (x ++ y) = (~~~ x) ++ (~~~ y) := by
   ext i
-  simp only [getLsb_not, getLsb_append, cond_eq_if]
+  simp only [getLsbD_not, getLsbD_append, cond_eq_if]
   split
   · simp_all
   · simp_all; omega
@@ -1100,19 +1192,19 @@ theorem msb_append {x : BitVec w} {y : BitVec v} :
 @[simp] theorem and_append {x₁ x₂ : BitVec w} {y₁ y₂ : BitVec v} :
     (x₁ ++ y₁) &&& (x₂ ++ y₂) = (x₁ &&& x₂) ++ (y₁ &&& y₂) := by
   ext i
-  simp only [getLsb_append, cond_eq_if]
+  simp only [getLsbD_append, cond_eq_if]
   split <;> simp [*]
 
 @[simp] theorem or_append {x₁ x₂ : BitVec w} {y₁ y₂ : BitVec v} :
     (x₁ ++ y₁) ||| (x₂ ++ y₂) = (x₁ ||| x₂) ++ (y₁ ||| y₂) := by
   ext i
-  simp only [getLsb_append, cond_eq_if]
+  simp only [getLsbD_append, cond_eq_if]
   split <;> simp [*]
 
 @[simp] theorem xor_append {x₁ x₂ : BitVec w} {y₁ y₂ : BitVec v} :
     (x₁ ++ y₁) ^^^ (x₂ ++ y₂) = (x₁ ^^^ x₂) ++ (y₁ ^^^ y₂) := by
   ext i
-  simp only [getLsb_append, cond_eq_if]
+  simp only [getLsbD_append, cond_eq_if]
   split <;> simp [*]
 
 theorem shiftRight_add {w : Nat} (x : BitVec w) (n m : Nat) :
@@ -1127,15 +1219,15 @@ theorem shiftRight_shiftRight {w : Nat} (x : BitVec w) (n m : Nat) :
 
 /-! ### rev -/
 
-theorem getLsb_rev (x : BitVec w) (i : Fin w) :
-    x.getLsb i.rev = x.getMsb i := by
-  simp [getLsb, getMsb]
+theorem getLsbD_rev (x : BitVec w) (i : Fin w) :
+    x.getLsbD i.rev = x.getMsbD i := by
+  simp [getLsbD, getMsbD]
   congr 1
   omega
 
-theorem getMsb_rev (x : BitVec w) (i : Fin w) :
-    x.getMsb i.rev = x.getLsb i := by
-  simp only [← getLsb_rev]
+theorem getMsbD_rev (x : BitVec w) (i : Fin w) :
+    x.getMsbD i.rev = x.getLsbD i := by
+  simp only [← getLsbD_rev]
   simp only [Fin.rev]
   congr
   omega
@@ -1152,9 +1244,9 @@ theorem toNat_cons' {x : BitVec w} :
     (cons a x).toNat = (a.toNat <<< w) + x.toNat := by
   simp [cons, Nat.shiftLeft_eq, Nat.mul_comm _ (2^w), Nat.mul_add_lt_is_or, x.isLt]
 
-@[simp] theorem getLsb_cons (b : Bool) {n} (x : BitVec n) (i : Nat) :
-    getLsb (cons b x) i = if i = n then b else getLsb x i := by
-  simp only [getLsb, toNat_cons, Nat.testBit_or]
+@[simp] theorem getLsbD_cons (b : Bool) {n} (x : BitVec n) (i : Nat) :
+    getLsbD (cons b x) i = if i = n then b else getLsbD x i := by
+  simp only [getLsbD, toNat_cons, Nat.testBit_or]
   rw [Nat.testBit_shiftLeft]
   rcases Nat.lt_trichotomy i n with i_lt_n | i_eq_n | n_lt_i
   · have p1 : ¬(n ≤ i) := by omega
@@ -1169,17 +1261,17 @@ theorem toNat_cons' {x : BitVec w} :
 @[simp] theorem msb_cons : (cons a x).msb = a := by
   simp [cons, msb_cast, msb_append]
 
-@[simp] theorem getMsb_cons_zero : (cons a x).getMsb 0 = a := by
+@[simp] theorem getMsbD_cons_zero : (cons a x).getMsbD 0 = a := by
   rw [← BitVec.msb, msb_cons]
 
-@[simp] theorem getMsb_cons_succ : (cons a x).getMsb (i + 1) = x.getMsb i := by
+@[simp] theorem getMsbD_cons_succ : (cons a x).getMsbD (i + 1) = x.getMsbD i := by
   simp [cons, Nat.le_add_left 1 i]
 
 theorem truncate_succ (x : BitVec w) :
-    truncate (i+1) x = cons (getLsb x i) (truncate i x) := by
-  apply eq_of_getLsb_eq
+    truncate (i+1) x = cons (getLsbD x i) (truncate i x) := by
+  apply eq_of_getLsbD_eq
   intro j
-  simp only [getLsb_truncate, getLsb_cons, j.isLt, decide_True, Bool.true_and]
+  simp only [getLsbD_truncate, getLsbD_cons, j.isLt, decide_True, Bool.true_and]
   if j_eq : j.val = i then
     simp [j_eq]
   else
@@ -1190,7 +1282,7 @@ theorem eq_msb_cons_truncate (x : BitVec (w+1)) : x = (cons x.msb (x.truncate w)
   ext i
   simp
   split <;> rename_i h
-  · simp [BitVec.msb, getMsb, h]
+  · simp [BitVec.msb, getMsbD, h]
   · by_cases h' : i < w
     · simp_all
     · omega
@@ -1221,18 +1313,18 @@ theorem eq_msb_cons_truncate (x : BitVec (w+1)) : x = (cons x.msb (x.truncate w)
   · rintro (_ | i)
     <;> simp [Nat.add_mod, Nat.add_comm, Nat.add_mul_div_right]
 
-theorem getLsb_concat (x : BitVec w) (b : Bool) (i : Nat) :
-    (concat x b).getLsb i = if i = 0 then b else x.getLsb (i - 1) := by
-  simp only [concat, getLsb, toNat_append, toNat_ofBool, Nat.testBit_or, Nat.shiftLeft_eq]
+theorem getLsbD_concat (x : BitVec w) (b : Bool) (i : Nat) :
+    (concat x b).getLsbD i = if i = 0 then b else x.getLsbD (i - 1) := by
+  simp only [concat, getLsbD, toNat_append, toNat_ofBool, Nat.testBit_or, Nat.shiftLeft_eq]
   cases i
   · simp [Nat.mod_eq_of_lt b.toNat_lt]
   · simp [Nat.div_eq_of_lt b.toNat_lt]
 
-@[simp] theorem getLsb_concat_zero : (concat x b).getLsb 0 = b := by
-  simp [getLsb_concat]
+@[simp] theorem getLsbD_concat_zero : (concat x b).getLsbD 0 = b := by
+  simp [getLsbD_concat]
 
-@[simp] theorem getLsb_concat_succ : (concat x b).getLsb (i + 1) = x.getLsb i := by
-  simp [getLsb_concat]
+@[simp] theorem getLsbD_concat_succ : (concat x b).getLsbD (i + 1) = x.getLsbD i := by
+  simp [getLsbD_concat]
 
 @[simp] theorem not_concat (x : BitVec w) (b : Bool) : ~~~(concat x b) = concat (~~~x) !b := by
   ext i; cases i using Fin.succRecOn <;> simp [*, Nat.succ_lt_succ]
@@ -1468,19 +1560,19 @@ protected theorem lt_of_le_ne (x y : BitVec n) (h1 : x <= y) (h2 : ¬ x = y) : x
 
 /-! ### ofBoolList -/
 
-@[simp] theorem getMsb_ofBoolListBE : (ofBoolListBE bs).getMsb i = bs.getD i false := by
+@[simp] theorem getMsbD_ofBoolListBE : (ofBoolListBE bs).getMsbD i = bs.getD i false := by
   induction bs generalizing i <;> cases i <;> simp_all [ofBoolListBE]
 
-@[simp] theorem getLsb_ofBoolListBE :
-    (ofBoolListBE bs).getLsb i = (decide (i < bs.length) && bs.getD (bs.length - 1 - i) false) := by
-  simp [getLsb_eq_getMsb]
+@[simp] theorem getLsbD_ofBoolListBE :
+    (ofBoolListBE bs).getLsbD i = (decide (i < bs.length) && bs.getD (bs.length - 1 - i) false) := by
+  simp [getLsbD_eq_getMsbD]
 
-@[simp] theorem getLsb_ofBoolListLE : (ofBoolListLE bs).getLsb i = bs.getD i false := by
+@[simp] theorem getLsb_ofBoolListLE : (ofBoolListLE bs).getLsbD i = bs.getD i false := by
   induction bs generalizing i <;> cases i <;> simp_all [ofBoolListLE]
 
-@[simp] theorem getMsb_ofBoolListLE :
-    (ofBoolListLE bs).getMsb i = (decide (i < bs.length) && bs.getD (bs.length - 1 - i) false) := by
-  simp [getMsb_eq_getLsb]
+@[simp] theorem getMsbD_ofBoolListLE :
+    (ofBoolListLE bs).getMsbD i = (decide (i < bs.length) && bs.getD (bs.length - 1 - i) false) := by
+  simp [getMsbD_eq_getLsbD]
 
 /-! # Rotate Left -/
 
@@ -1505,15 +1597,15 @@ Proof by example:
 Let x := <6 5 4 3 2 1 0> : BitVec 7.
 x.rotateLeft 2 = (<6 5 | 4 3 2 1 0>).rotateLeft 2 = <3 2 1 0 | 6 5>
 
-(x.rotateLeft 2).getLsb ⟨i, i < 2⟩
-= <3 2 1 0 | 6 5>.getLsb ⟨i, i < 2⟩
+(x.rotateLeft 2).getLsbD ⟨i, i < 2⟩
+= <3 2 1 0 | 6 5>.getLsbD ⟨i, i < 2⟩
 = <6 5>[i]
 = <6 5 | 4 3 2 1 0>[i + len(<4 3 2 1 0>)]
 = <6 5 | 4 3 2 1 0>[i + 7 - 2]
 -/
-theorem getLsb_rotateLeftAux_of_le {x : BitVec w} {r : Nat} {i : Nat} (hi : i < r) :
-    (x.rotateLeftAux r).getLsb i = x.getLsb (w - r + i) := by
-  rw [rotateLeftAux, getLsb_or, getLsb_ushiftRight]
+theorem getLsbD_rotateLeftAux_of_le {x : BitVec w} {r : Nat} {i : Nat} (hi : i < r) :
+    (x.rotateLeftAux r).getLsbD i = x.getLsbD (w - r + i) := by
+  rw [rotateLeftAux, getLsbD_or, getLsbD_ushiftRight]
   simp; omega
 
 /--
@@ -1524,45 +1616,45 @@ Proof by example:
 Let x := <6 5 4 3 2 1 0> : BitVec 7.
 x.rotateLeft 2 = (<6 5 | 4 3 2 1 0>).rotateLeft 2 = <3 2 1 0 | 6 5>
 
-(x.rotateLeft 2).getLsb ⟨i, i ≥ 2⟩
-= <3 2 1 0 | 6 5>.getLsb ⟨i, i ≥ 2⟩
+(x.rotateLeft 2).getLsbD ⟨i, i ≥ 2⟩
+= <3 2 1 0 | 6 5>.getLsbD ⟨i, i ≥ 2⟩
 = <3 2 1 0>[i - 2]
 = <6 5 | 3 2 1 0>[i - 2]
 
 Intuitively, grab the full width (7), then move the marker `|` by `r` to the right `(-2)`
 Then, access the bit at `i` from the right `(+i)`.
  -/
-theorem getLsb_rotateLeftAux_of_geq {x : BitVec w} {r : Nat} {i : Nat} (hi : i ≥ r) :
-    (x.rotateLeftAux r).getLsb i = (decide (i < w) && x.getLsb (i - r)) := by
-  rw [rotateLeftAux, getLsb_or]
-  suffices (x >>> (w - r)).getLsb i = false by
+theorem getLsbD_rotateLeftAux_of_geq {x : BitVec w} {r : Nat} {i : Nat} (hi : i ≥ r) :
+    (x.rotateLeftAux r).getLsbD i = (decide (i < w) && x.getLsbD (i - r)) := by
+  rw [rotateLeftAux, getLsbD_or]
+  suffices (x >>> (w - r)).getLsbD i = false by
     have hiltr : decide (i < r) = false := by
       simp [hi]
-    simp [getLsb_shiftLeft, Bool.or_false, hi, hiltr, this]
-  simp only [getLsb_ushiftRight]
-  apply getLsb_ge
+    simp [getLsbD_shiftLeft, Bool.or_false, hi, hiltr, this]
+  simp only [getLsbD_ushiftRight]
+  apply getLsbD_ge
   omega
 
-/-- When `r < w`, we give a formula for `(x.rotateRight r).getLsb i`. -/
-theorem getLsb_rotateLeft_of_le {x : BitVec w} {r i : Nat} (hr: r < w) :
-    (x.rotateLeft r).getLsb i =
+/-- When `r < w`, we give a formula for `(x.rotateRight r).getLsbD i`. -/
+theorem getLsbD_rotateLeft_of_le {x : BitVec w} {r i : Nat} (hr: r < w) :
+    (x.rotateLeft r).getLsbD i =
       cond (i < r)
-      (x.getLsb (w - r + i))
-      (decide (i < w) && x.getLsb (i - r)) := by
+      (x.getLsbD (w - r + i))
+      (decide (i < w) && x.getLsbD (i - r)) := by
   · rw [rotateLeft_eq_rotateLeftAux_of_lt hr]
     by_cases h : i < r
-    · simp [h, getLsb_rotateLeftAux_of_le h]
-    · simp [h, getLsb_rotateLeftAux_of_geq <| Nat.ge_of_not_lt h]
+    · simp [h, getLsbD_rotateLeftAux_of_le h]
+    · simp [h, getLsbD_rotateLeftAux_of_geq <| Nat.ge_of_not_lt h]
 
 @[simp]
-theorem getLsb_rotateLeft {x : BitVec w} {r i : Nat}  :
-    (x.rotateLeft r).getLsb i =
+theorem getLsbD_rotateLeft {x : BitVec w} {r i : Nat}  :
+    (x.rotateLeft r).getLsbD i =
       cond (i < r % w)
-      (x.getLsb (w - (r % w) + i))
-      (decide (i < w) && x.getLsb (i - (r % w))) := by
+      (x.getLsbD (w - (r % w) + i))
+      (decide (i < w) && x.getLsbD (i - (r % w))) := by
   rcases w with ⟨rfl, w⟩
   · simp
-  · rw [← rotateLeft_mod_eq_rotateLeft, getLsb_rotateLeft_of_le (Nat.mod_lt _ (by omega))]
+  · rw [← rotateLeft_mod_eq_rotateLeft, getLsbD_rotateLeft_of_le (Nat.mod_lt _ (by omega))]
 
 /-! ## Rotate Right -/
 
@@ -1574,17 +1666,17 @@ Proof by example:
 Let x := <6 5 4 3 2 1 0> : BitVec 7.
 x.rotateRight 2 = (<6 5 4 3 2 | 1 0>).rotateRight 2 = <1 0 | 6 5 4 3 2>
 
-(x.rotateLeft 2).getLsb ⟨i, i ≤ 7 - 2⟩
-= <1 0 | 6 5 4 3 2>.getLsb ⟨i, i ≤ 7 - 2⟩
-= <6 5 4 3 2>.getLsb i
+(x.rotateLeft 2).getLsbD ⟨i, i ≤ 7 - 2⟩
+= <1 0 | 6 5 4 3 2>.getLsbD ⟨i, i ≤ 7 - 2⟩
+= <6 5 4 3 2>.getLsbD i
 = <6 5 4 3 2 | 1 0>[i + 2]
 -/
-theorem getLsb_rotateRightAux_of_le {x : BitVec w} {r : Nat} {i : Nat} (hi : i < w - r) :
-    (x.rotateRightAux r).getLsb i = x.getLsb (r + i) := by
-  rw [rotateRightAux, getLsb_or, getLsb_ushiftRight]
-  suffices (x <<< (w - r)).getLsb i = false by
+theorem getLsbD_rotateRightAux_of_le {x : BitVec w} {r : Nat} {i : Nat} (hi : i < w - r) :
+    (x.rotateRightAux r).getLsbD i = x.getLsbD (r + i) := by
+  rw [rotateRightAux, getLsbD_or, getLsbD_ushiftRight]
+  suffices (x <<< (w - r)).getLsbD i = false by
     simp only [this, Bool.or_false]
-  simp only [getLsb_shiftLeft, Bool.and_eq_false_imp, Bool.and_eq_true, decide_eq_true_eq,
+  simp only [getLsbD_shiftLeft, Bool.and_eq_false_imp, Bool.and_eq_true, decide_eq_true_eq,
     Bool.not_eq_true', decide_eq_false_iff_not, Nat.not_lt, and_imp]
   omega
 
@@ -1596,20 +1688,20 @@ Proof by example:
 Let x := <6 5 4 3 2 1 0> : BitVec 7.
 x.rotateRight 2 = (<6 5 4 3 2 | 1 0>).rotateRight 2 = <1 0 | 6 5 4 3 2>
 
-(x.rotateLeft 2).getLsb ⟨i, i ≥ 7 - 2⟩
-= <1 0 | 6 5 4 3 2>.getLsb ⟨i, i ≤ 7 - 2⟩
-= <1 0>.getLsb (i - len(<6 5 4 3 2>)
+(x.rotateLeft 2).getLsbD ⟨i, i ≥ 7 - 2⟩
+= <1 0 | 6 5 4 3 2>.getLsbD ⟨i, i ≤ 7 - 2⟩
+= <1 0>.getLsbD (i - len(<6 5 4 3 2>)
 = <6 5 4 3 2 | 1 0> (i - len<6 4 4 3 2>)
  -/
-theorem getLsb_rotateRightAux_of_geq {x : BitVec w} {r : Nat} {i : Nat} (hi : i ≥ w - r) :
-    (x.rotateRightAux r).getLsb i = (decide (i < w) && x.getLsb (i - (w - r))) := by
-  rw [rotateRightAux, getLsb_or]
-  suffices (x >>> r).getLsb i = false by
-    simp only [this, getLsb_shiftLeft, Bool.false_or]
+theorem getLsbD_rotateRightAux_of_geq {x : BitVec w} {r : Nat} {i : Nat} (hi : i ≥ w - r) :
+    (x.rotateRightAux r).getLsbD i = (decide (i < w) && x.getLsbD (i - (w - r))) := by
+  rw [rotateRightAux, getLsbD_or]
+  suffices (x >>> r).getLsbD i = false by
+    simp only [this, getLsbD_shiftLeft, Bool.false_or]
     by_cases hiw : i < w
     <;> simp [hiw, hi]
-  simp only [getLsb_ushiftRight]
-  apply getLsb_ge
+  simp only [getLsbD_ushiftRight]
+  apply getLsbD_ge
   omega
 
 /-- `rotateRight` equals the bit fiddling definition of `rotateRightAux` when the rotation amount is
@@ -1625,25 +1717,25 @@ theorem rotateRight_mod_eq_rotateRight {x : BitVec w} {r : Nat} :
   simp only [rotateRight, Nat.mod_mod]
 
 /-- When `r < w`, we give a formula for `(x.rotateRight r).getLsb i`. -/
-theorem getLsb_rotateRight_of_le {x : BitVec w} {r i : Nat} (hr: r < w) :
-    (x.rotateRight r).getLsb i =
+theorem getLsbD_rotateRight_of_le {x : BitVec w} {r i : Nat} (hr: r < w) :
+    (x.rotateRight r).getLsbD i =
       cond (i < w - r)
-      (x.getLsb (r + i))
-      (decide (i < w) && x.getLsb (i - (w - r))) := by
+      (x.getLsbD (r + i))
+      (decide (i < w) && x.getLsbD (i - (w - r))) := by
   · rw [rotateRight_eq_rotateRightAux_of_lt hr]
     by_cases h : i < w - r
-    · simp [h, getLsb_rotateRightAux_of_le h]
-    · simp [h, getLsb_rotateRightAux_of_geq <| Nat.le_of_not_lt h]
+    · simp [h, getLsbD_rotateRightAux_of_le h]
+    · simp [h, getLsbD_rotateRightAux_of_geq <| Nat.le_of_not_lt h]
 
 @[simp]
-theorem getLsb_rotateRight {x : BitVec w} {r i : Nat} :
-    (x.rotateRight r).getLsb i =
+theorem getLsbD_rotateRight {x : BitVec w} {r i : Nat} :
+    (x.rotateRight r).getLsbD i =
       cond (i < w - (r % w))
-      (x.getLsb ((r % w) + i))
-      (decide (i < w) && x.getLsb (i - (w - (r % w)))) := by
+      (x.getLsbD ((r % w) + i))
+      (decide (i < w) && x.getLsbD (i - (w - (r % w)))) := by
   rcases w with ⟨rfl, w⟩
   · simp
-  · rw [← rotateRight_mod_eq_rotateRight, getLsb_rotateRight_of_le (Nat.mod_lt _ (by omega))]
+  · rw [← rotateRight_mod_eq_rotateRight, getLsbD_rotateRight_of_le (Nat.mod_lt _ (by omega))]
 
 /- ## twoPow -/
 
@@ -1656,10 +1748,10 @@ theorem toNat_twoPow (w : Nat) (i : Nat) : (twoPow w i).toNat = 2^i % 2^w := by
     rw [Nat.mod_eq_of_lt h1, Nat.shiftLeft_eq, Nat.one_mul]
 
 @[simp]
-theorem getLsb_twoPow (i j : Nat) : (twoPow w i).getLsb j = ((i < w) && (i = j)) := by
+theorem getLsbD_twoPow (i j : Nat) : (twoPow w i).getLsbD j = ((i < w) && (i = j)) := by
   rcases w with rfl | w
   · simp
-  · simp only [twoPow, getLsb_shiftLeft, getLsb_ofNat]
+  · simp only [twoPow, getLsbD_shiftLeft, getLsbD_ofNat]
     by_cases hj : j < i
     · simp only [hj, decide_True, Bool.not_true, Bool.and_false, Bool.false_and, Bool.false_eq,
       Bool.and_eq_false_imp, decide_eq_true_eq, decide_eq_false_iff_not]
@@ -1675,14 +1767,14 @@ theorem getLsb_twoPow (i j : Nat) : (twoPow w i).getLsb j = ((i < w) && (i = j))
 
 @[simp]
 theorem and_twoPow (x : BitVec w) (i : Nat) :
-    x &&& (twoPow w i) = if x.getLsb i then twoPow w i else 0#w := by
+    x &&& (twoPow w i) = if x.getLsbD i then twoPow w i else 0#w := by
   ext j
-  simp only [getLsb_and, getLsb_twoPow]
-  by_cases hj : i = j <;> by_cases hx : x.getLsb i <;> simp_all
+  simp only [getLsbD_and, getLsbD_twoPow]
+  by_cases hj : i = j <;> by_cases hx : x.getLsbD i <;> simp_all
 
 @[simp]
 theorem twoPow_and (x : BitVec w) (i : Nat) :
-    (twoPow w i) &&& x = if x.getLsb i then twoPow w i else 0#w := by
+    (twoPow w i) &&& x = if x.getLsbD i then twoPow w i else 0#w := by
   rw [BitVec.and_comm, and_twoPow]
 
 @[simp]
@@ -1703,8 +1795,8 @@ theorem twoPow_zero {w : Nat} : twoPow w 0 = 1#w := by
   simp
 
 @[simp]
-theorem getLsb_one {w i : Nat} : (1#w).getLsb i = (decide (0 < w) && decide (0 = i)) := by
-  rw [← twoPow_zero, getLsb_twoPow]
+theorem getLsbD_one {w i : Nat} : (1#w).getLsbD i = (decide (0 < w) && decide (0 = i)) := by
+  rw [← twoPow_zero, getLsbD_twoPow]
 
 /- ### zeroExtend, truncate, and bitwise operations -/
 
@@ -1712,12 +1804,12 @@ theorem getLsb_one {w i : Nat} : (1#w).getLsb i = (decide (0 < w) && decide (0 =
 When the `(i+1)`th bit of `x` is false,
 keeping the lower `(i + 1)` bits of `x` equals keeping the lower `i` bits.
 -/
-theorem zeroExtend_truncate_succ_eq_zeroExtend_truncate_of_getLsb_false
-  {x : BitVec w} {i : Nat} (hx : x.getLsb i = false) :
+theorem zeroExtend_truncate_succ_eq_zeroExtend_truncate_of_getLsbD_false
+  {x : BitVec w} {i : Nat} (hx : x.getLsbD i = false) :
     zeroExtend w (x.truncate (i + 1)) =
       zeroExtend w (x.truncate i) := by
   ext k
-  simp only [getLsb_zeroExtend, Fin.is_lt, decide_True, Bool.true_and, getLsb_or, getLsb_and]
+  simp only [getLsbD_zeroExtend, Fin.is_lt, decide_True, Bool.true_and, getLsbD_or, getLsbD_and]
   by_cases hik : i = k
   · subst hik
     simp [hx]
@@ -1728,22 +1820,22 @@ When the `(i+1)`th bit of `x` is true,
 keeping the lower `(i + 1)` bits of `x` equalsk eeping the lower `i` bits
 and then performing bitwise-or with `twoPow i = (1 << i)`,
 -/
-theorem zeroExtend_truncate_succ_eq_zeroExtend_truncate_or_twoPow_of_getLsb_true
-    {x : BitVec w} {i : Nat} (hx : x.getLsb i = true) :
+theorem zeroExtend_truncate_succ_eq_zeroExtend_truncate_or_twoPow_of_getLsbD_true
+    {x : BitVec w} {i : Nat} (hx : x.getLsbD i = true) :
     zeroExtend w (x.truncate (i + 1)) =
       zeroExtend w (x.truncate i) ||| (twoPow w i) := by
   ext k
-  simp only [getLsb_zeroExtend, Fin.is_lt, decide_True, Bool.true_and, getLsb_or, getLsb_and]
+  simp only [getLsbD_zeroExtend, Fin.is_lt, decide_True, Bool.true_and, getLsbD_or, getLsbD_and]
   by_cases hik : i = k
   · subst hik
     simp [hx]
   · by_cases hik' : k < i + 1 <;> simp [hik, hik'] <;> omega
 
 /-- Bitwise and of `(x : BitVec w)` with `1#w` equals zero extending `x.lsb` to `w`. -/
-theorem and_one_eq_zeroExtend_ofBool_getLsb {x : BitVec w} :
-    (x &&& 1#w) = zeroExtend w (ofBool (x.getLsb 0)) := by
+theorem and_one_eq_zeroExtend_ofBool_getLsbD {x : BitVec w} :
+    (x &&& 1#w) = zeroExtend w (ofBool (x.getLsbD 0)) := by
   ext i
-  simp only [getLsb_and, getLsb_one, getLsb_zeroExtend, Fin.is_lt, decide_True, getLsb_ofBool,
+  simp only [getLsbD_and, getLsbD_one, getLsbD_zeroExtend, Fin.is_lt, decide_True, getLsbD_ofBool,
     Bool.true_and]
   by_cases h : (0 = (i : Nat)) <;> simp [h] <;> omega
 
@@ -1772,13 +1864,13 @@ private theorem Nat.sub_mul_eq_mod_of_lt_of_le (hlo : w * n ≤ i) (hhi : i < w
     (by rw [Nat.mul_comm]; omega)
 
 @[simp]
-theorem getLsb_replicate {n w : Nat} (x : BitVec w) :
-    (x.replicate n).getLsb i =
-    (decide (i < w * n) && x.getLsb (i % w)) := by
+theorem getLsbD_replicate {n w : Nat} (x : BitVec w) :
+    (x.replicate n).getLsbD i =
+    (decide (i < w * n) && x.getLsbD (i % w)) := by
   induction n generalizing x
   case zero => simp
   case succ n ih =>
-    simp only [replicate_succ_eq, getLsb_cast, getLsb_append]
+    simp only [replicate_succ_eq, getLsbD_cast, getLsbD_append]
     by_cases hi : i < w * (n + 1)
     · simp only [hi, decide_True, Bool.true_and]
       by_cases hi' : i < w * n
@@ -1787,15 +1879,15 @@ theorem getLsb_replicate {n w : Nat} (x : BitVec w) :
         rw [Nat.sub_mul_eq_mod_of_lt_of_le] <;> omega
     · rw [Nat.mul_succ] at hi ⊢
       simp only [show ¬i < w * n by omega, decide_False, cond_false, hi, Bool.false_and]
-      apply BitVec.getLsb_ge (x := x) (i := i - w * n) (ge := by omega)
+      apply BitVec.getLsbD_ge (x := x) (i := i - w * n) (ge := by omega)
 
 /-! ### intMin -/
 
 /-- The bitvector of width `w` that has the smallest value when interpreted as an integer. -/
 abbrev intMin (w : Nat) := twoPow w (w - 1)
 
-theorem getLsb_intMin (w : Nat) : (intMin w).getLsb i = decide (i + 1 = w) := by
-  simp only [getLsb_twoPow, boolToPropSimps]
+theorem getLsbD_intMin (w : Nat) : (intMin w).getLsbD i = decide (i + 1 = w) := by
+  simp only [getLsbD_twoPow, boolToPropSimps]
   omega
 
 @[simp, bv_toNat]
@@ -1829,7 +1921,7 @@ theorem toNat_intMax : (intMax w).toNat = 2 ^ (w - 1) - 1 := by
     omega
 
 @[simp]
-theorem getLsb_intMax (w : Nat) : (intMax w).getLsb i = decide (i + 1 < w) := by
+theorem getLsbD_intMax (w : Nat) : (intMax w).getLsbD i = decide (i + 1 < w) := by
   rw [← testBit_toNat, toNat_intMax, Nat.testBit_two_pow_sub_one, decide_eq_decide]
   omega
 
diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean
index 663a6f6220..c25223dee0 100644
--- a/src/Init/Data/List/Lemmas.lean
+++ b/src/Init/Data/List/Lemmas.lean
@@ -255,7 +255,7 @@ theorem get!_len_le [Inhabited α] : ∀ {l : List α} {n}, length l ≤ n → l
 /-! ### getElem? and getElem -/
 
 @[simp] theorem getElem?_eq_getElem {l : List α} {n} (h : n < l.length) : l[n]? = some l[n] := by
-  simp only [← get?_eq_getElem?, get?_eq_get, h, get_eq_getElem]
+  simp only [getElem?_def, h, ↓reduceDIte]
 
 theorem getElem?_eq_some {l : List α} : l[n]? = some a ↔ ∃ h : n < l.length, l[n] = a := by
   simp only [← get?_eq_getElem?, get?_eq_some, get_eq_getElem]
diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean
index b68e85d57e..969171950e 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean
@@ -88,8 +88,8 @@ where
   go : BVPred → Expr
   | .bin (w := w) lhs op rhs =>
     mkApp4 (mkConst ``BVPred.bin) (toExpr w) (toExpr lhs) (toExpr op) (toExpr rhs)
-  | .getLsb (w := w) expr idx =>
-    mkApp3 (mkConst ``BVPred.getLsb) (toExpr w) (toExpr expr) (toExpr idx)
+  | .getLsbD (w := w) expr idx =>
+    mkApp3 (mkConst ``BVPred.getLsbD) (toExpr w) (toExpr expr) (toExpr idx)
 
 
 instance [ToExpr α] : ToExpr (BoolExpr α) where
diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVPred.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVPred.lean
index 94973b1314..c7dc36239f 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVPred.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVPred.lean
@@ -46,16 +46,16 @@ def of (t : Expr) : M (Option ReifiedBVPred) := do
     binaryReflection lhsExpr rhsExpr .eq ``Std.Tactic.BVDecide.Reflect.BitVec.beq_congr
   | BitVec.ult _ lhsExpr rhsExpr =>
     binaryReflection lhsExpr rhsExpr .ult ``Std.Tactic.BVDecide.Reflect.BitVec.ult_congr
-  | BitVec.getLsb _ subExpr idxExpr =>
+  | BitVec.getLsbD _ subExpr idxExpr =>
     let some sub ← ReifiedBVExpr.of subExpr | return none
     let some idx ← getNatValue? idxExpr | return none
-    let bvExpr : BVPred := .getLsb sub.bvExpr idx
-    let expr := mkApp3 (mkConst ``BVPred.getLsb) (toExpr sub.width) sub.expr idxExpr
+    let bvExpr : BVPred := .getLsbD sub.bvExpr idx
+    let expr := mkApp3 (mkConst ``BVPred.getLsbD) (toExpr sub.width) sub.expr idxExpr
     let proof := do
       let subEval ← ReifiedBVExpr.mkEvalExpr sub.width sub.expr
       let subProof ← sub.evalsAtAtoms
       return mkApp5
-        (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.getLsb_congr)
+        (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.getLsbD_congr)
         idxExpr
         (toExpr sub.width)
         subExpr
@@ -73,8 +73,8 @@ def of (t : Expr) : M (Option ReifiedBVPred) := do
     let ty ← inferType t
     let_expr Bool := ty | return none
     let atom ← ReifiedBVExpr.mkAtom (mkApp (mkConst ``BitVec.ofBool) t) 1
-    let bvExpr : BVPred := .getLsb atom.bvExpr 0
-    let expr := mkApp3 (mkConst ``BVPred.getLsb) (toExpr 1) atom.expr (toExpr 0)
+    let bvExpr : BVPred := .getLsbD atom.bvExpr 0
+    let expr := mkApp3 (mkConst ``BVPred.getLsbD) (toExpr 1) atom.expr (toExpr 0)
     let proof := do
       let atomEval ← ReifiedBVExpr.mkEvalExpr atom.width atom.expr
       let atomProof ← atom.evalsAtAtoms
diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean
index 5c78ba1b4e..0156328611 100644
--- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean
+++ b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean
@@ -154,9 +154,9 @@ builtin_dsimproc [simp, seval] reduceSDiv ((sdiv _ _ : BitVec _)) := reduceBin `
 /-- Simplification procedure for signed division of `BitVec`s using the SMT-Lib conventions. -/
 builtin_dsimproc [simp, seval] reduceSMTSDiv ((smtSDiv _ _ : BitVec _)) := reduceBin ``smtSDiv 3 smtSDiv
 /-- Simplification procedure for `getLsb` (lowest significant bit) on `BitVec`. -/
-builtin_dsimproc [simp, seval] reduceGetLsb (getLsb _ _) := reduceGetBit ``getLsb getLsb
+builtin_dsimproc [simp, seval] reduceGetLsb (getLsbD _ _) := reduceGetBit ``getLsbD getLsbD
 /-- Simplification procedure for `getMsb` (most significant bit) on `BitVec`. -/
-builtin_dsimproc [simp, seval] reduceGetMsb (getMsb _ _) := reduceGetBit ``getMsb getMsb
+builtin_dsimproc [simp, seval] reduceGetMsb (getMsbD _ _) := reduceGetBit ``getMsbD getMsbD
 
 /-- Simplification procedure for shift left on `BitVec`. -/
 builtin_dsimproc [simp, seval] reduceShiftLeft (BitVec.shiftLeft _ _) :=
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean
index ac74fc77f0..1c685f2c8d 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean
@@ -375,7 +375,7 @@ inductive BVPred where
   /--
   Getting a constant LSB from a `BitVec`.
   -/
-  | getLsb (expr : BVExpr w) (idx : Nat)
+  | getLsbD (expr : BVExpr w) (idx : Nat)
 
 namespace BVPred
 
@@ -389,7 +389,7 @@ structure ExprPair where
 
 def toString : BVPred → String
   | bin lhs op rhs => s!"({lhs.toString} {op.toString} {rhs.toString})"
-  | getLsb expr idx => s!"{expr.toString}[{idx}]"
+  | getLsbD expr idx => s!"{expr.toString}[{idx}]"
 
 instance : ToString BVPred := ⟨toString⟩
 
@@ -398,14 +398,14 @@ The semantics for `BVPred`.
 -/
 def eval (assign : BVExpr.Assignment) : BVPred → Bool
   | bin lhs op rhs => op.eval (lhs.eval assign) (rhs.eval assign)
-  | getLsb expr idx => (expr.eval assign).getLsb idx
+  | getLsbD expr idx => (expr.eval assign).getLsbD idx
 
 @[simp]
 theorem eval_bin : eval assign (.bin lhs op rhs) = op.eval (lhs.eval assign) (rhs.eval assign) := by
   rfl
 
 @[simp]
-theorem eval_getLsb : eval assign (.getLsb expr idx) = (expr.eval assign).getLsb idx := by
+theorem eval_getLsbD : eval assign (.getLsbD expr idx) = (expr.eval assign).getLsbD idx := by
   rfl
 
 end BVPred
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Const.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Const.lean
index 82202c4b3c..99b6f02beb 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Const.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Const.lean
@@ -27,7 +27,7 @@ where
   go (aig : AIG α) (val : BitVec w) (curr : Nat) (s : AIG.RefVec aig curr) (hcurr : curr ≤ w) :
       AIG.RefVecEntry α w :=
     if hcurr : curr < w then
-      let res := aig.mkConstCached (val.getLsb curr)
+      let res := aig.mkConstCached (val.getLsbD curr)
       let aig := res.aig
       let bitRef := res.ref
       let s := s.cast <| AIG.LawfulOperator.le_size (f := AIG.mkConstCached) ..
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations.lean
index de0ce36de7..6936abc556 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations.lean
@@ -8,7 +8,7 @@ import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Add
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Append
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Eq
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Extract
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.GetLsb
+import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.GetLsbD
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Mul
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Not
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Replicate
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/GetLsb.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/GetLsbD.lean
similarity index 76%
rename from src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/GetLsb.lean
rename to src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/GetLsbD.lean
index 234aedef5c..6aa350278d 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/GetLsb.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/GetLsbD.lean
@@ -8,7 +8,7 @@ import Std.Sat.AIG.CachedGatesLemmas
 import Std.Sat.AIG.RefVec
 
 /-!
-This module contains the implementation of a bitblaster for `BitVec.getLsb`.
+This module contains the implementation of a bitblaster for `BitVec.getLsbD`.
 -/
 
 namespace Std.Tactic.BVDecide
@@ -19,27 +19,27 @@ namespace BVPred
 
 variable [Hashable α] [DecidableEq α]
 
-structure GetLsbTarget (aig : AIG α) where
+structure GetLsbDTarget (aig : AIG α) where
   {w : Nat}
   vec : AIG.RefVec aig w
   idx : Nat
 
-def blastGetLsb (aig : AIG α) (target : GetLsbTarget aig) : AIG.Entrypoint α :=
+def blastGetLsbD (aig : AIG α) (target : GetLsbDTarget aig) : AIG.Entrypoint α :=
   if h : target.idx < target.w then
     ⟨aig, target.vec.get target.idx h⟩
   else
     AIG.mkConstCached aig false
 
-instance : AIG.LawfulOperator α GetLsbTarget blastGetLsb where
+instance : AIG.LawfulOperator α GetLsbDTarget blastGetLsbD where
   le_size := by
     intros
-    unfold blastGetLsb
+    unfold blastGetLsbD
     split
     · simp
     · apply AIG.LawfulOperator.le_size (f := AIG.mkConstCached)
   decl_eq := by
     intros
-    unfold blastGetLsb
+    unfold blastGetLsbD
     split
     · simp
     · rw [AIG.LawfulOperator.decl_eq (f := AIG.mkConstCached)]
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Pred.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Pred.lean
index 4d2aeb7257..d3e2728f76 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Pred.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Pred.lean
@@ -6,7 +6,7 @@ Authors: Henrik Böving
 prelude
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Eq
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Ult
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.GetLsb
+import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.GetLsbD
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
 
 /-!
@@ -33,7 +33,7 @@ def bitblast (aig : AIG BVBit) (pred : BVPred) : AIG.Entrypoint BVBit :=
     match op with
     | .eq => mkEq aig ⟨lhsRefs, rhsRefs⟩
     | .ult => mkUlt aig ⟨lhsRefs, rhsRefs⟩
-  | .getLsb expr idx =>
+  | .getLsbD expr idx =>
     /-
     Note: This blasts the entire expression up to `w` despite only needing it up to `idx`.
     However the vast majority of operations are interested in all bits so the API is currently
@@ -42,7 +42,7 @@ def bitblast (aig : AIG BVBit) (pred : BVPred) : AIG.Entrypoint BVBit :=
     let res := expr.bitblast aig
     let aig := res.aig
     let refs := res.vec
-    blastGetLsb aig ⟨refs, idx⟩
+    blastGetLsbD aig ⟨refs, idx⟩
 
 instance : AIG.LawfulOperator BVBit (fun _ => BVPred) bitblast where
   le_size := by
@@ -59,8 +59,8 @@ instance : AIG.LawfulOperator BVBit (fun _ => BVPred) bitblast where
         apply AIG.LawfulOperator.le_size_of_le_aig_size (f := mkUlt)
         apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := BVExpr.bitblast)
         apply AIG.LawfulVecOperator.le_size (f := BVExpr.bitblast)
-    | getLsb expr idx =>
-      apply AIG.LawfulOperator.le_size_of_le_aig_size (f := blastGetLsb)
+    | getLsbD expr idx =>
+      apply AIG.LawfulOperator.le_size_of_le_aig_size (f := blastGetLsbD)
       apply AIG.LawfulVecOperator.le_size (f := BVExpr.bitblast)
   decl_eq := by
     intro aig pred idx h1 h2
@@ -87,9 +87,9 @@ instance : AIG.LawfulOperator BVBit (fun _ => BVPred) bitblast where
         · apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := BVExpr.bitblast)
           apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := BVExpr.bitblast)
           assumption
-    | getLsb expr idx =>
+    | getLsbD expr idx =>
       simp only [bitblast]
-      rw [AIG.LawfulOperator.decl_eq (f := blastGetLsb)]
+      rw [AIG.LawfulOperator.decl_eq (f := blastGetLsbD)]
       rw [AIG.LawfulVecOperator.decl_eq (f := BVExpr.bitblast)]
       apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := BVExpr.bitblast)
       assumption
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Basic.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Basic.lean
index 67ded0cb20..b57266bfc5 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Basic.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Basic.lean
@@ -18,11 +18,11 @@ namespace Std.Tactic.BVDecide
 namespace BVExpr
 
 def Assignment.toAIGAssignment (assign : Assignment) : BVBit → Bool :=
-  fun bit => (assign.getD bit.var).bv.getLsb bit.idx
+  fun bit => (assign.getD bit.var).bv.getLsbD bit.idx
 
 @[simp]
 theorem Assignment.toAIGAssignment_apply (assign : Assignment) (bit : BVBit) :
-    assign.toAIGAssignment bit = (assign.getD bit.var).bv.getLsb bit.idx := by
+    assign.toAIGAssignment bit = (assign.getD bit.var).bv.getLsbD bit.idx := by
   rfl
 
 end BVExpr
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Carry.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Carry.lean
index 2cf0ef23aa..50678be49d 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Carry.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Carry.lean
@@ -26,8 +26,8 @@ namespace mkOverflowBit
 
 theorem go_eq_carry (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (cin : Ref aig) (origCin : Ref aig)
     (lhs rhs : RefVec aig w) (lhsExpr rhsExpr : BitVec w) (assign : α → Bool)
-    (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, lhs.get idx hidx, assign⟧ = lhsExpr.getLsb idx)
-    (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, rhs.get idx hidx, assign⟧ = rhsExpr.getLsb idx)
+    (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, lhs.get idx hidx, assign⟧ = lhsExpr.getLsbD idx)
+    (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, rhs.get idx hidx, assign⟧ = rhsExpr.getLsbD idx)
     (hcin : ⟦aig, cin, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦aig, origCin, assign⟧) :
     ⟦go aig lhs rhs curr hcurr cin, assign⟧
       =
@@ -59,8 +59,8 @@ end mkOverflowBit
 
 theorem mkOverflowBit_eq_carry (aig : AIG α) (input : OverflowInput aig) (lhs rhs : BitVec input.w)
     (assign : α → Bool)
-    (hleft : ∀ (idx : Nat) (hidx : idx < input.w), ⟦aig, input.vec.lhs.get idx hidx, assign⟧ = lhs.getLsb idx)
-    (hright : ∀ (idx : Nat) (hidx : idx < input.w), ⟦aig, input.vec.rhs.get idx hidx, assign⟧ = rhs.getLsb idx) :
+    (hleft : ∀ (idx : Nat) (hidx : idx < input.w), ⟦aig, input.vec.lhs.get idx hidx, assign⟧ = lhs.getLsbD idx)
+    (hright : ∀ (idx : Nat) (hidx : idx < input.w), ⟦aig, input.vec.rhs.get idx hidx, assign⟧ = rhs.getLsbD idx) :
     ⟦mkOverflowBit aig input, assign⟧
       =
     BitVec.carry input.w lhs rhs ⟦aig, input.cin, assign⟧ := by
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Const.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Const.lean
index 6f2a641bd3..bbff7b66ad 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Const.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Const.lean
@@ -87,7 +87,7 @@ theorem go_denote_eq (aig : AIG α) (c : BitVec w) (assign : α → Bool)
           assign
         ⟧
           =
-        c.getLsb idx := by
+        c.getLsbD idx := by
   intro idx hidx1 hidx2
   generalize hgo : go aig c curr s hcurr = res
   unfold go at hgo
@@ -117,7 +117,7 @@ theorem denote_blastConst (aig : AIG α) (c : BitVec w) (assign : α → Bool) :
     ∀ (idx : Nat) (hidx : idx < w),
         ⟦(blastConst aig c).aig, (blastConst aig c).vec.get idx hidx, assign⟧
           =
-        c.getLsb idx := by
+        c.getLsbD idx := by
   intros
   apply blastConst.go_denote_eq
   omega
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean
index 461f789191..caf90a4e5e 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean
@@ -58,7 +58,7 @@ theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) :
     ∀ (idx : Nat) (hidx : idx < w),
         ⟦(go aig expr).val.aig, (go aig expr).val.vec.get idx hidx, assign.toAIGAssignment⟧
           =
-        (expr.eval assign).getLsb idx := by
+        (expr.eval assign).getLsbD idx := by
   intro idx hidx
   induction expr generalizing aig idx with
   | const =>
@@ -67,13 +67,13 @@ theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) :
     simp [go, hidx, denote_blastVar]
   | zeroExtend v inner ih =>
     simp only [go, denote_blastZeroExtend, ih, dite_eq_ite, Bool.if_false_right,
-      eval_zeroExtend, BitVec.getLsb_zeroExtend, hidx, decide_True, Bool.true_and,
+      eval_zeroExtend, BitVec.getLsbD_zeroExtend, hidx, decide_True, Bool.true_and,
       Bool.and_iff_right_iff_imp, decide_eq_true_eq]
-    apply BitVec.lt_of_getLsb
+    apply BitVec.lt_of_getLsbD
   | append lhs rhs lih rih =>
     rename_i lw rw
     simp only [go, denote_blastAppend, RefVec.get_cast, Ref.cast_eq, eval_append,
-      BitVec.getLsb_append]
+      BitVec.getLsbD_append]
     split
     · next hsplit =>
       simp only [hsplit, decide_True, cond_true]
@@ -95,9 +95,9 @@ theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) :
         simp only [eval_signExtend]
         rw [BitVec.signExtend_eq_not_zeroExtend_not_of_msb_false]
         · simp only [denote_blastZeroExtend, ih, dite_eq_ite, Bool.if_false_right,
-            BitVec.getLsb_zeroExtend, hidx, decide_True, Bool.true_and, Bool.and_iff_right_iff_imp,
+            BitVec.getLsbD_zeroExtend, hidx, decide_True, Bool.true_and, Bool.and_iff_right_iff_imp,
             decide_eq_true_eq]
-          apply BitVec.lt_of_getLsb
+          apply BitVec.lt_of_getLsbD
         · subst heq
           rw [BitVec.msb_zero_length]
       · simp [heq]
@@ -105,23 +105,23 @@ theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) :
       rw [← hgo]
       rw [denote_blastSignExtend]
       simp only [eval_signExtend]
-      rw [BitVec.getLsb_signExtend]
+      rw [BitVec.getLsbD_signExtend]
       · simp only [hidx, decide_True, Bool.true_and]
         split
         · rw [ih]
-        · rw [BitVec.msb_eq_getLsb_last]
+        · rw [BitVec.msb_eq_getLsbD_last]
           rw [ih]
       · dsimp only; omega
   | extract hi lo inner ih =>
     simp only [go, denote_blastExtract, Bool.if_false_right, eval_extract,
-      BitVec.getLsb_extract]
+      BitVec.getLsbD_extract]
     have : idx ≤ hi - lo := by omega
     simp only [this, decide_True, Bool.true_and]
     split
     · next hsplit =>
       rw [ih]
     · apply Eq.symm
-      apply BitVec.getLsb_ge
+      apply BitVec.getLsbD_ge
       omega
   | shiftLeft lhs rhs lih rih =>
     simp only [go, eval_shiftLeft]
@@ -151,21 +151,21 @@ theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) :
     cases op with
     | and =>
       simp only [go, RefVec.denote_zip, denote_mkAndCached, rih, eval_bin, BVBinOp.eval_and,
-        BitVec.getLsb_and]
+        BitVec.getLsbD_and]
       simp only [go_val_eq_bitblast, RefVec.get_cast]
       rw [AIG.LawfulVecOperator.denote_input_vec (f := bitblast)]
       rw [← go_val_eq_bitblast]
       rw [lih]
     | or =>
       simp only [go, RefVec.denote_zip, denote_mkOrCached, rih, eval_bin, BVBinOp.eval_or,
-        BitVec.getLsb_or]
+        BitVec.getLsbD_or]
       simp only [go_val_eq_bitblast, RefVec.get_cast]
       rw [AIG.LawfulVecOperator.denote_input_vec (f := bitblast)]
       rw [← go_val_eq_bitblast]
       rw [lih]
     | xor =>
       simp only [go, RefVec.denote_zip, denote_mkXorCached, rih, eval_bin, BVBinOp.eval_xor,
-        BitVec.getLsb_xor]
+        BitVec.getLsbD_xor]
       simp only [go_val_eq_bitblast, RefVec.get_cast]
       rw [AIG.LawfulVecOperator.denote_input_vec (f := bitblast)]
       rw [← go_val_eq_bitblast]
@@ -200,17 +200,17 @@ theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) :
     | shiftLeftConst => simp [go, ih, hidx]
     | shiftRightConst =>
       simp only [go, denote_blastShiftRightConst, ih, dite_eq_ite, Bool.if_false_right, eval_un,
-        BVUnOp.eval_shiftRightConst, BitVec.getLsb_ushiftRight, Bool.and_iff_right_iff_imp,
+        BVUnOp.eval_shiftRightConst, BitVec.getLsbD_ushiftRight, Bool.and_iff_right_iff_imp,
         decide_eq_true_eq]
       intro h
-      apply BitVec.lt_of_getLsb
+      apply BitVec.lt_of_getLsbD
       assumption
     | rotateLeft => simp [go, ih, hidx]
     | rotateRight => simp [go, ih, hidx]
     | arithShiftRightConst n =>
       rename_i w
       have : ¬(w ≤ idx) := by omega
-      simp [go, ih, this, BitVec.getLsb_sshiftRight, BitVec.msb_eq_getLsb_last ]
+      simp [go, ih, this, BitVec.getLsbD_sshiftRight, BitVec.msb_eq_getLsbD_last ]
 
 end bitblast
 
@@ -219,7 +219,7 @@ theorem denote_bitblast (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment
     ∀ (idx : Nat) (hidx : idx < w),
         ⟦(bitblast aig expr).aig, (bitblast aig expr).vec.get idx hidx, assign.toAIGAssignment⟧
           =
-        (expr.eval assign).getLsb idx
+        (expr.eval assign).getLsbD idx
     := by
   intros
   rw [← bitblast.go_val_eq_bitblast]
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations.lean
index e265dc003e..093724fdda 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations.lean
@@ -8,7 +8,7 @@ import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Add
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Append
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Eq
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Extract
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.GetLsb
+import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.GetLsbD
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Mul
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Not
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Replicate
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.lean
index 880e4e3342..db4ac80c6d 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.lean
@@ -144,8 +144,8 @@ theorem atLeastTwo_eq_halfAdder (lhsBit rhsBit carry : Bool) :
 theorem go_denote_eq (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (cin : Ref aig)
     (s : AIG.RefVec aig curr) (lhs rhs : AIG.RefVec aig w) (assign : α → Bool)
     (lhsExpr rhsExpr : BitVec w)
-    (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, lhs.get idx hidx, assign⟧ = lhsExpr.getLsb idx)
-    (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, rhs.get idx hidx, assign⟧ = rhsExpr.getLsb idx)
+    (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, lhs.get idx hidx, assign⟧ = lhsExpr.getLsbD idx)
+    (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, rhs.get idx hidx, assign⟧ = rhsExpr.getLsbD idx)
     (hcin : ⟦aig, cin, assign⟧ = BitVec.carry curr lhsExpr rhsExpr false) :
     ∀ (idx : Nat) (hidx1 : idx < w),
         curr ≤ idx
@@ -211,14 +211,14 @@ end blastAdd
 
 theorem denote_blastAdd (aig : AIG α) (lhs rhs : BitVec w) (assign : α → Bool)
       (input : BinaryRefVec aig w)
-      (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.lhs.get idx hidx, assign⟧ = lhs.getLsb idx)
-      (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.rhs.get idx hidx, assign⟧ = rhs.getLsb idx) :
+      (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.lhs.get idx hidx, assign⟧ = lhs.getLsbD idx)
+      (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.rhs.get idx hidx, assign⟧ = rhs.getLsbD idx) :
       ∀ (idx : Nat) (hidx : idx < w),
           ⟦(blastAdd aig input).aig, (blastAdd aig input).vec.get idx hidx, assign⟧
             =
-          (lhs + rhs).getLsb idx := by
+          (lhs + rhs).getLsbD idx := by
   intro idx hidx
-  rw [BitVec.getLsb_add]
+  rw [BitVec.getLsbD_add]
   · rw [← hleft idx hidx]
     rw [← hright idx hidx]
     unfold blastAdd
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Eq.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Eq.lean
index 7c8674cbbe..d8ef872677 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Eq.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Eq.lean
@@ -22,8 +22,8 @@ variable [Hashable α] [DecidableEq α]
 
 theorem mkEq_denote_eq (aig : AIG α) (pair : AIG.BinaryRefVec aig w) (assign : α → Bool)
     (lhs rhs : BitVec w)
-    (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, pair.lhs.get idx hidx, assign⟧ = lhs.getLsb idx)
-    (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, pair.rhs.get idx hidx, assign⟧ = rhs.getLsb idx) :
+    (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, pair.lhs.get idx hidx, assign⟧ = lhs.getLsbD idx)
+    (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, pair.rhs.get idx hidx, assign⟧ = rhs.getLsbD idx) :
     ⟦mkEq aig pair, assign⟧ = (lhs == rhs) := by
   unfold mkEq
   rw [Bool.eq_iff_iff]
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/GetLsb.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/GetLsbD.lean
similarity index 84%
rename from src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/GetLsb.lean
rename to src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/GetLsbD.lean
index f24b73d166..78a8e92ede 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/GetLsb.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/GetLsbD.lean
@@ -5,7 +5,7 @@ Authors: Henrik Böving
 -/
 prelude
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Basic
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.GetLsb
+import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.GetLsbD
 
 /-!
 This module contains the verification of the `BitVec.getLsb` bitblaster from `Impl.Operations.Extract`.
@@ -21,16 +21,16 @@ namespace BVPred
 variable [Hashable α] [DecidableEq α]
 
 @[simp]
-theorem denote_blastGetLsb (aig : AIG α) (target : GetLsbTarget aig)
+theorem denote_blastGetLsbD (aig : AIG α) (target : GetLsbDTarget aig)
     (assign : α → Bool) :
-    ⟦blastGetLsb aig target, assign⟧
+    ⟦blastGetLsbD aig target, assign⟧
       =
     if h : target.idx < target.w then
       ⟦aig, target.vec.get target.idx h, assign⟧
     else
       false := by
   rcases target with ⟨expr, idx⟩
-  unfold blastGetLsb
+  unfold blastGetLsbD
   dsimp only
   split <;> simp
 
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Mul.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Mul.lean
index 5e6c9c0cdd..b109e448c5 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Mul.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Mul.lean
@@ -27,12 +27,12 @@ namespace blastMul
 
 theorem go_denote_eq {w : Nat} (aig : AIG BVBit) (curr : Nat) (hcurr : curr + 1 ≤ w)
     (acc : AIG.RefVec aig w) (lhs rhs : AIG.RefVec aig w) (lexpr rexpr : BitVec w) (assign : Assignment)
-    (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, lhs.get idx hidx, assign.toAIGAssignment⟧ = lexpr.getLsb idx)
-    (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, rhs.get idx hidx, assign.toAIGAssignment⟧ = rexpr.getLsb idx)
+    (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, lhs.get idx hidx, assign.toAIGAssignment⟧ = lexpr.getLsbD idx)
+    (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, rhs.get idx hidx, assign.toAIGAssignment⟧ = rexpr.getLsbD idx)
     (hacc : ∀ (idx : Nat) (hidx : idx < w),
                 ⟦aig, acc.get idx hidx, assign.toAIGAssignment⟧
                   =
-                (BitVec.mulRec lexpr rexpr curr).getLsb idx) :
+                (BitVec.mulRec lexpr rexpr curr).getLsbD idx) :
     ∀ (idx : Nat) (hidx : idx < w),
         ⟦
           (go aig lhs rhs (curr + 1) hcurr acc).aig,
@@ -40,7 +40,7 @@ theorem go_denote_eq {w : Nat} (aig : AIG BVBit) (curr : Nat) (hcurr : curr + 1
           assign.toAIGAssignment
         ⟧
           =
-        (BitVec.mulRec lexpr rexpr w).getLsb idx := by
+        (BitVec.mulRec lexpr rexpr w).getLsbD idx := by
   intro idx hidx
   generalize hgo: go aig lhs rhs (curr + 1) hcurr acc = res
   unfold go at hgo
@@ -65,7 +65,7 @@ theorem go_denote_eq {w : Nat} (aig : AIG BVBit) (curr : Nat) (hcurr : curr + 1
       simp only [RefVec.denote_ite, RefVec.get_cast, Ref.cast_eq, BitVec.ofNat_eq_ofNat]
       split
       · next hdiscr =>
-        have : rexpr.getLsb (curr + 1) = true := by
+        have : rexpr.getLsbD (curr + 1) = true := by
           rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastAdd)] at hdiscr
           rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftLeftConst)] at hdiscr
           rw [hright] at hdiscr
@@ -77,14 +77,14 @@ theorem go_denote_eq {w : Nat} (aig : AIG BVBit) (curr : Nat) (hcurr : curr + 1
           rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftLeftConst)]
           rw [hacc]
         · intros
-          simp only [denote_blastShiftLeftConst, BitVec.getLsb_shiftLeft]
+          simp only [denote_blastShiftLeftConst, BitVec.getLsbD_shiftLeft]
           split
           · next hdiscr => simp [hdiscr]
           · next hidx hdiscr =>
             rw [hleft]
             simp [hdiscr, hidx]
       · next hdiscr =>
-        have : rexpr.getLsb (curr + 1) = false := by
+        have : rexpr.getLsbD (curr + 1) = false := by
           rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastAdd)] at hdiscr
           rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftLeftConst)] at hdiscr
           rw [hright] at hdiscr
@@ -98,8 +98,8 @@ theorem go_denote_eq {w : Nat} (aig : AIG BVBit) (curr : Nat) (hcurr : curr + 1
     rw [← hgo]
     rw [hacc]
     rw [BitVec.mulRec_succ_eq]
-    have : rexpr.getLsb (curr + 1) = false := by
-      apply BitVec.getLsb_ge
+    have : rexpr.getLsbD (curr + 1) = false := by
+      apply BitVec.getLsbD_ge
       omega
     simp [this]
 termination_by w - curr
@@ -112,14 +112,14 @@ end blastMul
 
 theorem denote_blastMul (aig : AIG BVBit) (lhs rhs : BitVec w) (assign : Assignment)
       (input : BinaryRefVec aig w)
-      (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.lhs.get idx hidx, assign.toAIGAssignment⟧ = lhs.getLsb idx)
-      (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.rhs.get idx hidx, assign.toAIGAssignment⟧ = rhs.getLsb idx) :
+      (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.lhs.get idx hidx, assign.toAIGAssignment⟧ = lhs.getLsbD idx)
+      (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.rhs.get idx hidx, assign.toAIGAssignment⟧ = rhs.getLsbD idx) :
       ∀ (idx : Nat) (hidx : idx < w),
         ⟦(blastMul aig input).aig, (blastMul aig input).vec.get idx hidx, assign.toAIGAssignment⟧
           =
-        (lhs * rhs).getLsb idx := by
+        (lhs * rhs).getLsbD idx := by
   intro idx hidx
-  rw [BitVec.getLsb_mul]
+  rw [BitVec.getLsbD_mul]
   generalize hb : blastMul aig input = res
   unfold blastMul at hb
   dsimp only at hb
@@ -145,7 +145,7 @@ theorem denote_blastMul (aig : AIG BVBit) (lhs rhs : BitVec w) (assign : Assignm
       rw [BitVec.mulRec_zero_eq]
       simp only [Nat.succ_eq_add_one, RefVec.denote_ite, BinaryRefVec.rhs_get_cast,
         Ref.gate_cast, BinaryRefVec.lhs_get_cast, denote_blastConst,
-        BitVec.ofNat_eq_ofNat, eval_const, BitVec.getLsb_zero, Bool.if_false_right,
+        BitVec.ofNat_eq_ofNat, eval_const, BitVec.getLsbD_zero, Bool.if_false_right,
         Bool.decide_eq_true]
       split
       · next heq =>
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftLeft.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftLeft.lean
index bbe2428935..146e32d48e 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftLeft.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftLeft.lean
@@ -173,8 +173,8 @@ namespace blastShiftLeft
 
 theorem twoPowShift_eq (aig : AIG α) (target : TwoPowShiftTarget aig w) (lhs : BitVec w)
     (rhs : BitVec target.n) (assign : α → Bool)
-    (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, target.lhs.get idx hidx, assign⟧ = lhs.getLsb idx)
-    (hright : ∀ (idx : Nat) (hidx : idx < target.n), ⟦aig, target.rhs.get idx hidx, assign⟧ = rhs.getLsb idx) :
+    (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, target.lhs.get idx hidx, assign⟧ = lhs.getLsbD idx)
+    (hright : ∀ (idx : Nat) (hidx : idx < target.n), ⟦aig, target.rhs.get idx hidx, assign⟧ = rhs.getLsbD idx) :
     ∀ (idx : Nat) (hidx : idx < w),
         ⟦
           (twoPowShift aig target).aig,
@@ -182,7 +182,7 @@ theorem twoPowShift_eq (aig : AIG α) (target : TwoPowShiftTarget aig w) (lhs :
           assign
         ⟧
           =
-        (lhs <<< (rhs &&& BitVec.twoPow target.n target.pow)).getLsb idx := by
+        (lhs <<< (rhs &&& BitVec.twoPow target.n target.pow)).getLsbD idx := by
   intro idx hidx
   generalize hg : twoPowShift aig target = res
   rcases target with ⟨n, lvec, rvec, pow⟩
@@ -202,14 +202,14 @@ theorem twoPowShift_eq (aig : AIG α) (target : TwoPowShiftTarget aig w) (lhs :
         apply Nat.mod_eq_of_lt
         apply Nat.pow_lt_pow_of_lt <;> omega
       split
-      · simp only [BitVec.shiftLeft_eq', BitVec.toNat_twoPow, BitVec.getLsb_shiftLeft,
+      · simp only [BitVec.shiftLeft_eq', BitVec.toNat_twoPow, BitVec.getLsbD_shiftLeft,
         Bool.false_eq, Bool.and_eq_false_imp, Bool.and_eq_true, decide_eq_true_eq,
         Bool.not_eq_true', decide_eq_false_iff_not, Nat.not_lt, and_imp]
         intros
-        apply BitVec.getLsb_ge
+        apply BitVec.getLsbD_ge
         omega
       · rw [hleft]
-        simp only [BitVec.shiftLeft_eq', BitVec.toNat_twoPow, hmod, BitVec.getLsb_shiftLeft, hidx,
+        simp only [BitVec.shiftLeft_eq', BitVec.toNat_twoPow, hmod, BitVec.getLsbD_shiftLeft, hidx,
           decide_True, Bool.true_and, Bool.iff_and_self, Bool.not_eq_true', decide_eq_false_iff_not,
           Nat.not_lt]
         omega
@@ -224,8 +224,8 @@ theorem twoPowShift_eq (aig : AIG α) (target : TwoPowShiftTarget aig w) (lhs :
       rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftLeftConst)]
       rw [hleft]
       simp
-  · have : rhs.getLsb pow = false := by
-      apply BitVec.getLsb_ge
+  · have : rhs.getLsbD pow = false := by
+      apply BitVec.getLsbD_ge
       dsimp only
       omega
     simp only [this, Bool.false_eq_true, ↓reduceIte]
@@ -236,8 +236,8 @@ theorem twoPowShift_eq (aig : AIG α) (target : TwoPowShiftTarget aig w) (lhs :
 theorem go_denote_eq (aig : AIG α) (distance : AIG.RefVec aig n) (curr : Nat)
       (hcurr : curr ≤ n - 1) (acc : AIG.RefVec aig w)
     (lhs : BitVec w) (rhs : BitVec n) (assign : α → Bool)
-    (hacc : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, acc.get idx hidx, assign⟧ = (BitVec.shiftLeftRec lhs rhs curr).getLsb idx)
-    (hright : ∀ (idx : Nat) (hidx : idx < n), ⟦aig, distance.get idx hidx, assign⟧ = rhs.getLsb idx) :
+    (hacc : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, acc.get idx hidx, assign⟧ = (BitVec.shiftLeftRec lhs rhs curr).getLsbD idx)
+    (hright : ∀ (idx : Nat) (hidx : idx < n), ⟦aig, distance.get idx hidx, assign⟧ = rhs.getLsbD idx) :
     ∀ (idx : Nat) (hidx : idx < w),
         ⟦
           (go aig distance curr hcurr acc).aig,
@@ -245,7 +245,7 @@ theorem go_denote_eq (aig : AIG α) (distance : AIG.RefVec aig n) (curr : Nat)
           assign
         ⟧
           =
-        (BitVec.shiftLeftRec lhs rhs (n - 1)).getLsb idx := by
+        (BitVec.shiftLeftRec lhs rhs (n - 1)).getLsbD idx := by
   intro idx hidx
   generalize hgo : go aig distance curr hcurr acc = res
   unfold go at hgo
@@ -271,8 +271,8 @@ end blastShiftLeft
 
 theorem denote_blastShiftLeft (aig : AIG α) (target : ArbitraryShiftTarget aig w0)
     (lhs : BitVec w0) (rhs : BitVec target.n) (assign : α → Bool)
-    (hleft : ∀ (idx : Nat) (hidx : idx < w0), ⟦aig, target.target.get idx hidx, assign⟧ = lhs.getLsb idx)
-    (hright : ∀ (idx : Nat) (hidx : idx < target.n), ⟦aig, target.distance.get idx hidx, assign⟧ = rhs.getLsb idx) :
+    (hleft : ∀ (idx : Nat) (hidx : idx < w0), ⟦aig, target.target.get idx hidx, assign⟧ = lhs.getLsbD idx)
+    (hright : ∀ (idx : Nat) (hidx : idx < target.n), ⟦aig, target.distance.get idx hidx, assign⟧ = rhs.getLsbD idx) :
     ∀ (idx : Nat) (hidx : idx < w0),
         ⟦
           (blastShiftLeft aig target).aig,
@@ -280,7 +280,7 @@ theorem denote_blastShiftLeft (aig : AIG α) (target : ArbitraryShiftTarget aig
           assign
         ⟧
           =
-        (lhs <<< rhs).getLsb idx := by
+        (lhs <<< rhs).getLsbD idx := by
   intro idx hidx
   rw [BitVec.shiftLeft_eq_shiftLeftRec]
   generalize hg : blastShiftLeft aig target = res
@@ -293,10 +293,10 @@ theorem denote_blastShiftLeft (aig : AIG α) (target : ArbitraryShiftTarget aig
     subst hzero
     rw [← hg]
     simp only [hleft, Nat.zero_sub, BitVec.shiftLeftRec_zero, BitVec.and_twoPow, Nat.le_refl,
-      BitVec.getLsb_ge, Bool.false_eq_true, ↓reduceIte, BitVec.reduceHShiftLeft',
-      BitVec.getLsb_shiftLeft, Nat.sub_zero, Bool.iff_and_self, Bool.and_eq_true, decide_eq_true_eq,
+      BitVec.getLsbD_ge, Bool.false_eq_true, ↓reduceIte, BitVec.reduceHShiftLeft',
+      BitVec.getLsbD_shiftLeft, Nat.sub_zero, Bool.iff_and_self, Bool.and_eq_true, decide_eq_true_eq,
       Bool.not_eq_true', decide_eq_false_iff_not, Nat.not_lt, Nat.zero_le, and_true]
-    apply BitVec.lt_of_getLsb
+    apply BitVec.lt_of_getLsbD
   · rw [← hg]
     rw [blastShiftLeft.go_denote_eq]
     · intro idx hidx
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftRight.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftRight.lean
index e58db6a8bd..5fcfbdeee3 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftRight.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftRight.lean
@@ -262,8 +262,8 @@ namespace blastShiftRight
 
 theorem twoPowShift_eq (aig : AIG α) (target : TwoPowShiftTarget aig w) (lhs : BitVec w)
     (rhs : BitVec target.n) (assign : α → Bool)
-    (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, target.lhs.get idx hidx, assign⟧ = lhs.getLsb idx)
-    (hright : ∀ (idx : Nat) (hidx : idx < target.n), ⟦aig, target.rhs.get idx hidx, assign⟧ = rhs.getLsb idx) :
+    (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, target.lhs.get idx hidx, assign⟧ = lhs.getLsbD idx)
+    (hright : ∀ (idx : Nat) (hidx : idx < target.n), ⟦aig, target.rhs.get idx hidx, assign⟧ = rhs.getLsbD idx) :
     ∀ (idx : Nat) (hidx : idx < w),
         ⟦
           (twoPowShift aig target).aig,
@@ -271,7 +271,7 @@ theorem twoPowShift_eq (aig : AIG α) (target : TwoPowShiftTarget aig w) (lhs :
           assign
         ⟧
           =
-        (lhs >>> (rhs &&& BitVec.twoPow target.n target.pow)).getLsb idx := by
+        (lhs >>> (rhs &&& BitVec.twoPow target.n target.pow)).getLsbD idx := by
   intro idx hidx
   generalize hg : twoPowShift aig target = res
   rcases target with ⟨n, lvec, rvec, pow⟩
@@ -293,9 +293,9 @@ theorem twoPowShift_eq (aig : AIG α) (target : TwoPowShiftTarget aig w) (lhs :
       split
       · rw [hleft]
         simp [hmod]
-      · simp only [BitVec.ushiftRight_eq', BitVec.toNat_twoPow, BitVec.getLsb_ushiftRight,
+      · simp only [BitVec.ushiftRight_eq', BitVec.toNat_twoPow, BitVec.getLsbD_ushiftRight,
         Bool.false_eq]
-        apply BitVec.getLsb_ge
+        apply BitVec.getLsbD_ge
         omega
     · next hif1 =>
       simp only [Bool.not_eq_true] at hif1
@@ -308,8 +308,8 @@ theorem twoPowShift_eq (aig : AIG α) (target : TwoPowShiftTarget aig w) (lhs :
       rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftRightConst)]
       rw [hleft]
       simp
-  · have : rhs.getLsb pow = false := by
-      apply BitVec.getLsb_ge
+  · have : rhs.getLsbD pow = false := by
+      apply BitVec.getLsbD_ge
       dsimp only
       omega
     simp only [this, Bool.false_eq_true, ↓reduceIte]
@@ -320,8 +320,8 @@ theorem twoPowShift_eq (aig : AIG α) (target : TwoPowShiftTarget aig w) (lhs :
 theorem go_denote_eq (aig : AIG α) (distance : AIG.RefVec aig n) (curr : Nat)
       (hcurr : curr ≤ n - 1) (acc : AIG.RefVec aig w)
     (lhs : BitVec w) (rhs : BitVec n) (assign : α → Bool)
-    (hacc : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, acc.get idx hidx, assign⟧ = (BitVec.ushiftRightRec lhs rhs curr).getLsb idx)
-    (hright : ∀ (idx : Nat) (hidx : idx < n), ⟦aig, distance.get idx hidx, assign⟧ = rhs.getLsb idx) :
+    (hacc : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, acc.get idx hidx, assign⟧ = (BitVec.ushiftRightRec lhs rhs curr).getLsbD idx)
+    (hright : ∀ (idx : Nat) (hidx : idx < n), ⟦aig, distance.get idx hidx, assign⟧ = rhs.getLsbD idx) :
     ∀ (idx : Nat) (hidx : idx < w),
         ⟦
           (go aig distance curr hcurr acc).aig,
@@ -329,7 +329,7 @@ theorem go_denote_eq (aig : AIG α) (distance : AIG.RefVec aig n) (curr : Nat)
           assign
         ⟧
           =
-        (BitVec.ushiftRightRec lhs rhs (n - 1)).getLsb idx := by
+        (BitVec.ushiftRightRec lhs rhs (n - 1)).getLsbD idx := by
   intro idx hidx
   generalize hgo : go aig distance curr hcurr acc = res
   unfold go at hgo
@@ -355,8 +355,8 @@ end blastShiftRight
 
 theorem denote_blastShiftRight (aig : AIG α) (target : ArbitraryShiftTarget aig w0)
     (lhs : BitVec w0) (rhs : BitVec target.n) (assign : α → Bool)
-    (hleft : ∀ (idx : Nat) (hidx : idx < w0), ⟦aig, target.target.get idx hidx, assign⟧ = lhs.getLsb idx)
-    (hright : ∀ (idx : Nat) (hidx : idx < target.n), ⟦aig, target.distance.get idx hidx, assign⟧ = rhs.getLsb idx) :
+    (hleft : ∀ (idx : Nat) (hidx : idx < w0), ⟦aig, target.target.get idx hidx, assign⟧ = lhs.getLsbD idx)
+    (hright : ∀ (idx : Nat) (hidx : idx < target.n), ⟦aig, target.distance.get idx hidx, assign⟧ = rhs.getLsbD idx) :
     ∀ (idx : Nat) (hidx : idx < w0),
         ⟦
           (blastShiftRight aig target).aig,
@@ -364,7 +364,7 @@ theorem denote_blastShiftRight (aig : AIG α) (target : ArbitraryShiftTarget aig
           assign
         ⟧
           =
-        (lhs >>> rhs).getLsb idx := by
+        (lhs >>> rhs).getLsbD idx := by
   intro idx hidx
   rw [BitVec.shiftRight_eq_ushiftRightRec]
   generalize hres : blastShiftRight aig target = res
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Ult.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Ult.lean
index a338a26ee6..56e31838f5 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Ult.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Ult.lean
@@ -24,8 +24,8 @@ variable [Hashable α] [DecidableEq α]
 
 theorem mkUlt_denote_eq (aig : AIG α) (lhs rhs : BitVec w) (input : BinaryRefVec aig w)
     (assign : α → Bool)
-    (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.lhs.get idx hidx, assign⟧ = lhs.getLsb idx)
-    (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.rhs.get idx hidx, assign⟧ = rhs.getLsb idx) :
+    (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.lhs.get idx hidx, assign⟧ = lhs.getLsbD idx)
+    (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.rhs.get idx hidx, assign⟧ = rhs.getLsbD idx) :
     ⟦(mkUlt aig input).aig, (mkUlt aig input).ref, assign⟧ = BitVec.ult lhs rhs := by
   rw [BitVec.ult_eq_not_carry]
   unfold mkUlt
@@ -42,7 +42,7 @@ theorem mkUlt_denote_eq (aig : AIG α) (lhs rhs : BitVec w) (input : BinaryRefVe
   · dsimp only
     intro idx hidx
     rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
-    · simp only [RefVec.get_cast, Ref.gate_cast, BitVec.getLsb_not, hidx, decide_True,
+    · simp only [RefVec.get_cast, Ref.gate_cast, BitVec.getLsbD_not, hidx, decide_True,
         Bool.true_and]
       rw [BVExpr.bitblast.denote_blastNot]
       congr 1
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Pred.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Pred.lean
index d1dca38eb2..ddd3f678f2 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Pred.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Pred.lean
@@ -6,7 +6,7 @@ Authors: Henrik Böving
 prelude
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Eq
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Ult
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.GetLsb
+import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.GetLsbD
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Pred
 
@@ -48,10 +48,10 @@ theorem denote_bitblast (aig : AIG BVBit) (pred : BVPred) (assign : BVExpr.Assig
         · simp [Ref.hgate]
       · intros
         simp
-  | getLsb expr idx =>
-    simp only [bitblast, denote_blastGetLsb, BVExpr.denote_bitblast, dite_eq_ite,
-      Bool.if_false_right, eval_getLsb, Bool.and_iff_right_iff_imp, decide_eq_true_eq]
-    apply BitVec.lt_of_getLsb
+  | getLsbD expr idx =>
+    simp only [bitblast, denote_blastGetLsbD, BVExpr.denote_bitblast, dite_eq_ite,
+      Bool.if_false_right, eval_getLsbD, Bool.and_iff_right_iff_imp, decide_eq_true_eq]
+    apply BitVec.lt_of_getLsbD
 
 end BVPred
 
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Var.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Var.lean
index a23147ec87..66cdb77688 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Var.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Var.lean
@@ -85,7 +85,7 @@ theorem go_denote_eq (aig : AIG BVBit) (a : Nat) (assign : Assignment) (curr : N
           assign.toAIGAssignment
         ⟧
           =
-        ((BVExpr.var (w := w) a).eval assign).getLsb idx := by
+        ((BVExpr.var (w := w) a).eval assign).getLsbD idx := by
   intro idx hidx1 hidx2
   generalize hgo : go aig w a curr s hcurr = res
   unfold go at hgo
@@ -118,7 +118,7 @@ theorem denote_blastVar (aig : AIG BVBit) (var : BVVar w) (assign : Assignment)
     ∀ (idx : Nat) (hidx : idx < w),
         ⟦(blastVar aig var).aig, (blastVar aig var).vec.get idx hidx, assign.toAIGAssignment⟧
           =
-        ((BVExpr.var (w := w) var.ident).eval assign).getLsb idx := by
+        ((BVExpr.var (w := w) var.ident).eval assign).getLsbD idx := by
   intros
   apply blastVar.go_denote_eq
   omega
diff --git a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
index f615093dd1..6600f57cc0 100644
--- a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
+++ b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
@@ -34,7 +34,7 @@ attribute [bv_normalize] ge_iff_le
 theorem BitVec.truncate_eq_zeroExtend (x : BitVec w) : x.truncate n = x.zeroExtend n := by
   rfl
 
-attribute [bv_normalize] BitVec.msb_eq_getLsb_last
+attribute [bv_normalize] BitVec.msb_eq_getLsbD_last
 attribute [bv_normalize] BitVec.slt_eq_ult
 attribute [bv_normalize] BitVec.sle_eq_not_slt
 
@@ -57,9 +57,9 @@ attribute [bv_normalize] BitVec.sub_self
 attribute [bv_normalize] BitVec.sub_zero
 attribute [bv_normalize] BitVec.zeroExtend_eq
 attribute [bv_normalize] BitVec.zeroExtend_zero
-attribute [bv_normalize] BitVec.getLsb_zero
-attribute [bv_normalize] BitVec.getLsb_zero_length
-attribute [bv_normalize] BitVec.getLsb_concat_zero
+attribute [bv_normalize] BitVec.getLsbD_zero
+attribute [bv_normalize] BitVec.getLsbD_zero_length
+attribute [bv_normalize] BitVec.getLsbD_concat_zero
 attribute [bv_normalize] BitVec.mul_one
 attribute [bv_normalize] BitVec.one_mul
 
@@ -123,12 +123,12 @@ theorem BitVec.neg_add (a : BitVec w) : (-a) + a = 0#w := by
 @[bv_normalize]
 theorem BitVec.zero_sshiftRight : BitVec.sshiftRight 0#w a = 0#w := by
   ext
-  simp [BitVec.getLsb_sshiftRight]
+  simp [BitVec.getLsbD_sshiftRight]
 
 @[bv_normalize]
 theorem BitVec.sshiftRight_zero : BitVec.sshiftRight a 0 = a := by
   ext
-  simp [BitVec.getLsb_sshiftRight]
+  simp [BitVec.getLsbD_sshiftRight]
 
 @[bv_normalize]
 theorem BitVec.mul_zero (a : BitVec w) : a * 0#w = 0#w := by
diff --git a/src/Std/Tactic/BVDecide/Normalize/Canonicalize.lean b/src/Std/Tactic/BVDecide/Normalize/Canonicalize.lean
index 536efd9bf3..d585be7c18 100644
--- a/src/Std/Tactic/BVDecide/Normalize/Canonicalize.lean
+++ b/src/Std/Tactic/BVDecide/Normalize/Canonicalize.lean
@@ -75,7 +75,7 @@ theorem Bool.decide_eq_true (a : Bool) : (decide (a = true)) = a := by
 theorem Bool.eq_true_eq_true_eq (x y : Bool) : ((x = true) = (y = true)) = (x = y) :=
   by simp
 
-attribute [bv_normalize] BitVec.getLsb_cast
+attribute [bv_normalize] BitVec.getLsbD_cast
 attribute [bv_normalize] BitVec.testBit_toNat
 
 @[bv_normalize]
diff --git a/src/Std/Tactic/BVDecide/Reflect.lean b/src/Std/Tactic/BVDecide/Reflect.lean
index f23b3e486c..bf1fb46d62 100644
--- a/src/Std/Tactic/BVDecide/Reflect.lean
+++ b/src/Std/Tactic/BVDecide/Reflect.lean
@@ -103,11 +103,11 @@ theorem ult_congr (lhs rhs lhs' rhs' : BitVec w) (h1 : lhs' = lhs) (h2 : rhs' =
     (BitVec.ult lhs' rhs') = (BitVec.ult lhs rhs) := by
   simp[*]
 
-theorem getLsb_congr (i : Nat) (w : Nat) (e e' : BitVec w) (h : e' = e) :
-    (e'.getLsb i) = (e.getLsb i) := by
+theorem getLsbD_congr (i : Nat) (w : Nat) (e e' : BitVec w) (h : e' = e) :
+    (e'.getLsbD i) = (e.getLsbD i) := by
   simp[*]
 
-theorem ofBool_congr (b : Bool) (e' : BitVec 1) (h : e' = BitVec.ofBool b) : e'.getLsb 0 = b := by
+theorem ofBool_congr (b : Bool) (e' : BitVec 1) (h : e' = BitVec.ofBool b) : e'.getLsbD 0 = b := by
   cases b <;> simp [h]
 
 end BitVec
diff --git a/tests/lean/interactive/completionPrv.lean.expected.out b/tests/lean/interactive/completionPrv.lean.expected.out
index 6125fd9478..3dff7f4398 100644
--- a/tests/lean/interactive/completionPrv.lean.expected.out
+++ b/tests/lean/interactive/completionPrv.lean.expected.out
@@ -30,21 +30,21 @@
      "position": {"line": 9, "character": 11}},
     "id": {"const": {"declName": "instToBoolBool"}}}},
   {"sortText": "2",
-   "label": "BitVec.getLsb_ofBoolListBE",
+   "label": "BitVec.getLsbD_ofBoolListBE",
    "kind": 3,
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completionPrv.lean"},
      "position": {"line": 9, "character": 11}},
-    "id": {"const": {"declName": "BitVec.getLsb_ofBoolListBE"}}}},
+    "id": {"const": {"declName": "BitVec.getLsbD_ofBoolListBE"}}}},
   {"sortText": "3",
-   "label": "BitVec.getMsb_ofBoolListBE",
+   "label": "BitVec.getMsbD_ofBoolListBE",
    "kind": 3,
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completionPrv.lean"},
      "position": {"line": 9, "character": 11}},
-    "id": {"const": {"declName": "BitVec.getMsb_ofBoolListBE"}}}},
+    "id": {"const": {"declName": "BitVec.getMsbD_ofBoolListBE"}}}},
   {"sortText": "4",
    "label": "BitVec.ofBoolListBE",
    "kind": 3,
diff --git a/tests/lean/run/bitvec_simproc.lean b/tests/lean/run/bitvec_simproc.lean
index b6d2ca276e..3056b4d215 100644
--- a/tests/lean/run/bitvec_simproc.lean
+++ b/tests/lean/run/bitvec_simproc.lean
@@ -43,13 +43,13 @@ example (h : x = (1 : BitVec 32)) : x = - smtSDiv 9 0 := by
   simp; guard_target =ₛ x = 1#32; assumption
 example (h : x = (1 : BitVec 32)) : x = smtSDiv (-9) 0 := by
   simp; guard_target =ₛ x = 1#32; assumption
-example (h : x = false) : x = (4#3).getLsb 0:= by
+example (h : x = false) : x = (4#3).getLsbD 0:= by
   simp; guard_target =ₛ x = false; assumption
-example (h : x = true) : x = (4#3).getLsb 2:= by
+example (h : x = true) : x = (4#3).getLsbD 2:= by
   simp; guard_target =ₛ x = true; assumption
-example (h : x = true) : x = (4#3).getMsb 0:= by
+example (h : x = true) : x = (4#3).getMsbD 0:= by
   simp; guard_target =ₛ x = true; assumption
-example (h : x = false) : x = (4#3).getMsb 2:= by
+example (h : x = false) : x = (4#3).getMsbD 2:= by
   simp; guard_target =ₛ x = false; assumption
 example (h : x = (24 : BitVec 32)) : x = 6#32 <<< 2 := by
   simp; guard_target =ₛ x = 24#32; assumption
diff --git a/tests/lean/run/bv_bitwise.lean b/tests/lean/run/bv_bitwise.lean
index b5d6dd4a80..fe92517b40 100644
--- a/tests/lean/run/bv_bitwise.lean
+++ b/tests/lean/run/bv_bitwise.lean
@@ -14,16 +14,16 @@ theorem bitwise_unit_2 {x : BitVec 64} : x ^^^ x = 0 := by
 theorem bitwise_unit_2' {x : BitVec 64} : (BitVec.xor x x) = 0 := by
   bv_decide
 
-theorem bitwise_unit_3 {x : BitVec 64} : (x ^^^ x).getLsb 32 = false := by
+theorem bitwise_unit_3 {x : BitVec 64} : (x ^^^ x).getLsbD 32 = false := by
   bv_decide
 
-theorem bitwise_unit_4 {x : BitVec 64} : (x ^^^ ~~~x).getLsb 32 = true := by
+theorem bitwise_unit_4 {x : BitVec 64} : (x ^^^ ~~~x).getLsbD 32 = true := by
   bv_decide
 
-theorem bitwise_unit_5 {x : BitVec 64} : (x ^^^ ~~~x).getLsb 128 = false := by
+theorem bitwise_unit_5 {x : BitVec 64} : (x ^^^ ~~~x).getLsbD 128 = false := by
   bv_decide
 
-theorem bitwise_unit_6 {x : BitVec 64} : (x ^^^ ~~~x).getLsb 63 = (x ^^^ ~~~x).msb := by
+theorem bitwise_unit_6 {x : BitVec 64} : (x ^^^ ~~~x).getLsbD 63 = (x ^^^ ~~~x).msb := by
   bv_decide
 
 theorem bitwise_unit_7 (x : BitVec 32) : x ^^^ 123#32 = 123#'(by decide) ^^^ x := by
diff --git a/tests/lean/run/bv_cast.lean b/tests/lean/run/bv_cast.lean
index 3acb675649..cd5fa35339 100644
--- a/tests/lean/run/bv_cast.lean
+++ b/tests/lean/run/bv_cast.lean
@@ -35,5 +35,5 @@ theorem cast_unit_8 (x : BitVec 64) : (x.signExtend 128 = x.zeroExtend 128) ↔
 theorem cast_unit_9 (x : BitVec 32) : (x.replicate 20).zeroExtend 32 = x := by
   bv_decide
 
-theorem cast_unit_10 (x : BitVec 32) : (x.replicate 20).getLsb 40 = x.getLsb 8 := by
+theorem cast_unit_10 (x : BitVec 32) : (x.replicate 20).getLsbD 40 = x.getLsbD 8 := by
   bv_decide
diff --git a/tests/lean/run/bv_will_overflow.lean b/tests/lean/run/bv_will_overflow.lean
index d9e8a092a1..418a6d29ed 100644
--- a/tests/lean/run/bv_will_overflow.lean
+++ b/tests/lean/run/bv_will_overflow.lean
@@ -78,7 +78,7 @@ bool will_add_overflow_bitwise_3(int32_t a_, int32_t b_) {
 -/
 def will_add_overflow_bitwise_3 (a b : BitVec 32) : Bool :=
   let c := a + b
-  getLsb (((~~~a &&& ~~~b &&& c) ||| (a &&& b &&& ~~~c)) >>> 31) 0
+  getLsbD (((~~~a &&& ~~~b &&& c) ||| (a &&& b &&& ~~~c)) >>> 31) 0
 
 example (a b : BitVec 32) : will_add_overflow_bitwise_2 a b = will_add_overflow_bitwise_3 a b := by
   dsimp [will_add_overflow_bitwise_2, will_add_overflow_bitwise_3]
@@ -93,7 +93,7 @@ bool will_add_overflow_optimized_a(int32_t a_, int32_t b_) {
 -/
 def will_add_overflow_optimized_a (a b : BitVec 32) : Bool :=
   let c := a + b
-  getLsb ((~~~(a ^^^ b) &&& (c ^^^ a)) >>> 31) 0
+  getLsbD ((~~~(a ^^^ b) &&& (c ^^^ a)) >>> 31) 0
 
 example (a b : BitVec 32) :
     will_add_overflow_bitwise_3 a b = will_add_overflow_optimized_a a b := by
@@ -109,7 +109,7 @@ bool will_add_overflow_optimized_b(int32_t a_, int32_t b_) {
 -/
 def will_add_overflow_optimized_b (a b : BitVec 32) : Bool :=
   let c := a + b
-  getLsb (((c ^^^ a) &&& (c ^^^ b)) >>> 31) 0
+  getLsbD (((c ^^^ a) &&& (c ^^^ b)) >>> 31) 0
 
 example (a b : BitVec 32) :
     will_add_overflow_optimized_a a b = will_add_overflow_optimized_b a b := by