-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem slt_zero_iff_msb_cond {x : BitVec w} : x.slt 0#w ↔ x.msb = true

Proof state:
case mpr
w : Nat
x : BitVec w
h : x.msb = true
this : x.toInt = ↑x.toNat - ↑(2 ^ w)
⊢ x.slt 0#w = true

Tactic:
simp [BitVec.slt, this]

Result:
case mpr
w : Nat
x : BitVec w
h : x.msb = true
this : x.toInt = ↑x.toNat - ↑(2 ^ w)
⊢ ↑x.toNat - ↑(2 ^ w) < 0

Proof state:
case mp.h
w : Nat
x : BitVec w
hmsb : x.msb = false
this : x.toInt = ↑x.toNat
h : x.toInt < 0
⊢ False

Tactic:
omega

Result:
no goals

Proof state:
case mpr
w : Nat
x : BitVec w
h : x.msb = true
this : x.toInt = ↑x.toNat - ↑(2 ^ w)
⊢ ↑x.toNat - ↑(2 ^ w) < 0

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x : BitVec w
this : x.toInt = if x.msb = true then ↑x.toNat - ↑(2 ^ w) else ↑x.toNat
⊢ x.slt 0#w = true ↔ x.msb = true

Tactic:
constructor

Result:
case mp
w : Nat
x : BitVec w
this : x.toInt = if x.msb = true then ↑x.toNat - ↑(2 ^ w) else ↑x.toNat
⊢ x.slt 0#w = true → x.msb = true

case mpr
w : Nat
x : BitVec w
this : x.toInt = if x.msb = true then ↑x.toNat - ↑(2 ^ w) else ↑x.toNat
⊢ x.msb = true → x.slt 0#w = true

Proof state:
case mp
w : Nat
x : BitVec w
this : x.toInt = if x.msb = true then ↑x.toNat - ↑(2 ^ w) else ↑x.toNat
⊢ x.slt 0#w = true → x.msb = true

Tactic:
intros h

Result:
case mp
w : Nat
x : BitVec w
this : x.toInt = if x.msb = true then ↑x.toNat - ↑(2 ^ w) else ↑x.toNat
h : x.slt 0#w = true
⊢ x.msb = true

Proof state:
case mp.h
w : Nat
x : BitVec w
this : x.toInt = if x.msb = true then ↑x.toNat - ↑(2 ^ w) else ↑x.toNat
h : x.slt 0#w = true
⊢ ¬x.msb = true → False

Tactic:
intros hmsb

Result:
case mp.h
w : Nat
x : BitVec w
this : x.toInt = if x.msb = true then ↑x.toNat - ↑(2 ^ w) else ↑x.toNat
h : x.slt 0#w = true
hmsb : ¬x.msb = true
⊢ False

Proof state:
case mp.h
w : Nat
x : BitVec w
h : x.slt 0#w = true
hmsb : x.msb = false
this : x.toInt = ↑x.toNat
⊢ False

Tactic:
simp only [BitVec.slt, toInt_zero, decide_eq_true_eq] at h

Result:
case mp.h
w : Nat
x : BitVec w
hmsb : x.msb = false
this : x.toInt = ↑x.toNat
h : x.toInt < 0
⊢ False

Proof state:
case mpr
w : Nat
x : BitVec w
this : x.toInt = if x.msb = true then ↑x.toNat - ↑(2 ^ w) else ↑x.toNat
⊢ x.msb = true → x.slt 0#w = true

Tactic:
intros h

Result:
case mpr
w : Nat
x : BitVec w
this : x.toInt = if x.msb = true then ↑x.toNat - ↑(2 ^ w) else ↑x.toNat
h : x.msb = true
⊢ x.slt 0#w = true

Proof state:
case mp.h
w : Nat
x : BitVec w
this : x.toInt = if x.msb = true then ↑x.toNat - ↑(2 ^ w) else ↑x.toNat
h : x.slt 0#w = true
hmsb : x.msb = false
⊢ False

Tactic:
simp only [hmsb, Bool.false_eq_true, ↓reduceIte] at this

Result:
case mp.h
w : Nat
x : BitVec w
h : x.slt 0#w = true
hmsb : x.msb = false
this : x.toInt = ↑x.toNat
⊢ False

Proof state:
case mp
w : Nat
x : BitVec w
this : x.toInt = if x.msb = true then ↑x.toNat - ↑(2 ^ w) else ↑x.toNat
h : x.slt 0#w = true
⊢ x.msb = true

Tactic:
apply Classical.byContradiction

Result:
case mp.h
w : Nat
x : BitVec w
this : x.toInt = if x.msb = true then ↑x.toNat - ↑(2 ^ w) else ↑x.toNat
h : x.slt 0#w = true
⊢ ¬x.msb = true → False

Proof state:
w : Nat
x : BitVec w
⊢ x.slt 0#w = true ↔ x.msb = true

Tactic:
have := toInt_eq_msb_cond x

Result:
w : Nat
x : BitVec w
this : x.toInt = if x.msb = true then ↑x.toNat - ↑(2 ^ w) else ↑x.toNat
⊢ x.slt 0#w = true ↔ x.msb = true

Proof state:
case mpr
w : Nat
x : BitVec w
this : x.toInt = if x.msb = true then ↑x.toNat - ↑(2 ^ w) else ↑x.toNat
h : x.msb = true
⊢ x.slt 0#w = true

Tactic:
simp only [h, ↓reduceIte] at this

Result:
case mpr
w : Nat
x : BitVec w
h : x.msb = true
this : x.toInt = ↑x.toNat - ↑(2 ^ w)
⊢ x.slt 0#w = true

Proof state:
case mp.h
w : Nat
x : BitVec w
this : x.toInt = if x.msb = true then ↑x.toNat - ↑(2 ^ w) else ↑x.toNat
h : x.slt 0#w = true
hmsb : ¬x.msb = true
⊢ False

Tactic:
simp only [Bool.not_eq_true] at hmsb

Result:
case mp.h
w : Nat
x : BitVec w
this : x.toInt = if x.msb = true then ↑x.toNat - ↑(2 ^ w) else ↑x.toNat
h : x.slt 0#w = true
hmsb : x.msb = false
⊢ False