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

State before:
sz : ℕ
⊢ sz > 0 → toUint one = 1
Tactic:
intros h
State after:
sz : ℕ
h : sz > 0
⊢ toUint one = 1

State before:
sz : ℕ
h : sz > 0
⊢ toUint one = 1
Tactic:
induction sz with
| zero => cases (by decide: ¬ 0 > 0) h
| succ n ih => cases n; decide; simp [toUint]; apply ih; simp_arith
State after:
no goals

State before:
case zero
h : Nat.zero > 0
⊢ toUint one = 1
Tactic:
cases (by decide: ¬ 0 > 0) h
State after:
no goals

State before:
h : Nat.zero > 0
⊢ ¬0 > 0
Tactic:
decide
State after:
no goals

State before:
case succ
n : ℕ
ih : n > 0 → toUint one = 1
h : Nat.succ n > 0
⊢ toUint one = 1
Tactic:
cases n
State after:
case succ.zero
ih : Nat.zero > 0 → toUint one = 1
h : Nat.succ Nat.zero > 0
⊢ toUint one = 1

case succ.succ
n✝ : ℕ
ih : Nat.succ n✝ > 0 → toUint one = 1
h : Nat.succ (Nat.succ n✝) > 0
⊢ toUint one = 1

State before:
case succ.zero
ih : Nat.zero > 0 → toUint one = 1
h : Nat.succ Nat.zero > 0
⊢ toUint one = 1

case succ.succ
n✝ : ℕ
ih : Nat.succ n✝ > 0 → toUint one = 1
h : Nat.succ (Nat.succ n✝) > 0
⊢ toUint one = 1
Tactic:
decide
State after:
case succ.succ
n✝ : ℕ
ih : Nat.succ n✝ > 0 → toUint one = 1
h : Nat.succ (Nat.succ n✝) > 0
⊢ toUint one = 1

State before:
case succ.succ
n✝ : ℕ
ih : Nat.succ n✝ > 0 → toUint one = 1
h : Nat.succ (Nat.succ n✝) > 0
⊢ toUint one = 1
Tactic:
apply ih
State after:
case succ.succ
n✝ : ℕ
ih : Nat.succ n✝ > 0 → toUint one = 1
h : Nat.succ (Nat.succ n✝) > 0
⊢ Nat.succ n✝ > 0

State before:
case succ.succ
n✝ : ℕ
ih : Nat.succ n✝ > 0 → toUint one = 1
h : Nat.succ (Nat.succ n✝) > 0
⊢ Nat.succ n✝ > 0
Tactic:
simp_arith
State after:
no goals