-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getMsbD_sshiftRight {x : BitVec w} {i n : Nat} :
    getMsbD (x.sshiftRight n) i = (decide (i < w) && if i < n then x.msb else getMsbD x (i - n))

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

Tactic:
by_cases h : i < w

Result:
case pos
w : Nat
x : BitVec w
i n : Nat
h : i < w
⊢ (decide (i < w) && (!decide (w ≤ w - 1 - i) && if n + (w - 1 - i) < w then x.getLsbD (n + (w - 1 - i)) else x.msb)) =
    (decide (i < w) && if i < n then x.msb else decide (i - n < w) && x.getLsbD (w - 1 - (i - n)))

case neg
w : Nat
x : BitVec w
i n : Nat
h : ¬i < w
⊢ (decide (i < w) && (!decide (w ≤ w - 1 - i) && if n + (w - 1 - i) < w then x.getLsbD (n + (w - 1 - i)) else x.msb)) =
    (decide (i < w) && if i < n then x.msb else decide (i - n < w) && x.getLsbD (w - 1 - (i - n)))

Proof state:
case pos
w : Nat
x : BitVec w
i n : Nat
h : i < w
h₁ : ¬w ≤ w - 1 - i
h₂ : i < n
⊢ (if n + (w - 1 - i) < w then x.getLsbD (n + (w - 1 - i)) else x.msb) =
    if i < n then x.msb else decide (i - n < w) && x.getLsbD (w - 1 - (i - n))

Tactic:
simp only [h₂, ↓reduceIte, ite_eq_right_iff]

Result:
case pos
w : Nat
x : BitVec w
i n : Nat
h : i < w
h₁ : ¬w ≤ w - 1 - i
h₂ : i < n
⊢ n + (w - 1 - i) < w → x.getLsbD (n + (w - 1 - i)) = x.msb

Proof state:
case pos
w : Nat
x : BitVec w
i n : Nat
h : i < w
h₁ : w ≤ w - 1 - i
⊢ (!decide (w ≤ w - 1 - i) && if n + (w - 1 - i) < w then x.getLsbD (n + (w - 1 - i)) else x.msb) =
    if i < n then x.msb else decide (i - n < w) && x.getLsbD (w - 1 - (i - n))

Tactic:
simp [h₁]

Result:
case pos
w : Nat
x : BitVec w
i n : Nat
h : i < w
h₁ : w ≤ w - 1 - i
⊢ if i < n then x.msb = false else i - n < w → x.getLsbD (w - 1 - (i - n)) = false

Proof state:
case neg
w : Nat
x : BitVec w
i n : Nat
h : i < w
h₁ : ¬w ≤ w - 1 - i
h₂ : ¬i < n
⊢ (if n + (w - 1 - i) < w then x.getLsbD (n + (w - 1 - i)) else x.msb) = x.getLsbD (w - 1 - (i - n))

Tactic:
by_cases h₄ : n + (w - 1 - i) < w <;> (simp only [h₄, ↓reduceIte]; congr; omega)

Result:
no goals

Proof state:
case pos
w : Nat
x : BitVec w
i n : Nat
h : i < w
⊢ (decide (i < w) && (!decide (w ≤ w - 1 - i) && if n + (w - 1 - i) < w then x.getLsbD (n + (w - 1 - i)) else x.msb)) =
    (decide (i < w) && if i < n then x.msb else decide (i - n < w) && x.getLsbD (w - 1 - (i - n)))

Tactic:
simp only [h, decide_true, Bool.true_and]

Result:
case pos
w : Nat
x : BitVec w
i n : Nat
h : i < w
⊢ (!decide (w ≤ w - 1 - i) && if n + (w - 1 - i) < w then x.getLsbD (n + (w - 1 - i)) else x.msb) =
    if i < n then x.msb else decide (i - n < w) && x.getLsbD (w - 1 - (i - n))

