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

State before:
u : Unicode.Char
hu : Char.isASCII u = true
⊢ ↑(ofUnicode u hu) = u
Tactic:
rw [toUnicode_eq_iff_ofUnicode_eq]
State after:
no goals