-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem mulRec_eq_mul_signExtend_setWidth (x y : BitVec w) (s : Nat) :
    mulRec x y s = x * ((y.setWidth (s + 1)).setWidth w)

Proof state:
w : Nat
x y : BitVec w
hy : ¬y.getLsbD 0 = true
⊢ (if y.getLsbD 0 = true then x else 0#w) = x * setWidth w (setWidth 1 y)

Tactic:
simp [hy, setWidth_one_eq_ofBool_getLsb_zero]

Result:
no goals

Proof state:
w : Nat
x y : BitVec w
hy : y.getLsbD 0 = true
⊢ x = x * 1#w

Tactic:
simp

Result:
no goals

Proof state:
w : Nat
x y : BitVec w
hy : y.getLsbD 0 = true
⊢ 0 < 1

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x y : BitVec w
s' : Nat
hs : x.mulRec y s' = x * setWidth w (setWidth (s' + 1) y)
⊢ (if y.getLsbD (s' + 1) = true then x <<< (s' + 1) else 0#w) =
    x * if y.getLsbD (s' + 1) = true then twoPow w (s' + 1) else 0#w

Tactic:
by_cases hy : y.getLsbD (s' + 1) <;> simp [hy]

Result:
no goals

Proof state:
w : Nat
x y : BitVec w
s' : Nat
hs : x.mulRec y s' = x * setWidth w (setWidth (s' + 1) y)
⊢ (x * setWidth w (setWidth (s' + 1) y) + if y.getLsbD (s' + 1) = true then x <<< (s' + 1) else 0) =
    x * setWidth w (setWidth (s' + 1 + 1) y)

Tactic:
have heq :
  (if y.getLsbD (s' + 1) = true then x <<< (s' + 1) else 0) =
    (x * (y &&& (BitVec.twoPow w (s' + 1)))) := by
  simp only [ofNat_eq_ofNat, and_twoPow]
  by_cases hy : y.getLsbD (s' + 1) <;> simp [hy]

Result:
w : Nat
x y : BitVec w
s' : Nat
hs : x.mulRec y s' = x * setWidth w (setWidth (s' + 1) y)
heq : (if y.getLsbD (s' + 1) = true then x <<< (s' + 1) else 0) = x * (y &&& twoPow w (s' + 1))
⊢ (x * setWidth w (setWidth (s' + 1) y) + if y.getLsbD (s' + 1) = true then x <<< (s' + 1) else 0) =
    x * setWidth w (setWidth (s' + 1 + 1) y)

Proof state:
w : Nat
x y : BitVec w
s' : Nat
hs : x.mulRec y s' = x * setWidth w (setWidth (s' + 1) y)
heq : (if y.getLsbD (s' + 1) = true then x <<< (s' + 1) else 0) = x * (y &&& twoPow w (s' + 1))
⊢ (x * setWidth w (setWidth (s' + 1) y) + if y.getLsbD (s' + 1) = true then x <<< (s' + 1) else 0) =
    x * setWidth w (setWidth (s' + 1 + 1) y)

Tactic:
rw [heq, ← BitVec.mul_add, ← setWidth_setWidth_succ_eq_setWidth_setWidth_add_twoPow]

Result:
no goals

Proof state:
case succ
w : Nat
x y : BitVec w
n✝ : Nat
a✝ : x.mulRec y n✝ = x * setWidth w (setWidth (n✝ + 1) y)
⊢ x.mulRec y (n✝ + 1) = x * setWidth w (setWidth (n✝ + 1 + 1) y)

Tactic:
case succ s' hs =>
  rw [mulRec_succ_eq, hs]
  have heq :
    (if y.getLsbD (s' + 1) = true then x <<< (s' + 1) else 0) =
      (x * (y &&& (BitVec.twoPow w (s' + 1)))) := by
    simp only [ofNat_eq_ofNat, and_twoPow]
    by_cases hy : y.getLsbD (s' + 1) <;> simp [hy]
  rw [heq, ← BitVec.mul_add, ← setWidth_setWidth_succ_eq_setWidth_setWidth_add_twoPow]

Result:
no goals

Proof state:
w : Nat
x y : BitVec w
hy : y.getLsbD 0 = true
⊢ (if y.getLsbD 0 = true then x else 0#w) = x * setWidth w (setWidth 1 y)

Tactic:
simp only [hy, ↓reduceIte, setWidth_one_eq_ofBool_getLsb_zero,
  ofBool_true, ofNat_eq_ofNat]

Result:
w : Nat
x y : BitVec w
hy : y.getLsbD 0 = true
⊢ x = x * setWidth w 1#1

Proof state:
case pos
w : Nat
x y : BitVec w
h✝ : y.getLsbD 0 = true
⊢ (if y.getLsbD 0 = true then x else 0#w) = x * setWidth w (setWidth 1 y)

case neg
w : Nat
x y : BitVec w
h✝ : ¬y.getLsbD 0 = true
⊢ (if y.getLsbD 0 = true then x else 0#w) = x * setWidth w (setWidth 1 y)

Tactic:
case pos hy =>
  simp only [hy, ↓reduceIte, setWidth_one_eq_ofBool_getLsb_zero,
    ofBool_true, ofNat_eq_ofNat]
  rw [setWidth_ofNat_one_eq_ofNat_one_of_lt (by omega)]
  simp

Result:
case neg
w : Nat
x y : BitVec w
h✝ : ¬y.getLsbD 0 = true
⊢ (if y.getLsbD 0 = true then x else 0#w) = x * setWidth w (setWidth 1 y)

Proof state:
w : Nat
x y : BitVec w
s' : Nat
hs : x.mulRec y s' = x * setWidth w (setWidth (s' + 1) y)
⊢ x.mulRec y (s' + 1) = x * setWidth w (setWidth (s' + 1 + 1) y)

Tactic:
rw [mulRec_succ_eq, hs]

Result:
w : Nat
x y : BitVec w
s' : Nat
hs : x.mulRec y s' = x * setWidth w (setWidth (s' + 1) y)
⊢ (x * setWidth w (setWidth (s' + 1) y) + if y.getLsbD (s' + 1) = true then x <<< (s' + 1) else 0) =
    x * setWidth w (setWidth (s' + 1 + 1) y)

Proof state:
w : Nat
x y : BitVec w
hy : y.getLsbD 0 = true
⊢ x = x * setWidth w 1#1

Tactic:
rw [setWidth_ofNat_one_eq_ofNat_one_of_lt (by omega)]

Result:
w : Nat
x y : BitVec w
hy : y.getLsbD 0 = true
⊢ x = x * 1#w

Proof state:
w : Nat
x y : BitVec w
s : Nat
⊢ x.mulRec y s = x * setWidth w (setWidth (s + 1) y)

Tactic:
induction s

Result:
case zero
w : Nat
x y : BitVec w
⊢ x.mulRec y 0 = x * setWidth w (setWidth (0 + 1) y)

case succ
w : Nat
x y : BitVec w
n✝ : Nat
a✝ : x.mulRec y n✝ = x * setWidth w (setWidth (n✝ + 1) y)
⊢ x.mulRec y (n✝ + 1) = x * setWidth w (setWidth (n✝ + 1 + 1) y)

Proof state:
w : Nat
x y : BitVec w
s' : Nat
hs : x.mulRec y s' = x * setWidth w (setWidth (s' + 1) y)
⊢ (if y.getLsbD (s' + 1) = true then x <<< (s' + 1) else 0) = x * (y &&& twoPow w (s' + 1))

Tactic:
simp only [ofNat_eq_ofNat, and_twoPow]

Result:
w : Nat
x y : BitVec w
s' : Nat
hs : x.mulRec y s' = x * setWidth w (setWidth (s' + 1) y)
⊢ (if y.getLsbD (s' + 1) = true then x <<< (s' + 1) else 0#w) =
    x * if y.getLsbD (s' + 1) = true then twoPow w (s' + 1) else 0#w

Proof state:
w : Nat
x y : BitVec w
⊢ x.mulRec y 0 = x * setWidth w (setWidth (0 + 1) y)

Tactic:
simp only [mulRec_zero_eq, ofNat_eq_ofNat, Nat.reduceAdd]

Result:
w : Nat
x y : BitVec w
⊢ (if y.getLsbD 0 = true then x else 0#w) = x * setWidth w (setWidth 1 y)

Proof state:
case neg
w : Nat
x y : BitVec w
h✝ : ¬y.getLsbD 0 = true
⊢ (if y.getLsbD 0 = true then x else 0#w) = x * setWidth w (setWidth 1 y)

Tactic:
case neg hy =>
  simp [hy, setWidth_one_eq_ofBool_getLsb_zero]

Result:
no goals

Proof state:
case zero
w : Nat
x y : BitVec w
⊢ x.mulRec y 0 = x * setWidth w (setWidth (0 + 1) y)

case succ
w : Nat
x y : BitVec w
n✝ : Nat
a✝ : x.mulRec y n✝ = x * setWidth w (setWidth (n✝ + 1) y)
⊢ x.mulRec y (n✝ + 1) = x * setWidth w (setWidth (n✝ + 1 + 1) y)

Tactic:
case zero =>
  simp only [mulRec_zero_eq, ofNat_eq_ofNat, Nat.reduceAdd]
  by_cases y.getLsbD 0
  case pos hy =>
    simp only [hy, ↓reduceIte, setWidth_one_eq_ofBool_getLsb_zero,
      ofBool_true, ofNat_eq_ofNat]
    rw [setWidth_ofNat_one_eq_ofNat_one_of_lt (by omega)]
    simp
  case neg hy =>
    simp [hy, setWidth_one_eq_ofBool_getLsb_zero]

Result:
case succ
w : Nat
x y : BitVec w
n✝ : Nat
a✝ : x.mulRec y n✝ = x * setWidth w (setWidth (n✝ + 1) y)
⊢ x.mulRec y (n✝ + 1) = x * setWidth w (setWidth (n✝ + 1 + 1) y)

Proof state:
w : Nat
x y : BitVec w
⊢ (if y.getLsbD 0 = true then x else 0#w) = x * setWidth w (setWidth 1 y)

Tactic:
by_cases y.getLsbD 0

Result:
case pos
w : Nat
x y : BitVec w
h✝ : y.getLsbD 0 = true
⊢ (if y.getLsbD 0 = true then x else 0#w) = x * setWidth w (setWidth 1 y)

case neg
w : Nat
x y : BitVec w
h✝ : ¬y.getLsbD 0 = true
⊢ (if y.getLsbD 0 = true then x else 0#w) = x * setWidth w (setWidth 1 y)