-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toInt_signExtend_of_lt {x : BitVec w} (hv : w < v):
    (x.signExtend v).toInt = x.toInt

Proof state:
w v : Nat
x : BitVec w
hv : w < v
⊢ (if (signExtend v x).msb = true then ↑((setWidth v x).toNat + if x.msb = true then 2 ^ v - 2 ^ w else 0) - ↑(2 ^ v)
    else ↑((setWidth v x).toNat + if x.msb = true then 2 ^ v - 2 ^ w else 0)) =
    if x.msb = true then ↑x.toNat - ↑(2 ^ w) else ↑x.toNat

Tactic:
have : (x.signExtend v).msb = x.msb := by
  rw [msb_eq_getLsbD_last, getLsbD_eq_getElem (Nat.sub_one_lt_of_lt hv)]
  simp [getElem_signExtend, Nat.le_sub_one_of_lt hv]

Result:
w v : Nat
x : BitVec w
hv : w < v
this : (signExtend v x).msb = x.msb
⊢ (if (signExtend v x).msb = true then ↑((setWidth v x).toNat + if x.msb = true then 2 ^ v - 2 ^ w else 0) - ↑(2 ^ v)
    else ↑((setWidth v x).toNat + if x.msb = true then 2 ^ v - 2 ^ w else 0)) =
    if x.msb = true then ↑x.toNat - ↑(2 ^ w) else ↑x.toNat

Proof state:
w v : Nat
x : BitVec w
hv : w < v
⊢ (signExtend v x).msb = x.msb

Tactic:
rw [msb_eq_getLsbD_last, getLsbD_eq_getElem (Nat.sub_one_lt_of_lt hv)]

Result:
w v : Nat
x : BitVec w
hv : w < v
⊢ (signExtend v x)[v - 1] = x.msb

Proof state:
w v : Nat
x : BitVec w
hv : w < v
this : (signExtend v x).msb = x.msb
⊢ (if (signExtend v x).msb = true then ↑((setWidth v x).toNat + if x.msb = true then 2 ^ v - 2 ^ w else 0) - ↑(2 ^ v)
    else ↑((setWidth v x).toNat + if x.msb = true then 2 ^ v - 2 ^ w else 0)) =
    if x.msb = true then ↑x.toNat - ↑(2 ^ w) else ↑x.toNat

Tactic:
have H : 2^w ≤ 2^v := Nat.pow_le_pow_of_le_right (by omega) (by omega)

Result:
w v : Nat
x : BitVec w
hv : w < v
this : (signExtend v x).msb = x.msb
H : 2 ^ w ≤ 2 ^ v
⊢ (if (signExtend v x).msb = true then ↑((setWidth v x).toNat + if x.msb = true then 2 ^ v - 2 ^ w else 0) - ↑(2 ^ v)
    else ↑((setWidth v x).toNat + if x.msb = true then 2 ^ v - 2 ^ w else 0)) =
    if x.msb = true then ↑x.toNat - ↑(2 ^ w) else ↑x.toNat

Proof state:
case pos
w v : Nat
x : BitVec w
hv : w < v
this : (signExtend v x).msb = x.msb
H : 2 ^ w ≤ 2 ^ v
h : x.msb = true
⊢ ↑x.toNat + ↑(2 ^ v - 2 ^ w) - ↑(2 ^ v) = ↑x.toNat - ↑(2 ^ w)

Tactic:
omega

Result:
no goals

Proof state:
w v : Nat
x : BitVec w
hv : w < v
this : (signExtend v x).msb = x.msb
H : 2 ^ w ≤ 2 ^ v
⊢ (if (signExtend v x).msb = true then ↑((setWidth v x).toNat + if x.msb = true then 2 ^ v - 2 ^ w else 0) - ↑(2 ^ v)
    else ↑((setWidth v x).toNat + if x.msb = true then 2 ^ v - 2 ^ w else 0)) =
    if x.msb = true then ↑x.toNat - ↑(2 ^ w) else ↑x.toNat

Tactic:
simp only [this, toNat_setWidth, Int.natCast_add, Int.ofNat_emod, Int.natCast_mul]

Result:
w v : Nat
x : BitVec w
hv : w < v
this : (signExtend v x).msb = x.msb
H : 2 ^ w ≤ 2 ^ v
⊢ (if x.msb = true then ↑x.toNat % ↑(2 ^ v) + ↑(if x.msb = true then 2 ^ v - 2 ^ w else 0) - ↑(2 ^ v)
    else ↑x.toNat % ↑(2 ^ v) + ↑(if x.msb = true then 2 ^ v - 2 ^ w else 0)) =
    if x.msb = true then ↑x.toNat - ↑(2 ^ w) else ↑x.toNat

Proof state:
w v : Nat
x : BitVec w
hv : w < v
this : (signExtend v x).msb = x.msb
⊢ w ≤ v

Tactic:
omega

Result:
no goals

Proof state:
w v : Nat
x : BitVec w
hv : w < v
this : (signExtend v x).msb = x.msb
H : 2 ^ w ≤ 2 ^ v
⊢ (if x.msb = true then ↑x.toNat % ↑(2 ^ v) + ↑(if x.msb = true then 2 ^ v - 2 ^ w else 0) - ↑(2 ^ v)
    else ↑x.toNat % ↑(2 ^ v) + ↑(if x.msb = true then 2 ^ v - 2 ^ w else 0)) =
    if x.msb = true then ↑x.toNat - ↑(2 ^ w) else ↑x.toNat

Tactic:
by_cases h : x.msb
<;> norm_cast
<;> simp [h, Nat.mod_eq_of_lt (Nat.lt_of_lt_of_le x.isLt H)]

Result:
case pos
w v : Nat
x : BitVec w
hv : w < v
this : (signExtend v x).msb = x.msb
H : 2 ^ w ≤ 2 ^ v
h : x.msb = true
⊢ ↑x.toNat + ↑(2 ^ v - 2 ^ w) - ↑(2 ^ v) = ↑x.toNat - ↑(2 ^ w)

Proof state:
w v : Nat
x : BitVec w
hv : w < v
⊢ (signExtend v x).toInt = x.toInt

Tactic:
simp only [toInt_eq_msb_cond, toNat_signExtend]

Result:
w v : Nat
x : BitVec w
hv : w < v
⊢ (if (signExtend v x).msb = true then ↑((setWidth v x).toNat + if x.msb = true then 2 ^ v - 2 ^ w else 0) - ↑(2 ^ v)
    else ↑((setWidth v x).toNat + if x.msb = true then 2 ^ v - 2 ^ w else 0)) =
    if x.msb = true then ↑x.toNat - ↑(2 ^ w) else ↑x.toNat

Proof state:
w v : Nat
x : BitVec w
hv : w < v
this : (signExtend v x).msb = x.msb
⊢ 2 > 0

Tactic:
omega

Result:
no goals

Proof state:
w v : Nat
x : BitVec w
hv : w < v
⊢ (signExtend v x)[v - 1] = x.msb

Tactic:
simp [getElem_signExtend, Nat.le_sub_one_of_lt hv]

Result:
no goals