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

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

State before:
case a.a
i : Nat
s : ASCII.String
start stop : Nat
h : i < (s.extract start stop).length
h' : optParam (start + i < s.length) ⋯
⊢ (s.extract start stop)[i].toByte.toNat = s[start + i].toByte.toNat
Tactic:
simp
State after:
no goals