-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getMsbD_rotateRight_of_lt {w n m : Nat} {x : BitVec w} (hr : m < 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:
case neg
n m w : Nat
x : BitVec (w + 1)
hr : m < w + 1
h : ¬n < m
⊢ (x.rotateRightAux 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:
simp [h, getMsbD_rotateRightAux_of_ge <| Nat.ge_of_not_lt h]

Result:
case neg
n m w : Nat
x : BitVec (w + 1)
hr : m < w + 1
h : ¬n < m
⊢ (decide (n < w + 1) && x.getMsbD (n - m)) =
    (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)
hr : m < w + 1
h : n < m
⊢ w + 1 + n - m < w + 1

Tactic:
omega

Result:
no goals

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

Tactic:
rw [Nat.mod_eq_of_lt hr]

Result:
no goals

Proof state:
w n m : Nat
x : BitVec w
hr : m < 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
hr : m < 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)
hr : m < 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)))

Proof state:
case succ
n m w : Nat
x : BitVec (w + 1)
hr : m < 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:
rw [rotateRight_eq_rotateRightAux_of_lt (by omega)]

Result:
case succ
n m w : Nat
x : BitVec (w + 1)
hr : m < w + 1
⊢ (x.rotateRightAux 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 pos
n m w : Nat
x : BitVec (w + 1)
hr : m < w + 1
h : n < m
⊢ (x.rotateRightAux 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:
simp only [getMsbD_rotateRightAux_of_lt h, show n < w + 1 by omega, decide_true,
  show m % (w + 1) = m by rw [Nat.mod_eq_of_lt hr], h, ↓reduceIte,
  show (w + 1 + n - m) < (w + 1) by omega, Nat.mod_eq_of_lt, Bool.true_and]

Result:
case pos
n m w : Nat
x : BitVec (w + 1)
hr : m < w + 1
h : n < m
⊢ x.getMsbD (n + (w + 1 - m)) = x.getMsbD (w + 1 + n - m)

Proof state:
case succ
n m w : Nat
x : BitVec (w + 1)
hr : m < w + 1
⊢ (x.rotateRightAux 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 : n < m

Result:
case pos
n m w : Nat
x : BitVec (w + 1)
hr : m < w + 1
h : n < m
⊢ (x.rotateRightAux 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)
hr : m < w + 1
h : ¬n < m
⊢ (x.rotateRightAux 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 pos
n m w : Nat
x : BitVec (w + 1)
hr : m < w + 1
h : ¬n < m
h₁ : n < w + 1
⊢ (decide (n < w + 1) && x.getMsbD (n - m)) =
    (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 [h, h₁, decide_true, Bool.true_and, Nat.mod_eq_of_lt hr]

Result:
no goals

Proof state:
case neg
n m w : Nat
x : BitVec (w + 1)
hr : m < w + 1
h : ¬n < m
h₁ : ¬n < w + 1
⊢ (decide (n < w + 1) && x.getMsbD (n - m)) =
    (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 [h₁]

Result:
no goals

Proof state:
case zero
n m : Nat
x : BitVec 0
hr : m < 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:
n m w : Nat
x : BitVec (w + 1)
hr : m < w + 1
⊢ m < w + 1

Tactic:
omega

Result:
no goals

Proof state:
case pos
n m w : Nat
x : BitVec (w + 1)
hr : m < w + 1
h : n < m
⊢ x.getMsbD (n + (w + 1 - m)) = x.getMsbD (w + 1 + n - m)

Tactic:
congr 1

Result:
case pos.e_i
n m w : Nat
x : BitVec (w + 1)
hr : m < w + 1
h : n < m
⊢ n + (w + 1 - m) = w + 1 + n - m

Proof state:
case pos.e_i
n m w : Nat
x : BitVec (w + 1)
hr : m < w + 1
h : n < m
⊢ n + (w + 1 - m) = w + 1 + n - m

Tactic:
omega

Result:
no goals

Proof state:
case neg
n m w : Nat
x : BitVec (w + 1)
hr : m < w + 1
h : ¬n < m
⊢ (decide (n < w + 1) && x.getMsbD (n - m)) =
    (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₁ : n < w + 1

Result:
case pos
n m w : Nat
x : BitVec (w + 1)
hr : m < w + 1
h : ¬n < m
h₁ : n < w + 1
⊢ (decide (n < w + 1) && x.getMsbD (n - m)) =
    (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)
hr : m < w + 1
h : ¬n < m
h₁ : ¬n < w + 1
⊢ (decide (n < w + 1) && x.getMsbD (n - m)) =
    (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)
hr : m < w + 1
h : n < m
⊢ n < w + 1

Tactic:
omega

Result:
no goals