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

State before:
s : ASCII.String
c : ASCII.Char
i : Nat
h : i < s.length
h' : optParam (i < (s.push c).length) ⋯
⊢ (s.push c)[i] = s[i]
Tactic:
ext
State after:
case a.a
s : ASCII.String
c : ASCII.Char
i : Nat
h : i < s.length
h' : optParam (i < (s.push c).length) ⋯
⊢ (s.push c)[i].toByte.toNat = s[i].toByte.toNat

State before:
case a.a
s : ASCII.String
c : ASCII.Char
i : Nat
h : i < s.length
h' : optParam (i < (s.push c).length) ⋯
⊢ (s.push c)[i].toByte.toNat = s[i].toByte.toNat
Tactic:
simp [ByteArray.get_push_lt, h]
State after:
no goals