Theorem: FinInt.toSint_of_toUint (MLIR/Util/FinInt.lean)

State before:
sz : ℕ
n : FinInt (sz + 1)
⊢ toSint n =
    match n with
    | next false a => toUint n
    | next true a => toUint n - 2 ^ (sz + 1)
Tactic:
match n with
| .O m => simp [toSint, toUint]
| .I m => simp [toSint, toUint]; sorry_arith
State after:
no goals

State before:
sz : ℕ
n : FinInt (sz + 1)
m : FinInt sz
⊢ toSint (O m) =
    match O m with
    | next false a => toUint (O m)
    | next true a => toUint (O m) - 2 ^ (sz + 1)
Tactic:
simp [toSint, toUint]
State after:
no goals

State before:
sz : ℕ
n : FinInt (sz + 1)
m : FinInt sz
⊢ toSint (I m) =
    match I m with
    | next false a => toUint (I m)
    | next true a => toUint (I m) - 2 ^ (sz + 1)
Tactic:
simp [toSint, toUint]
State after:
sz : ℕ
n : FinInt (sz + 1)
m : FinInt sz
⊢ toUint m - 2 ^ sz = 2 ^ sz + toUint m - 2 ^ (sz + 1)

State before:
sz : ℕ
n : FinInt (sz + 1)
m : FinInt sz
⊢ toUint m - 2 ^ sz = 2 ^ sz + toUint m - 2 ^ (sz + 1)
Tactic:
sorry_arith
State after:
no goals