-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getMsbD_rotateLeft_of_lt {n w : Nat} {x : BitVec w} (hi : r < w):
    (x.rotateLeft r).getMsbD n = (decide (n < w) && x.getMsbD ((r + n) % w))

Proof state:
r n w : Nat
x : BitVec (w + 1)
hi : r < w + 1
⊢ r < w + 1

Tactic:
omega

Result:
no goals

Proof state:
case pos
r n w : Nat
x : BitVec (w + 1)
hi : r < w + 1
h : n < w + 1 - r
⊢ (x.rotateLeftAux r).getMsbD n = (decide (n < w + 1) && x.getMsbD ((r + n) % (w + 1)))

Tactic:
simp [getMsbD_rotateLeftAux_of_lt h, Nat.mod_eq_of_lt, show r + n < (w + 1) by omega, show n < w + 1 by omega]

Result:
no goals

Proof state:
case pos
r n w : Nat
x : BitVec (w + 1)
hi : r < w + 1
h : ¬n < w + 1 - r
h₁ : n < w + 1
h₂ : r + n < 2 * (w + 1)
⊢ x.getMsbD (n - (w + 1 - r)) = x.getMsbD ((r + n) % (w + 1))

Tactic:
congr 1

Result:
case pos.e_i
r n w : Nat
x : BitVec (w + 1)
hi : r < w + 1
h : ¬n < w + 1 - r
h₁ : n < w + 1
h₂ : r + n < 2 * (w + 1)
⊢ n - (w + 1 - r) = (r + n) % (w + 1)

Proof state:
r n w : Nat
x : BitVec (w + 1)
hi : r < w + 1
h : ¬n < w + 1 - r
h₁ : n < w + 1
h₂ : r + n < 2 * (w + 1)
⊢ r + n < (w + 1) * (1 + 1)

Tactic:
omega

Result:
no goals

Proof state:
case neg
r n w : Nat
x : BitVec (w + 1)
hi : r < w + 1
h : ¬n < w + 1 - r
⊢ (decide (n < w + 1) && x.getMsbD (n - (w + 1 - r))) = (decide (n < w + 1) && x.getMsbD ((r + n) % (w + 1)))

Tactic:
by_cases h₁ : n < w + 1

Result:
case pos
r n w : Nat
x : BitVec (w + 1)
hi : r < w + 1
h : ¬n < w + 1 - r
h₁ : n < w + 1
⊢ (decide (n < w + 1) && x.getMsbD (n - (w + 1 - r))) = (decide (n < w + 1) && x.getMsbD ((r + n) % (w + 1)))

case neg
r n w : Nat
x : BitVec (w + 1)
hi : r < w + 1
h : ¬n < w + 1 - r
h₁ : ¬n < w + 1
⊢ (decide (n < w + 1) && x.getMsbD (n - (w + 1 - r))) = (decide (n < w + 1) && x.getMsbD ((r + n) % (w + 1)))

Proof state:
r n w : Nat
x : BitVec (w + 1)
hi : r < w + 1
h : ¬n < w + 1 - r
h₁ : n < w + 1
⊢ r + n < 2 * (w + 1)

Tactic:
omega

Result:
no goals

Proof state:
case pos
r n w : Nat
x : BitVec (w + 1)
hi : r < w + 1
h : ¬n < w + 1 - r
h₁ : n < w + 1
⊢ (decide (n < w + 1) && x.getMsbD (n - (w + 1 - r))) = (decide (n < w + 1) && x.getMsbD ((r + n) % (w + 1)))

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

Result:
case pos
r n w : Nat
x : BitVec (w + 1)
hi : r < w + 1
h : ¬n < w + 1 - r
h₁ : n < w + 1
⊢ x.getMsbD (n - (w + 1 - r)) = x.getMsbD ((r + n) % (w + 1))

Proof state:
case pos.e_i
r n w : Nat
x : BitVec (w + 1)
hi : r < w + 1
h : ¬n < w + 1 - r
h₁ : n < w + 1
h₂ : r + n < 2 * (w + 1)
⊢ n - (w + 1 - r) = (r + n) % (w + 1)

Tactic:
rw [← Nat.sub_mul_eq_mod_of_lt_of_le (n := 1) (by omega) (by omega)]

Result:
case pos.e_i
r n w : Nat
x : BitVec (w + 1)
hi : r < w + 1
h : ¬n < w + 1 - r
h₁ : n < w + 1
h₂ : r + n < 2 * (w + 1)
⊢ n - (w + 1 - r) = r + n - (w + 1) * 1

Proof state:
r n w : Nat
x : BitVec (w + 1)
hi : r < w + 1
h : n < w + 1 - r
⊢ r + n < w + 1

Tactic:
omega

Result:
no goals

Proof state:
case succ
r n w : Nat
x : BitVec (w + 1)
hi : r < w + 1
⊢ (x.rotateLeftAux r).getMsbD n = (decide (n < w + 1) && x.getMsbD ((r + n) % (w + 1)))

