-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getMsbD_rotateRight {w n m : Nat} {x : BitVec w} :
    (x.rotateRight m).getMsbD n = (decide (n < w) && (if (n < m % w)
    then x.getMsbD ((w + n - m % w) % w) else x.getMsbD (n - m % w)))

Proof state:
n m w : Nat
x : BitVec (w + 1)
h₀ : m < w
⊢ m < w + 1

Tactic:
omega

Result:
no goals

Proof state:
case neg
n m w : Nat
x : BitVec (w + 1)
h₀ : ¬m < w
⊢ (decide (n < w + 1) &&
      if n < m % (w + 1) % (w + 1) then x.getMsbD ((w + 1 + n - m % (w + 1) % (w + 1)) % (w + 1))
      else x.getMsbD (n - m % (w + 1) % (w + 1))) =
    (decide (n < w + 1) &&
      if n < m % (w + 1) then x.getMsbD ((w + 1 + n - m % (w + 1)) % (w + 1)) else x.getMsbD (n - m % (w + 1)))

Tactic:
simp

Result:
no goals

Proof state:
case pos
n m w : Nat
x : BitVec (w + 1)
h₀ : m < w
⊢ (x.rotateRight m).getMsbD n =
    (decide (n < w + 1) &&
      if n < m % (w + 1) then x.getMsbD ((w + 1 + n - m % (w + 1)) % (w + 1)) else x.getMsbD (n - m % (w + 1)))

Tactic:
rw [getMsbD_rotateRight_of_lt (by omega)]

Result:
no goals

Proof state:
case succ
n m w : Nat
x : BitVec (w + 1)
⊢ (x.rotateRight m).getMsbD n =
    (decide (n < w + 1) &&
      if n < m % (w + 1) then x.getMsbD ((w + 1 + n - m % (w + 1)) % (w + 1)) else x.getMsbD (n - m % (w + 1)))

Tactic:
by_cases h₀ : m < w

Result:
case pos
n m w : Nat
x : BitVec (w + 1)
h₀ : m < w
⊢ (x.rotateRight m).getMsbD n =
    (decide (n < w + 1) &&
      if n < m % (w + 1) then x.getMsbD ((w + 1 + n - m % (w + 1)) % (w + 1)) else x.getMsbD (n - m % (w + 1)))

case neg
n m w : Nat
x : BitVec (w + 1)
h₀ : ¬m < w
⊢ (x.rotateRight m).getMsbD n =
    (decide (n < w + 1) &&
      if n < m % (w + 1) then x.getMsbD ((w + 1 + n - m % (w + 1)) % (w + 1)) else x.getMsbD (n - m % (w + 1)))

Proof state:
case a
n m w : Nat
x : BitVec (w + 1)
h₀ : ¬m < w
⊢ w + 1 > 0

Tactic:
simp

Result:
no goals

Proof state:
case neg
n m w : Nat
x : BitVec (w + 1)
h₀ : ¬m < w
⊢ (x.rotateRight m).getMsbD n =
    (decide (n < w + 1) &&
      if n < m % (w + 1) then x.getMsbD ((w + 1 + n - m % (w + 1)) % (w + 1)) else x.getMsbD (n - m % (w + 1)))

Tactic:
rw [← rotateRight_mod_eq_rotateRight, getMsbD_rotateRight_of_lt (by apply Nat.mod_lt; simp)]

Result:
case neg
n m w : Nat
x : BitVec (w + 1)
h₀ : ¬m < w
⊢ (decide (n < w + 1) &&
      if n < m % (w + 1) % (w + 1) then x.getMsbD ((w + 1 + n - m % (w + 1) % (w + 1)) % (w + 1))
      else x.getMsbD (n - m % (w + 1) % (w + 1))) =
    (decide (n < w + 1) &&
      if n < m % (w + 1) then x.getMsbD ((w + 1 + n - m % (w + 1)) % (w + 1)) else x.getMsbD (n - m % (w + 1)))

Proof state:
n m w : Nat
x : BitVec (w + 1)
h₀ : ¬m < w
⊢ m % (w + 1) < w + 1

Tactic:
apply Nat.mod_lt

Result:
case a
n m w : Nat
x : BitVec (w + 1)
h₀ : ¬m < w
⊢ w + 1 > 0

Proof state:
case zero
n m : Nat
x : BitVec 0
⊢ (x.rotateRight m).getMsbD n =
    (decide (n < 0) && if n < m % 0 then x.getMsbD ((0 + n - m % 0) % 0) else x.getMsbD (n - m % 0))

Tactic:
simp

Result:
no goals

Proof state:
w n m : Nat
x : BitVec w
⊢ (x.rotateRight m).getMsbD n =
    (decide (n < w) && if n < m % w then x.getMsbD ((w + n - m % w) % w) else x.getMsbD (n - m % w))

Tactic:
rcases w with rfl | w

Result:
case zero
n m : Nat
x : BitVec 0
⊢ (x.rotateRight m).getMsbD n =
    (decide (n < 0) && if n < m % 0 then x.getMsbD ((0 + n - m % 0) % 0) else x.getMsbD (n - m % 0))

case succ
n m w : Nat
x : BitVec (w + 1)
⊢ (x.rotateRight m).getMsbD n =
    (decide (n < w + 1) &&
      if n < m % (w + 1) then x.getMsbD ((w + 1 + n - m % (w + 1)) % (w + 1)) else x.getMsbD (n - m % (w + 1)))