[GOAL]
⊢ size ≠ 0
[PROOFSTEP]
decide
[GOAL]
⊢ size ≠ 0
[PROOFSTEP]
decide
[GOAL]
⊢ size ≠ 0
[PROOFSTEP]
decide
[GOAL]
⊢ size ≠ 0
[PROOFSTEP]
decide
[GOAL]
n : ℕ
h : n < size
⊢ Nat.isValidChar ↑(UInt32.ofNat n).val
[PROOFSTEP]
rw [UInt32.val_eq_of_lt]
[GOAL]
n : ℕ
h : n < size
⊢ Nat.isValidChar n
n : ℕ h : n < size ⊢ n < UInt32.size
[PROOFSTEP]
exact Or.inl $ Nat.lt_trans h $ by decide
[GOAL]
n : ℕ
h : n < size
⊢ size < 55296
[PROOFSTEP]
decide
[GOAL]
n : ℕ
h : n < size
⊢ n < UInt32.size
[PROOFSTEP]
exact Nat.lt_trans h $ by decide
[GOAL]
n : ℕ
h : n < size
⊢ size < UInt32.size
[PROOFSTEP]
decide
