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

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

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