-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
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)

Proof state:
case pos
w : Nat
x : BitVec w
s i : Nat
hmsb : x.msb = false
hi : i ≥ w
⊢ x.getLsbD (s + i) = (!decide (w ≤ i) && (decide (s + i < w) && x.getLsbD (s + i)))

Tactic:
simp only [hi, decide_true, Bool.not_true, Bool.false_and]

Result:
case pos
w : Nat
x : BitVec w
s i : Nat
hmsb : x.msb = false
hi : i ≥ w
⊢ x.getLsbD (s + i) = false

Proof state:
case pos
w : Nat
x : BitVec w
s i : Nat
hmsb : x.msb = false
hi : i ≥ w
⊢ x.getLsbD (s + i) = false

Tactic:
apply getLsbD_ge

Result:
case pos.ge
w : Nat
x : BitVec w
s i : Nat
hmsb : x.msb = false
hi : i ≥ w
⊢ w ≤ s + i

Proof state:
case neg
w : Nat
x : BitVec w
s i : Nat
hmsb : x.msb = true
hi : ¬i ≥ w
⊢ (x.sshiftRight s).getLsbD i = (!decide (w ≤ i) && if s + i < w then x.getLsbD (s + i) else true)

Tactic:
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]

Result:
case neg
w : Nat
x : BitVec w
s i : Nat
hmsb : x.msb = true
hi : ¬i ≥ w
⊢ w ≤ s + i ∨ x.getLsbD (s + i) = true → i < w

Proof state:
case neg
w : Nat
x : BitVec w
s i : Nat
hmsb : x.msb = false
hi : ¬i ≥ w
⊢ x.getLsbD (s + i) = true → s + i < w

Tactic:
intros hlsb

Result:
case neg
w : Nat
x : BitVec w
s i : Nat
hmsb : x.msb = false
hi : ¬i ≥ w
hlsb : x.getLsbD (s + i) = true
⊢ s + i < w

Proof state:
case false
w : Nat
x : BitVec w
s i : Nat
hmsb : x.msb = false
⊢ (x.sshiftRight s).getLsbD i = (!decide (w ≤ i) && if s + i < w then x.getLsbD (s + i) else false)

Tactic:
simp only [sshiftRight_eq_of_msb_false hmsb, getLsbD_ushiftRight, Bool.if_false_right]

Result:
case false
w : Nat
x : BitVec w
s i : Nat
hmsb : x.msb = false
⊢ x.getLsbD (s + i) = (!decide (w ≤ i) && (decide (s + i < w) && x.getLsbD (s + i)))

Proof state:
case neg
w : Nat
x : BitVec w
s i : Nat
hmsb : x.msb = false
hi : ¬i ≥ w
⊢ x.getLsbD (s + i) = (!decide (w ≤ i) && (decide (s + i < w) && x.getLsbD (s + i)))

Tactic:
simp only [hi, decide_false, Bool.not_false, Bool.true_and, Bool.iff_and_self,
  decide_eq_true_eq]

Result:
case neg
w : Nat
x : BitVec w
s i : Nat
hmsb : x.msb = false
hi : ¬i ≥ w
⊢ x.getLsbD (s + i) = true → s + i < w

Proof state:
case pos
w : Nat
x : BitVec w
s i : Nat
hmsb : x.msb = true
hi : i ≥ w
⊢ (x.sshiftRight s).getLsbD i = (!decide (w ≤ i) && if s + i < w then x.getLsbD (s + i) else true)

Tactic:
simp [hi]

Result:
no goals

Proof state:
case neg
w : Nat
x : BitVec w
s i : Nat
hmsb : x.msb = false
hi : ¬i ≥ w
hlsb : x.getLsbD (s + i) = true
⊢ s + i < w

Tactic:
apply BitVec.lt_of_getLsbD hlsb

Result:
no goals

Proof state:
w : Nat
x : BitVec w
s i : Nat
⊢ (x.sshiftRight s).getLsbD i = (!decide (w ≤ i) && if s + i < w then x.getLsbD (s + i) else x.msb)

Tactic:
rcases hmsb : x.msb with rfl | rfl

Result:
case false
w : Nat
x : BitVec w
s i : Nat
hmsb : x.msb = false
⊢ (x.sshiftRight s).getLsbD i = (!decide (w ≤ i) && if s + i < w then x.getLsbD (s + i) else false)

case true
w : Nat
x : BitVec w
s i : Nat
hmsb : x.msb = true
⊢ (x.sshiftRight s).getLsbD i = (!decide (w ≤ i) && if s + i < w then x.getLsbD (s + i) else true)

Proof state:
case true
w : Nat
x : BitVec w
s i : Nat
hmsb : x.msb = true
⊢ (x.sshiftRight s).getLsbD i = (!decide (w ≤ i) && if s + i < w then x.getLsbD (s + i) else true)

Tactic:
by_cases hi : i ≥ w

Result:
case pos
w : Nat
x : BitVec w
s i : Nat
hmsb : x.msb = true
hi : i ≥ w
⊢ (x.sshiftRight s).getLsbD i = (!decide (w ≤ i) && if s + i < w then x.getLsbD (s + i) else true)

case neg
w : Nat
x : BitVec w
s i : Nat
hmsb : x.msb = true
hi : ¬i ≥ w
⊢ (x.sshiftRight s).getLsbD i = (!decide (w ≤ i) && if s + i < w then x.getLsbD (s + i) else true)

Proof state:
case false
w : Nat
x : BitVec w
s i : Nat
hmsb : x.msb = false
⊢ x.getLsbD (s + i) = (!decide (w ≤ i) && (decide (s + i < w) && x.getLsbD (s + i)))

Tactic:
by_cases hi : i ≥ w

Result:
case pos
w : Nat
x : BitVec w
s i : Nat
hmsb : x.msb = false
hi : i ≥ w
⊢ x.getLsbD (s + i) = (!decide (w ≤ i) && (decide (s + i < w) && x.getLsbD (s + i)))

case neg
w : Nat
x : BitVec w
s i : Nat
hmsb : x.msb = false
hi : ¬i ≥ w
⊢ x.getLsbD (s + i) = (!decide (w ≤ i) && (decide (s + i < w) && x.getLsbD (s + i)))

Proof state:
case pos.ge
w : Nat
x : BitVec w
s i : Nat
hmsb : x.msb = false
hi : i ≥ w
⊢ w ≤ s + i

Tactic:
omega

Result:
no goals

Proof state:
case neg
w : Nat
x : BitVec w
s i : Nat
hmsb : x.msb = true
hi : ¬i ≥ w
⊢ w ≤ s + i ∨ x.getLsbD (s + i) = true → i < w

Tactic:
omega

Result:
no goals