-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem ofInt_negSucc_eq_not_ofNat {w n : Nat} :
    BitVec.ofInt w (Int.negSucc n) = ~~~.ofNat w n

Proof state:
w n a✝ : Nat
h : ↑(2 ^ w) - 1 - ↑n % ↑(2 ^ w) = ↑a✝
⊢ a✝ = 2 ^ w - 1 - n % 2 ^ w

Tactic:
omega

Result:
no goals

Proof state:
w n a✝ : Nat
h : Int.negSucc n % ↑(2 ^ w) = Int.ofNat a✝
⊢ (match Int.ofNat a✝ with
    | Int.ofNat n => n
    | Int.negSucc a => 0) =
    2 ^ w - 1 - n % 2 ^ w

Tactic:
rw [Int.ofNat_eq_coe, Int.negSucc_emod] at h

Result:
w n a✝ : Nat
h : ↑(2 ^ w) - 1 - ↑n % ↑(2 ^ w) = ↑a✝
⊢ (match Int.ofNat a✝ with
    | Int.ofNat n => n
    | Int.negSucc a => 0) =
    2 ^ w - 1 - n % 2 ^ w

case bpos
w n a✝ : Nat
h : Int.negSucc n % ↑(2 ^ w) = ↑a✝
⊢ 0 < ↑(2 ^ w)

Proof state:
case negSucc
w n a✝ : Nat
h : Int.negSucc n % ↑(2 ^ w) = Int.negSucc a✝
⊢ (match Int.negSucc a✝ with
    | Int.ofNat n => n
    | Int.negSucc a => 0) =
    2 ^ w - 1 - n % 2 ^ w

Tactic:
case negSucc a =>
  have neg := Int.negSucc_lt_zero a
  have _ : 0 ≤ Int.negSucc n % ((2 ^ w : Nat) : Int) := Int.emod_nonneg _ (by omega)
  omega

Result:
no goals

Proof state:
w n a : Nat
h : Int.negSucc n % ↑(2 ^ w) = Int.negSucc a
⊢ (match Int.negSucc a with
    | Int.ofNat n => n
    | Int.negSucc a => 0) =
    2 ^ w - 1 - n % 2 ^ w

Tactic:
have neg := Int.negSucc_lt_zero a

Result:
w n a : Nat
h : Int.negSucc n % ↑(2 ^ w) = Int.negSucc a
neg : Int.negSucc a < 0
⊢ (match Int.negSucc a with
    | Int.ofNat n => n
    | Int.negSucc a => 0) =
    2 ^ w - 1 - n % 2 ^ w

Proof state:
w n a : Nat
h : Int.negSucc n % ↑(2 ^ w) = Int.negSucc a
neg : Int.negSucc a < 0
x✝ : 0 ≤ Int.negSucc n % ↑(2 ^ w)
⊢ (match Int.negSucc a with
    | Int.ofNat n => n
    | Int.negSucc a => 0) =
    2 ^ w - 1 - n % 2 ^ w

Tactic:
omega

Result:
no goals

Proof state:
w n a : Nat
h : Int.negSucc n % ↑(2 ^ w) = Int.negSucc a
neg : Int.negSucc a < 0
⊢ (match Int.negSucc a with
    | Int.ofNat n => n
    | Int.negSucc a => 0) =
    2 ^ w - 1 - n % 2 ^ w

Tactic:
have _ : 0 ≤ Int.negSucc n % ((2 ^ w : Nat) : Int) := Int.emod_nonneg _ (by omega)

Result:
w n a : Nat
h : Int.negSucc n % ↑(2 ^ w) = Int.negSucc a
neg : Int.negSucc a < 0
x✝ : 0 ≤ Int.negSucc n % ↑(2 ^ w)
⊢ (match Int.negSucc a with
    | Int.ofNat n => n
    | Int.negSucc a => 0) =
    2 ^ w - 1 - n % 2 ^ w

Proof state:
w n : Nat
⊢ (match Int.negSucc n % ↑(2 ^ w) with
    | Int.ofNat n => n
    | Int.negSucc a => 0) =
    2 ^ w - 1 - n % 2 ^ w

Tactic:
cases h : Int.negSucc n % ((2 ^ w : Nat) : Int)

Result:
case ofNat
w n a✝ : Nat
h : Int.negSucc n % ↑(2 ^ w) = Int.ofNat a✝
⊢ (match Int.ofNat a✝ with
    | Int.ofNat n => n
    | Int.negSucc a => 0) =
    2 ^ w - 1 - n % 2 ^ w

case negSucc
w n a✝ : Nat
h : Int.negSucc n % ↑(2 ^ w) = Int.negSucc a✝
⊢ (match Int.negSucc a✝ with
    | Int.ofNat n => n
    | Int.negSucc a => 0) =
    2 ^ w - 1 - n % 2 ^ w

Proof state:
w n a : Nat
h : Int.negSucc n % ↑(2 ^ w) = Int.negSucc a
neg : Int.negSucc a < 0
⊢ ↑(2 ^ w) ≠ 0

Tactic:
omega

Result:
no goals

Proof state:
w n : Nat
⊢ BitVec.ofInt w (Int.negSucc n) = ~~~BitVec.ofNat w n

Tactic:
simp only [BitVec.ofInt, Int.toNat, Int.ofNat_eq_coe, toNat_eq, toNat_ofNatLt, toNat_not,
  toNat_ofNat]

Result:
w n : Nat
⊢ (match Int.negSucc n % ↑(2 ^ w) with
    | Int.ofNat n => n
    | Int.negSucc a => 0) =
    2 ^ w - 1 - n % 2 ^ w

Proof state:
w n a✝ : Nat
h : ↑(2 ^ w) - 1 - ↑n % ↑(2 ^ w) = ↑a✝
⊢ (match Int.ofNat a✝ with
    | Int.ofNat n => n
    | Int.negSucc a => 0) =
    2 ^ w - 1 - n % 2 ^ w

Tactic:
dsimp only

Result:
w n a✝ : Nat
h : ↑(2 ^ w) - 1 - ↑n % ↑(2 ^ w) = ↑a✝
⊢ a✝ = 2 ^ w - 1 - n % 2 ^ w

Proof state:
case bpos
w n a✝ : Nat
h : Int.negSucc n % ↑(2 ^ w) = ↑a✝
⊢ 0 < ↑(2 ^ w)

Tactic:
omega

Result:
no goals