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

State before:
s : ASCII.String
c : ASCII.Char
⊢ (s.push c)[s.length] = c
Tactic:
ext
State after:
case a.a
s : ASCII.String
c : ASCII.Char
⊢ (s.push c)[s.length].toByte.toNat = c.toByte.toNat

State before:
case a.a
s : ASCII.String
c : ASCII.Char
⊢ (s.push c)[s.length].toByte.toNat = c.toByte.toNat
Tactic:
simp
State after:
no goals