Tactic:
by_cases h : n < (w + 1) - r

Result:
case pos
r n w : Nat
x : BitVec (w + 1)
hi : r < w + 1
h : n < w + 1 - r
⊢ (x.rotateLeftAux r).getMsbD n = (decide (n < w + 1) && x.getMsbD ((r + n) % (w + 1)))

case neg
r n w : Nat
x : BitVec (w + 1)
hi : r < w + 1
h : ¬n < w + 1 - r
⊢ (x.rotateLeftAux r).getMsbD n = (decide (n < w + 1) && x.getMsbD ((r + n) % (w + 1)))

Proof state:
case pos
r n w : Nat
x : BitVec (w + 1)
hi : r < w + 1
h : ¬n < w + 1 - r
h₁ : n < w + 1
⊢ x.getMsbD (n - (w + 1 - r)) = x.getMsbD ((r + n) % (w + 1))

Tactic:
have h₂ : (r + n) < 2 * (w + 1) := by omega

Result:
case pos
r n w : Nat
x : BitVec (w + 1)
hi : r < w + 1
h : ¬n < w + 1 - r
h₁ : n < w + 1
h₂ : r + n < 2 * (w + 1)
⊢ x.getMsbD (n - (w + 1 - r)) = x.getMsbD ((r + n) % (w + 1))

Proof state:
case zero
r n : Nat
x : BitVec 0
hi : r < 0
⊢ (x.rotateLeft r).getMsbD n = (decide (n < 0) && x.getMsbD ((r + n) % 0))

Tactic:
simp

Result:
no goals

Proof state:
case succ
r n w : Nat
x : BitVec (w + 1)
hi : r < w + 1
⊢ (x.rotateLeft r).getMsbD n = (decide (n < w + 1) && x.getMsbD ((r + n) % (w + 1)))

Tactic:
rw [BitVec.rotateLeft_eq_rotateLeftAux_of_lt (by omega)]

Result:
case succ
r n w : Nat
x : BitVec (w + 1)
hi : r < w + 1
⊢ (x.rotateLeftAux r).getMsbD n = (decide (n < w + 1) && x.getMsbD ((r + n) % (w + 1)))

Proof state:
case pos.e_i
r n w : Nat
x : BitVec (w + 1)
hi : r < w + 1
h : ¬n < w + 1 - r
h₁ : n < w + 1
h₂ : r + n < 2 * (w + 1)
⊢ n - (w + 1 - r) = r + n - (w + 1) * 1

Tactic:
omega

Result:
no goals

Proof state:
r n w : Nat
x : BitVec (w + 1)
hi : r < w + 1
h : n < w + 1 - r
⊢ n < w + 1

Tactic:
omega

Result:
no goals

Proof state:
case neg
r n w : Nat
x : BitVec (w + 1)
hi : r < w + 1
h : ¬n < w + 1 - r
h₁ : ¬n < w + 1
⊢ (decide (n < w + 1) && x.getMsbD (n - (w + 1 - r))) = (decide (n < w + 1) && x.getMsbD ((r + n) % (w + 1)))

Tactic:
simp [h₁]

Result:
no goals

Proof state:
r n w : Nat
x : BitVec (w + 1)
hi : r < w + 1
h : ¬n < w + 1 - r
h₁ : n < w + 1
h₂ : r + n < 2 * (w + 1)
⊢ (w + 1) * 1 ≤ r + n

Tactic:
omega

Result:
no goals

Proof state:
r n w : Nat
x : BitVec w
hi : r < w
⊢ (x.rotateLeft r).getMsbD n = (decide (n < w) && x.getMsbD ((r + n) % w))

Tactic:
rcases w with rfl | w

Result:
case zero
r n : Nat
x : BitVec 0
hi : r < 0
⊢ (x.rotateLeft r).getMsbD n = (decide (n < 0) && x.getMsbD ((r + n) % 0))

case succ
r n w : Nat
x : BitVec (w + 1)
hi : r < w + 1
⊢ (x.rotateLeft r).getMsbD n = (decide (n < w + 1) && x.getMsbD ((r + n) % (w + 1)))

Proof state:
case neg
r n w : Nat
x : BitVec (w + 1)
hi : r < w + 1
h : ¬n < w + 1 - r
⊢ (x.rotateLeftAux r).getMsbD n = (decide (n < w + 1) && x.getMsbD ((r + n) % (w + 1)))

Tactic:
simp [getMsbD_rotateLeftAux_of_ge <| Nat.ge_of_not_lt h]

Result:
case neg
r n w : Nat
x : BitVec (w + 1)
hi : r < w + 1
h : ¬n < w + 1 - r
⊢ (decide (n < w + 1) && x.getMsbD (n - (w + 1 - r))) = (decide (n < w + 1) && x.getMsbD ((r + n) % (w + 1)))