Theorem: ASCII.Char.ofUnicode?_eq_ofUnicode (ASCII/Lemmas.lean)

State before:
u : Unicode.Char
hu : Char.isASCII u = true
⊢ ofUnicode? u = some (ofUnicode u hu)
Tactic:
simp [ofUnicode?, dif_pos hu]
State after:
no goals