n : ℕ
h : n < size
⊢ Nat.isValidChar n

n : ℕ
h : n < size
⊢ n < UInt32.size
n : ℕ
h : n < size
⊢ Nat.isValidChar ↑(UInt32.ofNat n).val
rw [UInt32.val_eq_of_lt]
n : ℕ
h : n < size
⊢ n < UInt32.size
n : ℕ
h : n < size
⊢ Nat.isValidChar n

n : ℕ
h : n < size
⊢ n < UInt32.size
exact Or.inl $ Nat.lt_trans h $ by decide
no goals
n : ℕ
h : n < size
⊢ n < UInt32.size
exact Nat.lt_trans h $ by decide
no goals
n : ℕ
h : n < size
⊢ size < 55296
decide
no goals
n : ℕ
h : n < size
⊢ size < UInt32.size
decide