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

State before:
sz : ℕ
n : FinInt sz
⊢ toUint n < 2 ^ sz
Tactic:
revert n
State after:
sz : ℕ
⊢ ∀ {n : FinInt sz}, toUint n < 2 ^ sz

State before:
sz : ℕ
⊢ ∀ {n : FinInt sz}, toUint n < 2 ^ sz
Tactic:
induction sz <;> intros n <;> cases n <;> simp
State after:
case succ.next
n✝ : ℕ
a✝¹ : Bool
a✝ : FinInt n✝
n_ih✝ : ∀ {n : FinInt (Nat.add n✝ 0)}, toUint n < 2 ^ Nat.add n✝ 0
⊢ toUint (next a✝¹ a✝) < 2 ^ Nat.succ n✝

State before:
case succ.next
n✝ : ℕ
a✝¹ : Bool
a✝ : FinInt n✝
n_ih✝ : ∀ {n : FinInt (Nat.add n✝ 0)}, toUint n < 2 ^ Nat.add n✝ 0
⊢ toUint (next a✝¹ a✝) < 2 ^ Nat.succ n✝
Tactic:
sorry
State after:
no goals