-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem ushiftRightRec_eq (x : BitVec w₁) (y : BitVec w₂) (n : Nat) :
    ushiftRightRec x y n = x >>> (y.setWidth (n + 1)).setWidth w₂

Proof state:
case pos
w₁ w₂ n : Nat
ih : ∀ (x : BitVec w₁) (y : BitVec w₂), x.ushiftRightRec y n = x >>> setWidth w₂ (setWidth (n + 1) y)
x : BitVec w₁
y : BitVec w₂
h : y.getLsbD (n + 1) = true
⊢ setWidth w₂ (setWidth (n + 1) y) &&& twoPow w₂ (n + 1) = 0#w₂

Tactic:
simp [and_twoPow]

Result:
no goals

Proof state:
w₁ w₂ n : Nat
ih : ∀ (x : BitVec w₁) (y : BitVec w₂), x.ushiftRightRec y n = x >>> setWidth w₂ (setWidth (n + 1) y)
x : BitVec w₁
y : BitVec w₂
⊢ (x >>> setWidth w₂ (setWidth (n + 1) y) >>> if y.getLsbD (n + 1) = true then twoPow w₂ (n + 1) else 0#w₂) =
    x >>> setWidth w₂ (setWidth (n + 1 + 1) y)

Tactic:
by_cases h : y.getLsbD (n + 1) <;> simp only [h, ↓reduceIte]

Result:
case pos
w₁ w₂ n : Nat
ih : ∀ (x : BitVec w₁) (y : BitVec w₂), x.ushiftRightRec y n = x >>> setWidth w₂ (setWidth (n + 1) y)
x : BitVec w₁
y : BitVec w₂
h : y.getLsbD (n + 1) = true
⊢ x >>> setWidth w₂ (setWidth (n + 1) y) >>> twoPow w₂ (n + 1) = x >>> setWidth w₂ (setWidth (n + 1 + 1) y)

case neg
w₁ w₂ n : Nat
ih : ∀ (x : BitVec w₁) (y : BitVec w₂), x.ushiftRightRec y n = x >>> setWidth w₂ (setWidth (n + 1) y)
x : BitVec w₁
y : BitVec w₂
h : ¬y.getLsbD (n + 1) = true
⊢ (x >>> setWidth w₂ (setWidth (n + 1) y) >>> if false = true then twoPow w₂ (n + 1) else 0#w₂) =
    x >>> setWidth w₂ (setWidth (n + 1 + 1) y)

Proof state:
w₁ w₂ : Nat
x : BitVec w₁
y : BitVec w₂
⊢ x.ushiftRightRec y 0 = x >>> setWidth w₂ (setWidth (0 + 1) y)

Tactic:
ext i

Result:
case pred
w₁ w₂ : Nat
x : BitVec w₁
y : BitVec w₂
i : Nat
a✝ : i < w₁
⊢ (x.ushiftRightRec y 0).getLsbD i = (x >>> setWidth w₂ (setWidth (0 + 1) y)).getLsbD i

Proof state:
case pos
w₁ w₂ n : Nat
ih : ∀ (x : BitVec w₁) (y : BitVec w₂), x.ushiftRightRec y n = x >>> setWidth w₂ (setWidth (n + 1) y)
x : BitVec w₁
y : BitVec w₂
h : y.getLsbD (n + 1) = true
⊢ x >>> setWidth w₂ (setWidth (n + 1) y) >>> twoPow w₂ (n + 1) = x >>> setWidth w₂ (setWidth (n + 1 + 1) y)

Tactic:
rw [setWidth_setWidth_succ_eq_setWidth_setWidth_or_twoPow_of_getLsbD_true h,
  ushiftRight'_or_of_and_eq_zero]

Result:
case pos
w₁ w₂ n : Nat
ih : ∀ (x : BitVec w₁) (y : BitVec w₂), x.ushiftRightRec y n = x >>> setWidth w₂ (setWidth (n + 1) y)
x : BitVec w₁
y : BitVec w₂
h : y.getLsbD (n + 1) = true
⊢ setWidth w₂ (setWidth (n + 1) y) &&& twoPow w₂ (n + 1) = 0#w₂

Proof state:
case pred
w₁ w₂ : Nat
x : BitVec w₁
y : BitVec w₂
i : Nat
a✝ : i < w₁
⊢ (x.ushiftRightRec y 0).getLsbD i = (x >>> setWidth w₂ (setWidth (0 + 1) y)).getLsbD i

Tactic:
simp only [ushiftRightRec_zero, twoPow_zero, Nat.reduceAdd,
  and_one_eq_setWidth_ofBool_getLsbD, setWidth_one]

Result:
no goals

Proof state:
case zero
w₁ w₂ : Nat
x : BitVec w₁
y : BitVec w₂
⊢ x.ushiftRightRec y 0 = x >>> setWidth w₂ (setWidth (0 + 1) y)

case succ
w₁ w₂ n✝ : Nat
a✝ : ∀ (x : BitVec w₁) (y : BitVec w₂), x.ushiftRightRec y n✝ = x >>> setWidth w₂ (setWidth (n✝ + 1) y)
x : BitVec w₁
y : BitVec w₂
⊢ x.ushiftRightRec y (n✝ + 1) = x >>> setWidth w₂ (setWidth (n✝ + 1 + 1) y)

Tactic:
case zero =>
  ext i
  simp only [ushiftRightRec_zero, twoPow_zero, Nat.reduceAdd,
    and_one_eq_setWidth_ofBool_getLsbD, setWidth_one]

Result:
case succ
w₁ w₂ n✝ : Nat
a✝ : ∀ (x : BitVec w₁) (y : BitVec w₂), x.ushiftRightRec y n✝ = x >>> setWidth w₂ (setWidth (n✝ + 1) y)
x : BitVec w₁
y : BitVec w₂
⊢ x.ushiftRightRec y (n✝ + 1) = x >>> setWidth w₂ (setWidth (n✝ + 1 + 1) y)

Proof state:
case neg
w₁ w₂ n : Nat
ih : ∀ (x : BitVec w₁) (y : BitVec w₂), x.ushiftRightRec y n = x >>> setWidth w₂ (setWidth (n + 1) y)
x : BitVec w₁
y : BitVec w₂
h : ¬y.getLsbD (n + 1) = true
⊢ (x >>> setWidth w₂ (setWidth (n + 1) y) >>> if false = true then twoPow w₂ (n + 1) else 0#w₂) =
    x >>> setWidth w₂ (setWidth (n + 1 + 1) y)

Tactic:
simp [setWidth_setWidth_succ_eq_setWidth_setWidth_of_getLsbD_false, h]

Result:
no goals

Proof state:
w₁ w₂ : Nat
x : BitVec w₁
y : BitVec w₂
n : Nat
⊢ x.ushiftRightRec y n = x >>> setWidth w₂ (setWidth (n + 1) y)

Tactic:
induction n generalizing x y

Result:
case zero
w₁ w₂ : Nat
x : BitVec w₁
y : BitVec w₂
⊢ x.ushiftRightRec y 0 = x >>> setWidth w₂ (setWidth (0 + 1) y)

case succ
w₁ w₂ n✝ : Nat
a✝ : ∀ (x : BitVec w₁) (y : BitVec w₂), x.ushiftRightRec y n✝ = x >>> setWidth w₂ (setWidth (n✝ + 1) y)
x : BitVec w₁
y : BitVec w₂
⊢ x.ushiftRightRec y (n✝ + 1) = x >>> setWidth w₂ (setWidth (n✝ + 1 + 1) y)

Proof state:
w₁ w₂ n : Nat
ih : ∀ (x : BitVec w₁) (y : BitVec w₂), x.ushiftRightRec y n = x >>> setWidth w₂ (setWidth (n + 1) y)
x : BitVec w₁
y : BitVec w₂
⊢ x.ushiftRightRec y (n + 1) = x >>> setWidth w₂ (setWidth (n + 1 + 1) y)

Tactic:
simp only [ushiftRightRec_succ, and_twoPow]

Result:
w₁ w₂ n : Nat
ih : ∀ (x : BitVec w₁) (y : BitVec w₂), x.ushiftRightRec y n = x >>> setWidth w₂ (setWidth (n + 1) y)
x : BitVec w₁
y : BitVec w₂
⊢ (x.ushiftRightRec y n >>> if y.getLsbD (n + 1) = true then twoPow w₂ (n + 1) else 0#w₂) =
    x >>> setWidth w₂ (setWidth (n + 1 + 1) y)

Proof state:
w₁ w₂ n : Nat
ih : ∀ (x : BitVec w₁) (y : BitVec w₂), x.ushiftRightRec y n = x >>> setWidth w₂ (setWidth (n + 1) y)
x : BitVec w₁
y : BitVec w₂
⊢ (x.ushiftRightRec y n >>> if y.getLsbD (n + 1) = true then twoPow w₂ (n + 1) else 0#w₂) =
    x >>> setWidth w₂ (setWidth (n + 1 + 1) y)

Tactic:
rw [ih]

Result:
w₁ w₂ n : Nat
ih : ∀ (x : BitVec w₁) (y : BitVec w₂), x.ushiftRightRec y n = x >>> setWidth w₂ (setWidth (n + 1) y)
x : BitVec w₁
y : BitVec w₂
⊢ (x >>> setWidth w₂ (setWidth (n + 1) y) >>> if y.getLsbD (n + 1) = true then twoPow w₂ (n + 1) else 0#w₂) =
    x >>> setWidth w₂ (setWidth (n + 1 + 1) y)