Theorem: ASCII.String.nil_append (ASCII/Lemmas.lean)

State before:
t : ASCII.String
⊢ "".toASCII ⋯ ++ t = t
Tactic:
ext
State after:
case a.a
t : ASCII.String
⊢ ("".toASCII ⋯ ++ t).toByteArray.data = t.toByteArray.data

State before:
case a.a
t : ASCII.String
⊢ ("".toASCII ⋯ ++ t).toByteArray.data = t.toByteArray.data
Tactic:
simp
State after:
no goals