Theorem: ASCII.Char.toUnicode_isASCII (ASCII/Char.lean)

State before:
c : ASCII.Char
⊢ Char.isASCII ↑c = true
Tactic:
simp [Char.toUnicode, Char.isASCII, _root_.Char.toNat]
State after:
c : ASCII.Char
⊢ c.toByte.toNat < 128

State before:
c : ASCII.Char
⊢ c.toByte.toNat < 128
Tactic:
exact c.valid
State after:
no goals