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

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