Proof state:
case pos
w : Nat
x : BitVec w
i n : Nat
h : i < w
h₁ : w ≤ w - 1 - i
⊢ if i < n then x.msb = false else i - n < w → x.getLsbD (w - 1 - (i - n)) = false

Tactic:
omega

Result:
no goals

Proof state:
case neg
w : Nat
x : BitVec w
i n : Nat
h : i < w
h₁ : ¬w ≤ w - 1 - i
h₂ : ¬i < n
h₄ : ¬n + (w - 1 - i) < w
⊢ x.msb = x.getLsbD (w - 1 - (i - n))

Tactic:
omega

Result:
no goals

Proof state:
case neg
w : Nat
x : BitVec w
i n : Nat
h : i < w
h₁ : ¬w ≤ w - 1 - i
h₂ : ¬i < n
h₄ : ¬n + (w - 1 - i) < w
⊢ (if n + (w - 1 - i) < w then x.getLsbD (n + (w - 1 - i)) else x.msb) = x.getLsbD (w - 1 - (i - n))

Tactic:
simp only [h₄, ↓reduceIte]

Result:
case neg
w : Nat
x : BitVec w
i n : Nat
h : i < w
h₁ : ¬w ≤ w - 1 - i
h₂ : ¬i < n
h₄ : ¬n + (w - 1 - i) < w
⊢ x.msb = x.getLsbD (w - 1 - (i - n))

Proof state:
case neg
w : Nat
x : BitVec w
i n : Nat
h : i < w
h₁ : ¬w ≤ w - 1 - i
h₂ : ¬i < n
⊢ (if n + (w - 1 - i) < w then x.getLsbD (n + (w - 1 - i)) else x.msb) =
    if i < n then x.msb else decide (i - n < w) && x.getLsbD (w - 1 - (i - n))

Tactic:
simp only [show i - n < w by omega, h₂, ↓reduceIte, decide_true, Bool.true_and]

Result:
case neg
w : Nat
x : BitVec w
i n : Nat
h : i < w
h₁ : ¬w ≤ w - 1 - i
h₂ : ¬i < n
⊢ (if n + (w - 1 - i) < w then x.getLsbD (n + (w - 1 - i)) else x.msb) = x.getLsbD (w - 1 - (i - n))

Proof state:
w : Nat
x : BitVec w
i n : Nat
h : i < w
h₁ : ¬w ≤ w - 1 - i
h₂ : ¬i < n
⊢ i - n < w

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x : BitVec w
i n : Nat
⊢ (x.sshiftRight n).getMsbD i = (decide (i < w) && if i < n then x.msb else x.getMsbD (i - n))

Tactic:
simp only [getMsbD, BitVec.getLsbD_sshiftRight]

Result:
w : Nat
x : BitVec w
i n : Nat
⊢ (decide (i < w) && (!decide (w ≤ w - 1 - i) && if n + (w - 1 - i) < w then x.getLsbD (n + (w - 1 - i)) else x.msb)) =
    (decide (i < w) && if i < n then x.msb else decide (i - n < w) && x.getLsbD (w - 1 - (i - n)))

Proof state:
case neg
w : Nat
x : BitVec w
i n : Nat
h : ¬i < w
⊢ (decide (i < w) && (!decide (w ≤ w - 1 - i) && if n + (w - 1 - i) < w then x.getLsbD (n + (w - 1 - i)) else x.msb)) =
    (decide (i < w) && if i < n then x.msb else decide (i - n < w) && x.getLsbD (w - 1 - (i - n)))

Tactic:
simp [h]

Result:
no goals

Proof state:
case neg
w : Nat
x : BitVec w
i n : Nat
h : i < w
h₁ : ¬w ≤ w - 1 - i
⊢ (if n + (w - 1 - i) < w then x.getLsbD (n + (w - 1 - i)) else x.msb) =
    if i < n then x.msb else decide (i - n < w) && x.getLsbD (w - 1 - (i - n))

