-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem getMsbD_neg {i : Nat} {x : BitVec w} :
    getMsbD (-x) i =
      (getMsbD x i ^^ decide (∃ j < w, i < j ∧ getMsbD x j = true))

Proof state:
w i : Nat
x : BitVec w
⊢ (-x).getMsbD i = (x.getMsbD i ^^ decide (∃ j, j < w ∧ i < j ∧ x.getMsbD j = true))

Tactic:
simp only [getMsbD, getLsbD_neg, Bool.decide_and, Bool.and_eq_true, decide_eq_true_eq]

Result:
w i : Nat
x : BitVec w
⊢ (decide (i < w) &&
      (x.getLsbD (w - 1 - i) ^^ decide (w - 1 - i < w) && decide (∃ j, j < w - 1 - i ∧ x.getLsbD j = true))) =
    (decide (i < w) && x.getLsbD (w - 1 - i) ^^ decide (∃ j, j < w ∧ i < j ∧ j < w ∧ x.getLsbD (w - 1 - j) = true))

Proof state:
case mp
w i : Nat
x : BitVec w
hi : i < w
h₁ : w - 1 - i < w
⊢ (∃ j, j < w - 1 - i ∧ x.getLsbD j = true) → ∃ j, j < w ∧ i < j ∧ j < w ∧ x.getLsbD (w - 1 - j) = true

Tactic:
rintro ⟨j, hj, h⟩

Result:
case mp.intro.intro
w i : Nat
x : BitVec w
hi : i < w
h₁ : w - 1 - i < w
j : Nat
hj : j < w - 1 - i
h : x.getLsbD j = true
⊢ ∃ j, j < w ∧ i < j ∧ j < w ∧ x.getLsbD (w - 1 - j) = true

Proof state:
w i : Nat
x : BitVec w
hi : i < w
h₁ : w - 1 - i < w
⊢ (∃ j, j < w - 1 - i ∧ x.getLsbD j = true) ↔ ∃ j, j < w ∧ i < j ∧ j < w ∧ x.getLsbD (w - 1 - j) = true

Tactic:
constructor

Result:
case mp
w i : Nat
x : BitVec w
hi : i < w
h₁ : w - 1 - i < w
⊢ (∃ j, j < w - 1 - i ∧ x.getLsbD j = true) → ∃ j, j < w ∧ i < j ∧ j < w ∧ x.getLsbD (w - 1 - j) = true

case mpr
w i : Nat
x : BitVec w
hi : i < w
h₁ : w - 1 - i < w
⊢ (∃ j, j < w ∧ i < j ∧ j < w ∧ x.getLsbD (w - 1 - j) = true) → ∃ j, j < w - 1 - i ∧ x.getLsbD j = true

Proof state:
case mpr
w i : Nat
x : BitVec w
hi : i < w
h₁ : w - 1 - i < w
⊢ (∃ j, j < w ∧ i < j ∧ j < w ∧ x.getLsbD (w - 1 - j) = true) → ∃ j, j < w - 1 - i ∧ x.getLsbD j = true

Tactic:
rintro ⟨j, hj₁, hj₂, -, h⟩

Result:
case mpr.intro.intro.intro.intro
w i : Nat
x : BitVec w
hi : i < w
h₁ : w - 1 - i < w
j : Nat
hj₁ : j < w
hj₂ : i < j
h : x.getLsbD (w - 1 - j) = true
⊢ ∃ j, j < w - 1 - i ∧ x.getLsbD j = true

Proof state:
case mp.intro.intro
w i : Nat
x : BitVec w
hi : i < w
h₁ : w - 1 - i < w
j : Nat
hj : j < w - 1 - i
h : x.getLsbD j = true
⊢ (x.getLsbD j = true) = (x.getLsbD (w - 1 - (w - 1 - j)) = true)

Tactic:
congr

Result:
case mp.intro.intro.e_a.e_i
w i : Nat
x : BitVec w
hi : i < w
h₁ : w - 1 - i < w
j : Nat
hj : j < w - 1 - i
h : x.getLsbD j = true
⊢ j = w - 1 - (w - 1 - j)

