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

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

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

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