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

State before:
c : ASCII.Char
⊢ ofNatAux c.toNat ⋯ = c
Tactic:
rw [← toNat_eq_iff_ofNatAux_eq]
State after:
no goals