Proof state:
w i : Nat
x : BitVec w
hi : i < w
⊢ (decide (i < w) &&
      (x.getLsbD (w - 1 - i) ^^ decide (w - 1 - i < w) && decide (∃ j, j < w - 1 - i ∧ x.getLsbD j = true))) =
    (decide (i < w) && x.getLsbD (w - 1 - i) ^^ decide (∃ j, j < w ∧ i < j ∧ j < w ∧ x.getLsbD (w - 1 - j) = true))

Tactic:
have h₁ : w - 1 - i < w := by omega

Result:
w i : Nat
x : BitVec w
hi : i < w
h₁ : w - 1 - i < w
⊢ (decide (i < w) &&
      (x.getLsbD (w - 1 - i) ^^ decide (w - 1 - i < w) && decide (∃ j, j < w - 1 - i ∧ x.getLsbD j = true))) =
    (decide (i < w) && x.getLsbD (w - 1 - i) ^^ decide (∃ j, j < w ∧ i < j ∧ j < w ∧ x.getLsbD (w - 1 - j) = true))

Proof state:
w i : Nat
x : BitVec w
hi : i < w
⊢ w - 1 - i < w

Tactic:
omega

Result:
no goals

Proof state:
w i : Nat
x : BitVec w
hi : i < w
h₁ : w - 1 - i < w
j : Nat
hj₁ : j < w
hj₂ : i < j
h : x.getLsbD (w - 1 - j) = true
⊢ w - 1 - j < w - 1 - i

Tactic:
omega

Result:
no goals

Proof state:
w i : Nat
x : BitVec w
hi : i < w
h₁ : w - 1 - i < w
j : Nat
hj : j < w - 1 - i
h : x.getLsbD j = true
⊢ i < w - 1 - j

Tactic:
omega

Result:
no goals

Proof state:
case mp.intro.intro.e_a.e_i
w i : Nat
x : BitVec w
hi : i < w
h₁ : w - 1 - i < w
j : Nat
hj : j < w - 1 - i
h : x.getLsbD j = true
⊢ j = w - 1 - (w - 1 - j)

Tactic:
omega

Result:
no goals

Proof state:
w i : Nat
x : BitVec w
⊢ (decide (i < w) &&
      (x.getLsbD (w - 1 - i) ^^ decide (w - 1 - i < w) && decide (∃ j, j < w - 1 - i ∧ x.getLsbD j = true))) =
    (decide (i < w) && x.getLsbD (w - 1 - i) ^^ decide (∃ j, j < w ∧ i < j ∧ j < w ∧ x.getLsbD (w - 1 - j) = true))

Tactic:
by_cases hi : i < w

Result:
case pos
w i : Nat
x : BitVec w
hi : i < w
⊢ (decide (i < w) &&
      (x.getLsbD (w - 1 - i) ^^ decide (w - 1 - i < w) && decide (∃ j, j < w - 1 - i ∧ x.getLsbD j = true))) =
    (decide (i < w) && x.getLsbD (w - 1 - i) ^^ decide (∃ j, j < w ∧ i < j ∧ j < w ∧ x.getLsbD (w - 1 - j) = true))

case neg
w i : Nat
x : BitVec w
hi : ¬i < w
⊢ (decide (i < w) &&
      (x.getLsbD (w - 1 - i) ^^ decide (w - 1 - i < w) && decide (∃ j, j < w - 1 - i ∧ x.getLsbD j = true))) =
    (decide (i < w) && x.getLsbD (w - 1 - i) ^^ decide (∃ j, j < w ∧ i < j ∧ j < w ∧ x.getLsbD (w - 1 - j) = true))

Proof state:
w i : Nat
x : BitVec w
hi : ¬i < w
⊢ ∀ (x_1 : Nat), x_1 < w → i < x_1 → x_1 < w → x.getLsbD (w - 1 - x_1) = false

Tactic:
omega

Result:
no goals

Proof state:
w i : Nat
x : BitVec w
hi : i < w
h₁ : w - 1 - i < w
j : Nat
hj : j < w - 1 - i
h : x.getLsbD j = true
⊢ w - 1 - j < w

Tactic:
omega

Result:
no goals

Proof state:
case mp.intro.intro
w i : Nat
x : BitVec w
hi : i < w
h₁ : w - 1 - i < w
j : Nat
hj : j < w - 1 - i
h : x.getLsbD j = true
⊢ ∃ j, j < w ∧ i < j ∧ j < w ∧ x.getLsbD (w - 1 - j) = true

