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

State before:
n : Nat
hn : n < 128
⊢ (ofNat n).toNat = n
Tactic:
rw [toNat_eq_iff_ofNat_eq]
State after:
case hn
n : Nat
hn : n < 128
⊢ n < 128

State before:
case hn
n : Nat
hn : n < 128
⊢ n < 128
Tactic:
exact hn
State after:
no goals