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

State before:
n : Nat
hn : n < 128
⊢ (ofNatAux n hn).toNat = n
Tactic:
rw [toNat_eq_iff_ofNatAux_eq]
State after:
no goals