Tactic:
by_cases h₂ : i < n

Result:
case pos
w : Nat
x : BitVec w
i n : Nat
h : i < w
h₁ : ¬w ≤ w - 1 - i
h₂ : i < n
⊢ (if n + (w - 1 - i) < w then x.getLsbD (n + (w - 1 - i)) else x.msb) =
    if i < n then x.msb else decide (i - n < w) && x.getLsbD (w - 1 - (i - n))

case neg
w : Nat
x : BitVec w
i n : Nat
h : i < w
h₁ : ¬w ≤ w - 1 - i
h₂ : ¬i < n
⊢ (if n + (w - 1 - i) < w then x.getLsbD (n + (w - 1 - i)) else x.msb) =
    if i < n then x.msb else decide (i - n < w) && x.getLsbD (w - 1 - (i - n))

Proof state:
case pos
w : Nat
x : BitVec w
i n : Nat
h : i < w
h₁ : ¬w ≤ w - 1 - i
h₂ : i < n
⊢ n + (w - 1 - i) < w → x.getLsbD (n + (w - 1 - i)) = x.msb

Tactic:
omega

Result:
no goals

Proof state:
case neg
w : Nat
x : BitVec w
i n : Nat
h : i < w
h₁ : ¬w ≤ w - 1 - i
⊢ (!decide (w ≤ w - 1 - i) && if n + (w - 1 - i) < w then x.getLsbD (n + (w - 1 - i)) else x.msb) =
    if i < n then x.msb else decide (i - n < w) && x.getLsbD (w - 1 - (i - n))

Tactic:
simp only [h₁, decide_false, Bool.not_false, Bool.true_and]

Result:
case neg
w : Nat
x : BitVec w
i n : Nat
h : i < w
h₁ : ¬w ≤ w - 1 - i
⊢ (if n + (w - 1 - i) < w then x.getLsbD (n + (w - 1 - i)) else x.msb) =
    if i < n then x.msb else decide (i - n < w) && x.getLsbD (w - 1 - (i - n))

Proof state:
case pos
w : Nat
x : BitVec w
i n : Nat
h : i < w
⊢ (!decide (w ≤ w - 1 - i) && if n + (w - 1 - i) < w then x.getLsbD (n + (w - 1 - i)) else x.msb) =
    if i < n then x.msb else decide (i - n < w) && x.getLsbD (w - 1 - (i - n))

Tactic:
by_cases h₁ : w ≤ w - 1 - i

Result:
case pos
w : Nat
x : BitVec w
i n : Nat
h : i < w
h₁ : w ≤ w - 1 - i
⊢ (!decide (w ≤ w - 1 - i) && if n + (w - 1 - i) < w then x.getLsbD (n + (w - 1 - i)) else x.msb) =
    if i < n then x.msb else decide (i - n < w) && x.getLsbD (w - 1 - (i - n))

case neg
w : Nat
x : BitVec w
i n : Nat
h : i < w
h₁ : ¬w ≤ w - 1 - i
⊢ (!decide (w ≤ w - 1 - i) && if n + (w - 1 - i) < w then x.getLsbD (n + (w - 1 - i)) else x.msb) =
    if i < n then x.msb else decide (i - n < w) && x.getLsbD (w - 1 - (i - n))

Proof state:
case pos
w : Nat
x : BitVec w
i n : Nat
h : i < w
h₁ : ¬w ≤ w - 1 - i
h₂ : ¬i < n
h₄ : n + (w - 1 - i) < w
⊢ x.getLsbD (n + (w - 1 - i)) = x.getLsbD (w - 1 - (i - n))

Tactic:
congr

Result:
case pos.e_i
w : Nat
x : BitVec w
i n : Nat
h : i < w
h₁ : ¬w ≤ w - 1 - i
h₂ : ¬i < n
h₄ : n + (w - 1 - i) < w
⊢ n + (w - 1 - i) = w - 1 - (i - n)