c : Char
cs : List Char
b e : Pos
⊢ (if e.byteIdx ≤ b.byteIdx then "" else { data := extract.go₁ (c :: cs) 0 (b + c) (e + c) }) =
    if b.byteIdx ≥ e.byteIdx then "" else { data := extract.go₁ cs 0 b e }
c : Char
cs : List Char
b e : Pos
⊢ extract { data := c :: cs } (b + c) (e + c) = extract { data := cs } b e
simp [extract, Nat.add_le_add_iff_le_right]
no goals
c : Char
cs : List Char
b e : Pos
⊢ (if e.byteIdx ≤ b.byteIdx then "" else { data := extract.go₁ (c :: cs) 0 (b + c) (e + c) }) =
    if b.byteIdx ≥ e.byteIdx then "" else { data := extract.go₁ cs 0 b e }
split <;> [rfl; rw [extract.go₁_cons_addChar]]