Theorem: ASCII.Char.ofNat_toNat (ASCII/Lemmas.lean)

State before:
c : ASCII.Char
⊢ ofNat c.toNat = c
Tactic:
rw [← toNat_eq_iff_ofNat_eq]
State after:
case hn
c : ASCII.Char
⊢ c.toNat < 128

State before:
case hn
c : ASCII.Char
⊢ c.toNat < 128
Tactic:
exact c.toNat_lt
State after:
no goals