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

State before:
s t : ASCII.String
i : Nat
hlt : i < s.length
h : optParam (i < (s ++ t).length) ⋯
⊢ (s ++ t)[i] = s[i]
Tactic:
ext
State after:
case a.a
s t : ASCII.String
i : Nat
hlt : i < s.length
h : optParam (i < (s ++ t).length) ⋯
⊢ (s ++ t)[i].toByte.toNat = s[i].toByte.toNat

State before:
case a.a
s t : ASCII.String
i : Nat
hlt : i < s.length
h : optParam (i < (s ++ t).length) ⋯
⊢ (s ++ t)[i].toByte.toNat = s[i].toByte.toNat
Tactic:
simp [ByteArray.get_append_left hlt]
State after:
no goals