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

State before:
sz : ℕ
n : FinInt (sz + 1)
⊢ toSint n < 2 ^ sz
Tactic:
cases n
State after:
case next
sz : ℕ
a✝¹ : Bool
a✝ : FinInt sz
⊢ toSint (next a✝¹ a✝) < 2 ^ sz

State before:
sz : ℕ
bn : Bool
n' : FinInt sz
⊢ toSint (next bn n') < 2 ^ sz
Tactic:
case next bn n' =>
cases bn <;> simp [toSint]
. apply toUint_lt
. sorry_arith
State after:
no goals

State before:
sz : ℕ
bn : Bool
n' : FinInt sz
⊢ toSint (next bn n') < 2 ^ sz
Tactic:
cases bn <;> simp [toSint]
State after:
case false
sz : ℕ
n' : FinInt sz
⊢ toUint n' < 2 ^ sz

case true
sz : ℕ
n' : FinInt sz
⊢ toUint n' - 2 ^ sz < 2 ^ sz

State before:
case false
sz : ℕ
n' : FinInt sz
⊢ toUint n' < 2 ^ sz

case true
sz : ℕ
n' : FinInt sz
⊢ toUint n' - 2 ^ sz < 2 ^ sz
Tactic:
. apply toUint_lt
State after:
case true
sz : ℕ
n' : FinInt sz
⊢ toUint n' - 2 ^ sz < 2 ^ sz

State before:
case true
sz : ℕ
n' : FinInt sz
⊢ toUint n' - 2 ^ sz < 2 ^ sz
Tactic:
. sorry_arith
State after:
no goals