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

State before:
sz : ℕ
⊢ toUint zero = 0
Tactic:
induction sz with
| zero => decide
| succ n ih => simp [toUint, ih]
State after:
no goals

State before:
case zero

⊢ toUint zero = 0
Tactic:
decide
State after:
no goals

State before:
case succ
n : ℕ
ih : toUint zero = 0
⊢ toUint zero = 0
Tactic:
simp [toUint, ih]
State after:
no goals