-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem shiftLeftRec_eq {x : BitVec w₁} {y : BitVec w₂} {n : Nat} :
    shiftLeftRec x y n = x <<< (y.setWidth (n + 1)).setWidth w₂

Proof state:
w₁ w₂ : Nat
x : BitVec w₁
y : BitVec w₂
⊢ x.shiftLeftRec 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.shiftLeftRec y 0).getLsbD i = (x <<< setWidth w₂ (setWidth (0 + 1) y)).getLsbD i

Proof state:
w₁ w₂ n : Nat
ih : ∀ {x : BitVec w₁} {y : BitVec w₂}, x.shiftLeftRec 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)

Result:
case pos
w₁ w₂ n : Nat
ih : ∀ {x : BitVec w₁} {y : BitVec w₂}, x.shiftLeftRec 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 y.getLsbD (n + 1) = true then twoPow w₂ (n + 1) else 0#w₂) =
    x <<< setWidth w₂ (setWidth (n + 1 + 1) y)

case neg
w₁ w₂ n : Nat
ih : ∀ {x : BitVec w₁} {y : BitVec w₂}, x.shiftLeftRec 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 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₂ : Nat
x : BitVec w₁
y : BitVec w₂
n : Nat
⊢ x.shiftLeftRec 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.shiftLeftRec y 0 = x <<< setWidth w₂ (setWidth (0 + 1) y)

case succ
w₁ w₂ n✝ : Nat
a✝ : ∀ {x : BitVec w₁} {y : BitVec w₂}, x.shiftLeftRec y n✝ = x <<< setWidth w₂ (setWidth (n✝ + 1) y)
x : BitVec w₁
y : BitVec w₂
⊢ x.shiftLeftRec y (n✝ + 1) = x <<< setWidth w₂ (setWidth (n✝ + 1 + 1) y)

Proof state:
case pos
w₁ w₂ n : Nat
ih : ∀ {x : BitVec w₁} {y : BitVec w₂}, x.shiftLeftRec 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,
  shiftLeft_or_of_and_eq_zero]

Result:
case pos
w₁ w₂ n : Nat
ih : ∀ {x : BitVec w₁} {y : BitVec w₂}, x.shiftLeftRec 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:
w₁ w₂ n : Nat
ih : ∀ {x : BitVec w₁} {y : BitVec w₂}, x.shiftLeftRec y n = x <<< setWidth w₂ (setWidth (n + 1) y)
x : BitVec w₁
y : BitVec w₂
⊢ (x.shiftLeftRec 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.shiftLeftRec 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)

Proof state:
case neg
w₁ w₂ n : Nat
ih : ∀ {x : BitVec w₁} {y : BitVec w₂}, x.shiftLeftRec 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) = x <<< setWidth w₂ (setWidth (n + 1 + 1) y)

Tactic:
rw [setWidth_setWidth_succ_eq_setWidth_setWidth_of_getLsbD_false (i := n + 1)]

Result:
case neg
w₁ w₂ n : Nat
ih : ∀ {x : BitVec w₁} {y : BitVec w₂}, x.shiftLeftRec y n = x <<< setWidth w₂ (setWidth (n + 1) y)
x : BitVec w₁
y : BitVec w₂
h : ¬y.getLsbD (n + 1) = true
⊢ y.getLsbD (n + 1) = false

Proof state:
w₁ w₂ n : Nat
ih : ∀ {x : BitVec w₁} {y : BitVec w₂}, x.shiftLeftRec y n = x <<< setWidth w₂ (setWidth (n + 1) y)
x : BitVec w₁
y : BitVec w₂
⊢ x.shiftLeftRec y (n + 1) = x <<< setWidth w₂ (setWidth (n + 1 + 1) y)

Tactic:
simp only [shiftLeftRec_succ, and_twoPow]

Result:
w₁ w₂ n : Nat
ih : ∀ {x : BitVec w₁} {y : BitVec w₂}, x.shiftLeftRec y n = x <<< setWidth w₂ (setWidth (n + 1) y)
x : BitVec w₁
y : BitVec w₂
⊢ (x.shiftLeftRec 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:
case pos
w₁ w₂ n : Nat
ih : ∀ {x : BitVec w₁} {y : BitVec w₂}, x.shiftLeftRec 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:
case zero
w₁ w₂ : Nat
x : BitVec w₁
y : BitVec w₂
⊢ x.shiftLeftRec y 0 = x <<< setWidth w₂ (setWidth (0 + 1) y)

case succ
w₁ w₂ n✝ : Nat
a✝ : ∀ {x : BitVec w₁} {y : BitVec w₂}, x.shiftLeftRec y n✝ = x <<< setWidth w₂ (setWidth (n✝ + 1) y)
x : BitVec w₁
y : BitVec w₂
⊢ x.shiftLeftRec y (n✝ + 1) = x <<< setWidth w₂ (setWidth (n✝ + 1 + 1) y)

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

Result:
case succ
w₁ w₂ n✝ : Nat
a✝ : ∀ {x : BitVec w₁} {y : BitVec w₂}, x.shiftLeftRec y n✝ = x <<< setWidth w₂ (setWidth (n✝ + 1) y)
x : BitVec w₁
y : BitVec w₂
⊢ x.shiftLeftRec 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.shiftLeftRec 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 y.getLsbD (n + 1) = true then twoPow w₂ (n + 1) else 0#w₂) =
    x <<< setWidth w₂ (setWidth (n + 1 + 1) y)

Tactic:
simp only [h, false_eq_true, ↓reduceIte, shiftLeft_zero']

Result:
case neg
w₁ w₂ n : Nat
ih : ∀ {x : BitVec w₁} {y : BitVec w₂}, x.shiftLeftRec 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) = x <<< setWidth w₂ (setWidth (n + 1 + 1) y)

Proof state:
case neg
w₁ w₂ n : Nat
ih : ∀ {x : BitVec w₁} {y : BitVec w₂}, x.shiftLeftRec y n = x <<< setWidth w₂ (setWidth (n + 1) y)
x : BitVec w₁
y : BitVec w₂
h : ¬y.getLsbD (n + 1) = true
⊢ y.getLsbD (n + 1) = false

Tactic:
simp [h]

Result:
no goals

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

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

Result:
no goals

Proof state:
case pos
w₁ w₂ n : Nat
ih : ∀ {x : BitVec w₁} {y : BitVec w₂}, x.shiftLeftRec 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 y.getLsbD (n + 1) = true then twoPow w₂ (n + 1) else 0#w₂) =
    x <<< setWidth w₂ (setWidth (n + 1 + 1) y)

Tactic:
simp only [h, ↓reduceIte]

Result:
case pos
w₁ w₂ n : Nat
ih : ∀ {x : BitVec w₁} {y : BitVec w₂}, x.shiftLeftRec 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)