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

State before:
sz : ℕ
⊢ toUint minusOne = 2 ^ sz - 1
Tactic:
induction sz with
| zero => decide
| succ n ih => simp [toUint, ih]; sorry_arith
State after:
no goals

State before:
case zero

⊢ toUint minusOne = 2 ^ Nat.zero - 1
Tactic:
decide
State after:
no goals

State before:
case succ
n : ℕ
ih : toUint minusOne = 2 ^ n - 1
⊢ toUint minusOne = 2 ^ Nat.succ n - 1
Tactic:
simp [toUint, ih]
State after:
case succ
n : ℕ
ih : toUint minusOne = 2 ^ n - 1
⊢ 2 ^ n + (2 ^ n - 1) = 2 ^ Nat.succ n - 1

State before:
case succ
n : ℕ
ih : toUint minusOne = 2 ^ n - 1
⊢ 2 ^ n + (2 ^ n - 1) = 2 ^ Nat.succ n - 1
Tactic:
sorry_arith
State after:
no goals