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

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

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