Tactic:
refine ⟨w - 1 - j, by omega, by omega, by omega, _root_.cast ?_ h⟩

Result:
case mp.intro.intro
w i : Nat
x : BitVec w
hi : i < w
h₁ : w - 1 - i < w
j : Nat
hj : j < w - 1 - i
h : x.getLsbD j = true
⊢ (x.getLsbD j = true) = (x.getLsbD (w - 1 - (w - 1 - j)) = true)

Proof state:
w i : Nat
x : BitVec w
hi : i < w
h₁ : w - 1 - i < w
⊢ (decide (i < w) &&
      (x.getLsbD (w - 1 - i) ^^ decide (w - 1 - i < w) && decide (∃ j, j < w - 1 - i ∧ x.getLsbD j = true))) =
    (decide (i < w) && x.getLsbD (w - 1 - i) ^^ decide (∃ j, j < w ∧ i < j ∧ j < w ∧ x.getLsbD (w - 1 - j) = true))

Tactic:
simp only [hi, decide_true, h₁, Bool.true_and, Bool.bne_right_inj, decide_eq_decide]

Result:
w i : Nat
x : BitVec w
hi : i < w
h₁ : w - 1 - i < w
⊢ (∃ j, j < w - 1 - i ∧ x.getLsbD j = true) ↔ ∃ j, j < w ∧ i < j ∧ j < w ∧ x.getLsbD (w - 1 - j) = true

Proof state:
case mpr.intro.intro.intro.intro
w i : Nat
x : BitVec w
hi : i < w
h₁ : w - 1 - i < w
j : Nat
hj₁ : j < w
hj₂ : i < j
h : x.getLsbD (w - 1 - j) = true
⊢ ∃ j, j < w - 1 - i ∧ x.getLsbD j = true

Tactic:
exact ⟨w - 1 - j, by omega, h⟩

Result:
no goals

Proof state:
case pos
w i : Nat
x : BitVec w
hi : i < w
⊢ (decide (i < w) &&
      (x.getLsbD (w - 1 - i) ^^ decide (w - 1 - i < w) && decide (∃ j, j < w - 1 - i ∧ x.getLsbD j = true))) =
    (decide (i < w) && x.getLsbD (w - 1 - i) ^^ decide (∃ j, j < w ∧ i < j ∧ j < w ∧ x.getLsbD (w - 1 - j) = true))

case neg
w i : Nat
x : BitVec w
hi : ¬i < w
⊢ (decide (i < w) &&
      (x.getLsbD (w - 1 - i) ^^ decide (w - 1 - i < w) && decide (∃ j, j < w - 1 - i ∧ x.getLsbD j = true))) =
    (decide (i < w) && x.getLsbD (w - 1 - i) ^^ decide (∃ j, j < w ∧ i < j ∧ j < w ∧ x.getLsbD (w - 1 - j) = true))

Tactic:
case neg =>
  simp [hi]; omega

Result:
case pos
w i : Nat
x : BitVec w
hi : i < w
⊢ (decide (i < w) &&
      (x.getLsbD (w - 1 - i) ^^ decide (w - 1 - i < w) && decide (∃ j, j < w - 1 - i ∧ x.getLsbD j = true))) =
    (decide (i < w) && x.getLsbD (w - 1 - i) ^^ decide (∃ j, j < w ∧ i < j ∧ j < w ∧ x.getLsbD (w - 1 - j) = true))

Proof state:
w i : Nat
x : BitVec w
hi : ¬i < w
⊢ (decide (i < w) &&
      (x.getLsbD (w - 1 - i) ^^ decide (w - 1 - i < w) && decide (∃ j, j < w - 1 - i ∧ x.getLsbD j = true))) =
    (decide (i < w) && x.getLsbD (w - 1 - i) ^^ decide (∃ j, j < w ∧ i < j ∧ j < w ∧ x.getLsbD (w - 1 - j) = true))

Tactic:
simp [hi]

Result:
w i : Nat
x : BitVec w
hi : ¬i < w
⊢ ∀ (x_1 : Nat), x_1 < w → i < x_1 → x_1 < w → x.getLsbD (w - 1 - x_1) = false