-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem shiftLeft_ushiftRight {x : BitVec w} {n : Nat}:
    x >>> n <<< n = x &&& BitVec.allOnes w <<< n

Proof state:
case neg
w n : Nat
ih : ∀ {x : BitVec w}, x >>> n <<< n = x &&& allOnes w <<< n
x : BitVec w
i : Nat
h : i < w
hw : ¬w = 0
⊢ (x >>> 1 <<< 1 &&& allOnes w <<< n <<< 1).getLsbD i = (x &&& allOnes w <<< n <<< 1).getLsbD i

Tactic:
by_cases hi₂ : i = 0

Result:
case pos
w n : Nat
ih : ∀ {x : BitVec w}, x >>> n <<< n = x &&& allOnes w <<< n
x : BitVec w
i : Nat
h : i < w
hw : ¬w = 0
hi₂ : i = 0
⊢ (x >>> 1 <<< 1 &&& allOnes w <<< n <<< 1).getLsbD i = (x &&& allOnes w <<< n <<< 1).getLsbD i

case neg
w n : Nat
ih : ∀ {x : BitVec w}, x >>> n <<< n = x &&& allOnes w <<< n
x : BitVec w
i : Nat
h : i < w
hw : ¬w = 0
hi₂ : ¬i = 0
⊢ (x >>> 1 <<< 1 &&& allOnes w <<< n <<< 1).getLsbD i = (x &&& allOnes w <<< n <<< 1).getLsbD i

Proof state:
case neg
w n : Nat
ih : ∀ {x : BitVec w}, x >>> n <<< n = x &&& allOnes w <<< n
x : BitVec w
i : Nat
h : i < w
hw : ¬w = 0
hi₂ : ¬i = 0
⊢ (x >>> 1 <<< 1 &&& allOnes w <<< n <<< 1).getLsbD i = (x &&& allOnes w <<< n <<< 1).getLsbD i

Tactic:
simp [Nat.lt_one_iff, hi₂, h, show 1 + (i - 1) = i by omega]

Result:
no goals

Proof state:
w n : Nat
ih : ∀ {x : BitVec w}, x >>> n <<< n = x &&& allOnes w <<< n
x : BitVec w
⊢ x >>> (n + 1) <<< (n + 1) = x &&& allOnes w <<< (n + 1)

Tactic:
rw [BitVec.shiftLeft_add, Nat.add_comm, BitVec.shiftRight_add, ih,
   Nat.add_comm, BitVec.shiftLeft_add, BitVec.shiftLeft_and_distrib]

Result:
w n : Nat
ih : ∀ {x : BitVec w}, x >>> n <<< n = x &&& allOnes w <<< n
x : BitVec w
⊢ x >>> 1 <<< 1 &&& allOnes w <<< n <<< 1 = x &&& allOnes w <<< n <<< 1

Proof state:
w n : Nat
ih : ∀ {x : BitVec w}, x >>> n <<< n = x &&& allOnes w <<< n
x : BitVec w
⊢ x >>> 1 <<< 1 &&& allOnes w <<< n <<< 1 = x &&& allOnes w <<< n <<< 1

Tactic:
ext i h

Result:
case pred
w n : Nat
ih : ∀ {x : BitVec w}, x >>> n <<< n = x &&& allOnes w <<< n
x : BitVec w
i : Nat
h : i < w
⊢ (x >>> 1 <<< 1 &&& allOnes w <<< n <<< 1).getLsbD i = (x &&& allOnes w <<< n <<< 1).getLsbD i

Proof state:
case pos
w n : Nat
ih : ∀ {x : BitVec w}, x >>> n <<< n = x &&& allOnes w <<< n
x : BitVec w
i : Nat
h : i < w
hw : w = 0
⊢ (x >>> 1 <<< 1 &&& allOnes w <<< n <<< 1).getLsbD i = (x &&& allOnes w <<< n <<< 1).getLsbD i

Tactic:
simp [hw]

Result:
no goals

Proof state:
w : Nat
x : BitVec w
⊢ x >>> 0 <<< 0 = x &&& allOnes w <<< 0

