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

State before:
sz : ℕ
n : FinInt sz
⊢ toUint n ≥ 0
Tactic:
revert n
State after:
sz : ℕ
⊢ ∀ {n : FinInt sz}, toUint n ≥ 0

State before:
sz : ℕ
⊢ ∀ {n : FinInt sz}, toUint n ≥ 0
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 ≥ 0
⊢ 0 ≤ toUint (next a✝¹ a✝)

State before:
sz : ℕ
bn : Bool
n' : FinInt sz
ih : ∀ {n : FinInt (Nat.add sz 0)}, toUint n ≥ 0
⊢ 0 ≤ toUint (next bn n')
Tactic:
case next sz bn n' ih =>
  cases bn <;> simp [@ih n']
  apply Int.add_ge_zero; apply Int.pow_ge_zero; decide; apply ih
State after:
no goals

State before:
sz : ℕ
bn : Bool
n' : FinInt sz
ih : ∀ {n : FinInt (Nat.add sz 0)}, toUint n ≥ 0
⊢ 0 ≤ toUint (next bn n')
Tactic:
cases bn <;> simp [@ih n']
State after:
case true
sz : ℕ
n' : FinInt sz
ih : ∀ {n : FinInt (Nat.add sz 0)}, toUint n ≥ 0
⊢ 0 ≤ 2 ^ sz + toUint n'

State before:
case true
sz : ℕ
n' : FinInt sz
ih : ∀ {n : FinInt (Nat.add sz 0)}, toUint n ≥ 0
⊢ 0 ≤ 2 ^ sz + toUint n'
Tactic:
apply Int.add_ge_zero
State after:
case true.a
sz : ℕ
n' : FinInt sz
ih : ∀ {n : FinInt (Nat.add sz 0)}, toUint n ≥ 0
⊢ 2 ^ sz ≥ 0

case true.a
sz : ℕ
n' : FinInt sz
ih : ∀ {n : FinInt (Nat.add sz 0)}, toUint n ≥ 0
⊢ toUint n' ≥ 0

State before:
case true.a
sz : ℕ
n' : FinInt sz
ih : ∀ {n : FinInt (Nat.add sz 0)}, toUint n ≥ 0
⊢ 2 ^ sz ≥ 0

case true.a
sz : ℕ
n' : FinInt sz
ih : ∀ {n : FinInt (Nat.add sz 0)}, toUint n ≥ 0
⊢ toUint n' ≥ 0
Tactic:
apply Int.pow_ge_zero
State after:
case true.a.a
sz : ℕ
n' : FinInt sz
ih : ∀ {n : FinInt (Nat.add sz 0)}, toUint n ≥ 0
⊢ 2 ≥ 0

case true.a
sz : ℕ
n' : FinInt sz
ih : ∀ {n : FinInt (Nat.add sz 0)}, toUint n ≥ 0
⊢ toUint n' ≥ 0

State before:
case true.a.a
sz : ℕ
n' : FinInt sz
ih : ∀ {n : FinInt (Nat.add sz 0)}, toUint n ≥ 0
⊢ 2 ≥ 0

case true.a
sz : ℕ
n' : FinInt sz
ih : ∀ {n : FinInt (Nat.add sz 0)}, toUint n ≥ 0
⊢ toUint n' ≥ 0
Tactic:
decide
State after:
case true.a
sz : ℕ
n' : FinInt sz
ih : ∀ {n : FinInt (Nat.add sz 0)}, toUint n ≥ 0
⊢ toUint n' ≥ 0

State before:
case true.a
sz : ℕ
n' : FinInt sz
ih : ∀ {n : FinInt (Nat.add sz 0)}, toUint n ≥ 0
⊢ toUint n' ≥ 0
Tactic:
apply ih
State after:
no goals