Theorem: toChar_aux (Metamath/Verify.lean)

State before:
n : Nat
h : n < UInt8.size
⊢ Nat.isValidChar (UInt32.ofNat n).val.val
Tactic:
rw [UInt32.val_eq_of_lt]
State after:
n : Nat
h : n < UInt8.size
⊢ Nat.isValidChar n

n : Nat
h : n < UInt8.size
⊢ n < UInt32.size

State before:
n : Nat
h : n < UInt8.size
⊢ Nat.isValidChar n

n : Nat
h : n < UInt8.size
⊢ n < UInt32.size
Tactic:
exact Or.inl (Nat.lt_trans h (by decide))
State after:
n : Nat
h : n < UInt8.size
⊢ n < UInt32.size

State before:
n : Nat
h : n < UInt8.size
⊢ n < UInt32.size
Tactic:
exact Nat.lt_trans h (by decide)
State after:
no goals

State before:
n : Nat
h : n < UInt8.size
⊢ UInt8.size < 55296
Tactic:
decide
State after:
no goals

State before:
n : Nat
h : n < UInt8.size
⊢ UInt8.size < UInt32.size
Tactic:
decide
State after:
no goals