Tactic:
ext

Result:
case pred
w : Nat
x : BitVec w
i✝ : Nat
a✝ : i✝ < w
⊢ (x >>> 0 <<< 0).getLsbD i✝ = (x &&& allOnes w <<< 0).getLsbD i✝

Proof state:
case zero
w : Nat
x : BitVec w
⊢ x >>> 0 <<< 0 = x &&& allOnes w <<< 0

case succ
w n✝ : Nat
a✝ : ∀ {x : BitVec w}, x >>> n✝ <<< n✝ = x &&& allOnes w <<< n✝
x : BitVec w
⊢ x >>> (n✝ + 1) <<< (n✝ + 1) = x &&& allOnes w <<< (n✝ + 1)

Tactic:
case zero =>
  ext; simp

Result:
case succ
w n✝ : Nat
a✝ : ∀ {x : BitVec w}, x >>> n✝ <<< n✝ = x &&& allOnes w <<< n✝
x : BitVec w
⊢ x >>> (n✝ + 1) <<< (n✝ + 1) = x &&& allOnes w <<< (n✝ + 1)

Proof state:
w : Nat
x : BitVec w
n : Nat
⊢ x >>> n <<< n = x &&& allOnes w <<< n

Tactic:
induction n generalizing x

Result:
case zero
w : Nat
x : BitVec w
⊢ x >>> 0 <<< 0 = x &&& allOnes w <<< 0

case succ
w n✝ : Nat
a✝ : ∀ {x : BitVec w}, x >>> n✝ <<< n✝ = x &&& allOnes w <<< n✝
x : BitVec w
⊢ x >>> (n✝ + 1) <<< (n✝ + 1) = x &&& allOnes w <<< (n✝ + 1)

Proof state:
case pos
w n : Nat
ih : ∀ {x : BitVec w}, x >>> n <<< n = x &&& allOnes w <<< n
x : BitVec w
i : Nat
h : i < w
hw : ¬w = 0
hi₂ : i = 0
⊢ (x >>> 1 <<< 1 &&& allOnes w <<< n <<< 1).getLsbD i = (x &&& allOnes w <<< n <<< 1).getLsbD i

Tactic:
simp [hi₂]

Result:
no goals

Proof state:
case pred
w : Nat
x : BitVec w
i✝ : Nat
a✝ : i✝ < w
⊢ (x >>> 0 <<< 0).getLsbD i✝ = (x &&& allOnes w <<< 0).getLsbD i✝

Tactic:
simp

Result:
no goals

Proof state:
case pred
w n : Nat
ih : ∀ {x : BitVec w}, x >>> n <<< n = x &&& allOnes w <<< n
x : BitVec w
i : Nat
h : i < w
⊢ (x >>> 1 <<< 1 &&& allOnes w <<< n <<< 1).getLsbD i = (x &&& allOnes w <<< n <<< 1).getLsbD i

Tactic:
by_cases hw : w = 0

Result:
case pos
w n : Nat
ih : ∀ {x : BitVec w}, x >>> n <<< n = x &&& allOnes w <<< n
x : BitVec w
i : Nat
h : i < w
hw : w = 0
⊢ (x >>> 1 <<< 1 &&& allOnes w <<< n <<< 1).getLsbD i = (x &&& allOnes w <<< n <<< 1).getLsbD i

case neg
w n : Nat
ih : ∀ {x : BitVec w}, x >>> n <<< n = x &&& allOnes w <<< n
x : BitVec w
i : Nat
h : i < w
hw : ¬w = 0
⊢ (x >>> 1 <<< 1 &&& allOnes w <<< n <<< 1).getLsbD i = (x &&& allOnes w <<< n <<< 1).getLsbD i

Proof state:
w n : Nat
ih : ∀ {x : BitVec w}, x >>> n <<< n = x &&& allOnes w <<< n
x : BitVec w
i : Nat
h : i < w
hw : ¬w = 0
hi₂ : ¬i = 0
⊢ 1 + (i - 1) = i

Tactic:
omega

Result:
no goals