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

State before:
s t : ASCII.String
c : ASCII.Char
⊢ s ++ t.push c = (s ++ t).push c
Tactic:
ext
State after:
case a.a
s t : ASCII.String
c : ASCII.Char
⊢ (s ++ t.push c).toByteArray.data = ((s ++ t).push c).toByteArray.data

State before:
case a.a
s t : ASCII.String
c : ASCII.Char
⊢ (s ++ t.push c).toByteArray.data = ((s ++ t).push c).toByteArray.data
Tactic:
simp [Array.push_eq_append_singleton, Array.append_assoc]
State after:
no goals