-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem msb_neg {w : Nat} {x : BitVec w} :
    (-x).msb = ((x != 0#w && x != intMin w) ^^ x.msb)

Proof state:
case pred
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : ¬x = 0#w
w_pos : 0 < w
getMsbD_x : ∀ (x_1 : Nat), x_1 < w → 0 < x_1 → x.getMsbD x_1 = false
hmsb : x.msb = true
i : Nat
hi : i < w
⊢ x.getMsbD i = decide (i = 0)

Tactic:
cases i

Result:
case pred.zero
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : ¬x = 0#w
w_pos : 0 < w
getMsbD_x : ∀ (x_1 : Nat), x_1 < w → 0 < x_1 → x.getMsbD x_1 = false
hmsb : x.msb = true
hi : 0 < w
⊢ x.getMsbD 0 = decide (0 = 0)

case pred.succ
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : ¬x = 0#w
w_pos : 0 < w
getMsbD_x : ∀ (x_1 : Nat), x_1 < w → 0 < x_1 → x.getMsbD x_1 = false
hmsb : x.msb = true
n✝ : Nat
hi : n✝ + 1 < w
⊢ x.getMsbD (n✝ + 1) = decide (n✝ + 1 = 0)

Proof state:
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : ¬x = 0#w
w_pos : 0 < w
this : ∃ j, j < w ∧ 0 < j ∧ x.getMsbD j = true
⊢ (x.getMsbD 0 ^^ decide (∃ j, j < w ∧ 0 < j ∧ x.getMsbD j = true)) = (x != 0#w && x != intMin w ^^ x.getMsbD 0)

Tactic:
simp [show x != 0#w by simpa, show x != intMin w by simpa, this]

Result:
no goals

Proof state:
case pos
w : Nat
x : BitVec w
hmin : x = intMin w
⊢ (x.getMsbD 0 ^^ decide (∃ j, j < w ∧ 0 < j ∧ x.getMsbD j = true)) = (x != 0#w && x != intMin w ^^ x.getMsbD 0)

case neg
w : Nat
x : BitVec w
hmin : ¬x = intMin w
⊢ (x.getMsbD 0 ^^ decide (∃ j, j < w ∧ 0 < j ∧ x.getMsbD j = true)) = (x != 0#w && x != intMin w ^^ x.getMsbD 0)

Tactic:
case pos =>
  have : (∃ j, j < w ∧ 0 < j ∧ 0 < w ∧ j = 0) ↔ False := by
    simp; omega
  simp [hmin, getMsbD_intMin, this]

Result:
case neg
w : Nat
x : BitVec w
hmin : ¬x = intMin w
⊢ (x.getMsbD 0 ^^ decide (∃ j, j < w ∧ 0 < j ∧ x.getMsbD j = true)) = (x != 0#w && x != intMin w ^^ x.getMsbD 0)

Proof state:
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : ¬x = 0#w
w_pos : 0 < w
getMsbD_x : ∀ (x_1 : Nat), x_1 < w → 0 < x_1 → x.getMsbD x_1 = false
hmsb : x.msb = true
n✝ : Nat
hi : n✝ + 1 < w
⊢ 0 < n✝ + 1

Tactic:
omega

Result:
no goals

Proof state:
case h.false
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : ¬x = 0#w
w_pos : 0 < w
getMsbD_x : ∀ (x_1 : Nat), x_1 < w → 0 < x_1 → x.getMsbD x_1 = false
hmsb : x.msb = false
⊢ False

Tactic:
case false =>
  apply hzero
  apply eq_of_getMsbD_eq
  intro i hi
  simp only [getMsbD_zero]
  cases i
  case zero => exact hmsb
  case succ => exact getMsbD_x _ hi (by omega)

Result:
no goals

Proof state:
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : ¬x = 0#w
⊢ 0 < w

Tactic:
cases w

Result:
case zero
x : BitVec 0
hmin : ¬x = intMin 0
hzero : ¬x = 0#0
⊢ 0 < 0

case succ
n✝ : Nat
x : BitVec (n✝ + 1)
hmin : ¬x = intMin (n✝ + 1)
hzero : ¬x = 0#(n✝ + 1)
⊢ 0 < n✝ + 1

Proof state:
case pos
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : x = 0#w
⊢ (x.getMsbD 0 ^^ decide (∃ j, j < w ∧ 0 < j ∧ x.getMsbD j = true)) = (x != 0#w && x != intMin w ^^ x.getMsbD 0)

case neg
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : ¬x = 0#w
⊢ (x.getMsbD 0 ^^ decide (∃ j, j < w ∧ 0 < j ∧ x.getMsbD j = true)) = (x != 0#w && x != intMin w ^^ x.getMsbD 0)

Tactic:
case pos => simp [hzero]

Result:
case neg
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : ¬x = 0#w
⊢ (x.getMsbD 0 ^^ decide (∃ j, j < w ∧ 0 < j ∧ x.getMsbD j = true)) = (x != 0#w && x != intMin w ^^ x.getMsbD 0)

Proof state:
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : ¬x = 0#w
w_pos : 0 < w
getMsbD_x : ∀ (x_1 : Nat), x_1 < w → 0 < x_1 → x.getMsbD x_1 = false
hmsb : x.msb = false
n✝ : Nat
hi : n✝ + 1 < w
⊢ 0 < n✝ + 1

Tactic:
omega

Result:
no goals

Proof state:
case zero
x : BitVec 0
hmin : ¬x = intMin 0
hzero : ¬x = 0#0
⊢ 0 < 0

Tactic:
rw [@of_length_zero x] at hzero

Result:
case zero
x : BitVec 0
hmin : ¬x = intMin 0
hzero : ¬0#0 = 0#0
⊢ 0 < 0

Proof state:
case h.false
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : ¬x = 0#w
w_pos : 0 < w
getMsbD_x : ∀ (x_1 : Nat), x_1 < w → 0 < x_1 → x.getMsbD x_1 = false
hmsb : x.msb = false
⊢ False

case h.true
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : ¬x = 0#w
w_pos : 0 < w
getMsbD_x : ∀ (x_1 : Nat), x_1 < w → 0 < x_1 → x.getMsbD x_1 = false
hmsb : x.msb = true
⊢ False

Tactic:
case true =>
  apply hmin
  apply eq_of_getMsbD_eq
  intro i hi
  simp only [getMsbD_intMin, w_pos, decide_true, Bool.true_and]
  cases i
  case zero => exact hmsb
  case succ => exact getMsbD_x _ hi (by omega)

Result:
case h.false
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : ¬x = 0#w
w_pos : 0 < w
getMsbD_x : ∀ (x_1 : Nat), x_1 < w → 0 < x_1 → x.getMsbD x_1 = false
hmsb : x.msb = false
⊢ False

Proof state:
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : ¬x = 0#w
w_pos : 0 < w
getMsbD_x : ∀ (x_1 : Nat), x_1 < w → 0 < x_1 → x.getMsbD x_1 = false
hmsb : x.msb = false
hi : 0 < w
⊢ x.getMsbD 0 = false

Tactic:
exact hmsb

Result:
no goals

Proof state:
w : Nat
x : BitVec w
hmin : x = intMin w
⊢ (∃ j, j < w ∧ 0 < j ∧ 0 < w ∧ j = 0) ↔ False

Tactic:
simp

Result:
w : Nat
x : BitVec w
hmin : x = intMin w
⊢ ∀ (x : Nat), x < w → 0 < x → 0 < w → ¬x = 0

Proof state:
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : ¬x = 0#w
w_pos : 0 < w
getMsbD_x : ∀ (x_1 : Nat), x_1 < w → 0 < x_1 → x.getMsbD x_1 = false
hmsb : x.msb = false
n✝ : Nat
hi : n✝ + 1 < w
⊢ x.getMsbD (n✝ + 1) = false

Tactic:
exact getMsbD_x _ hi (by omega)

Result:
no goals

Proof state:
w : Nat
x : BitVec w
hmin : ¬x = intMin w
⊢ (x.getMsbD 0 ^^ decide (∃ j, j < w ∧ 0 < j ∧ x.getMsbD j = true)) = (x != 0#w && x != intMin w ^^ x.getMsbD 0)

Tactic:
by_cases hzero : x = 0#w

Result:
case pos
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : x = 0#w
⊢ (x.getMsbD 0 ^^ decide (∃ j, j < w ∧ 0 < j ∧ x.getMsbD j = true)) = (x != 0#w && x != intMin w ^^ x.getMsbD 0)

case neg
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : ¬x = 0#w
⊢ (x.getMsbD 0 ^^ decide (∃ j, j < w ∧ 0 < j ∧ x.getMsbD j = true)) = (x != 0#w && x != intMin w ^^ x.getMsbD 0)

Proof state:
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : ¬x = 0#w
w_pos : 0 < w
⊢ ∃ j, j < w ∧ 0 < j ∧ x.getMsbD j = true

Tactic:
false_or_by_contra

Result:
case h
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : ¬x = 0#w
w_pos : 0 < w
a✝ : ¬∃ j, j < w ∧ 0 < j ∧ x.getMsbD j = true
⊢ False

Proof state:
case pred
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : ¬x = 0#w
w_pos : 0 < w
getMsbD_x : ∀ (x_1 : Nat), x_1 < w → 0 < x_1 → x.getMsbD x_1 = false
hmsb : x.msb = false
⊢ ∀ (i : Nat), i < w → x.getMsbD i = (0#w).getMsbD i

Tactic:
intro i hi

Result:
case pred
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : ¬x = 0#w
w_pos : 0 < w
getMsbD_x : ∀ (x_1 : Nat), x_1 < w → 0 < x_1 → x.getMsbD x_1 = false
hmsb : x.msb = false
i : Nat
hi : i < w
⊢ x.getMsbD i = (0#w).getMsbD i

Proof state:
case pred.zero
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : ¬x = 0#w
w_pos : 0 < w
getMsbD_x : ∀ (x_1 : Nat), x_1 < w → 0 < x_1 → x.getMsbD x_1 = false
hmsb : x.msb = true
hi : 0 < w
⊢ x.getMsbD 0 = decide (0 = 0)

case pred.succ
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : ¬x = 0#w
w_pos : 0 < w
getMsbD_x : ∀ (x_1 : Nat), x_1 < w → 0 < x_1 → x.getMsbD x_1 = false
hmsb : x.msb = true
n✝ : Nat
hi : n✝ + 1 < w
⊢ x.getMsbD (n✝ + 1) = decide (n✝ + 1 = 0)

Tactic:
case zero => exact hmsb

Result:
case pred.succ
w : Nat
x : BitVec w
hmin : ¬x = intMin w
hzero : ¬x = 0#w
w_pos : 0 < w
getMsbD_x : ∀ (x_1 : Nat), x_1 < w → 0 < x_1 → x.getMsbD x_1 = false
hmsb : x.msb = true
n✝ : Nat
hi : n✝ + 1 < w
⊢ x.getMsbD (n✝ + 1) = decide (n✝ + 1 = 0)