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

State before:
c : ASCII.Char
n : Nat
hn : n < 128
⊢ c.toNat = n ↔ ofNat n = c
Tactic:
rw [ofNat, dif_pos hn]
State after:
c : ASCII.Char
n : Nat
hn : n < 128
⊢ c.toNat = n ↔ ofNatAux n hn = c

State before:
c : ASCII.Char
n : Nat
hn : n < 128
⊢ c.toNat = n ↔ ofNatAux n hn = c
Tactic:
exact toNat_eq_iff_ofNatAux_eq ..
State after:
no goals