l m r : List Char
⊢ (if utf8Len l ≥ utf8Len l + utf8Len m then ""
    else { data := extract.go₁ (l ++ m ++ r) 0 { byteIdx := utf8Len l } { byteIdx := utf8Len l + utf8Len m } }) =
    { data := m }
l m r : List Char
⊢ extract { data := l ++ m ++ r } { byteIdx := utf8Len l } { byteIdx := utf8Len l + utf8Len m } = { data := m }
simp only [extract]
case inl
l m r : List Char
h✝ : utf8Len l ≥ utf8Len l + utf8Len m
⊢ "" = { data := m }

case inr
l m r : List Char
h✝ : ¬utf8Len l ≥ utf8Len l + utf8Len m
⊢ { data := extract.go₁ (l ++ m ++ r) 0 { byteIdx := utf8Len l } { byteIdx := utf8Len l + utf8Len m } } = { data := m }
l m r : List Char
⊢ (if utf8Len l ≥ utf8Len l + utf8Len m then ""
    else { data := extract.go₁ (l ++ m ++ r) 0 { byteIdx := utf8Len l } { byteIdx := utf8Len l + utf8Len m } }) =
    { data := m }
split
no goals
case inl
l m r : List Char
h✝ : utf8Len l ≥ utf8Len l + utf8Len m
⊢ "" = { data := m }
next h => rw [utf8Len_eq_zero.1 <| Nat.le_zero.1 <| (Nat.add_le_add_iff_le_left _ _ 0).1 h]
no goals
l m r : List Char
h : utf8Len l ≥ utf8Len l + utf8Len m
⊢ "" = { data := m }
rw [utf8Len_eq_zero.1 <| Nat.le_zero.1 <| (Nat.add_le_add_iff_le_left _ _ 0).1 h]
case inr.e_data
l m r : List Char
h✝ : ¬utf8Len l ≥ utf8Len l + utf8Len m
⊢ extract.go₁ (l ++ m ++ r) 0 { byteIdx := utf8Len l } { byteIdx := utf8Len l + utf8Len m } = m
case inr
l m r : List Char
h✝ : ¬utf8Len l ≥ utf8Len l + utf8Len m
⊢ { data := extract.go₁ (l ++ m ++ r) 0 { byteIdx := utf8Len l } { byteIdx := utf8Len l + utf8Len m } } = { data := m }
congr
case inr.e_data
l m r : List Char
h✝ : ¬utf8Len l ≥ utf8Len l + utf8Len m
⊢ extract.go₂ (m ++ r) { byteIdx := utf8Len l } { byteIdx := utf8Len l + utf8Len m } = m
case inr.e_data
l m r : List Char
h✝ : ¬utf8Len l ≥ utf8Len l + utf8Len m
⊢ extract.go₁ (l ++ m ++ r) 0 { byteIdx := utf8Len l } { byteIdx := utf8Len l + utf8Len m } = m
rw [List.append_assoc, extract.go₁_append_right _ _ _ _ _ (by rfl)]
case inr.e_data.a
l m r : List Char
h✝ : ¬utf8Len l ≥ utf8Len l + utf8Len m
⊢ utf8Len l + utf8Len m = utf8Len m + utf8Len l
case inr.e_data
l m r : List Char
h✝ : ¬utf8Len l ≥ utf8Len l + utf8Len m
⊢ extract.go₂ (m ++ r) { byteIdx := utf8Len l } { byteIdx := utf8Len l + utf8Len m } = m
apply extract.go₂_append_left
no goals
case inr.e_data.a
l m r : List Char
h✝ : ¬utf8Len l ≥ utf8Len l + utf8Len m
⊢ utf8Len l + utf8Len m = utf8Len m + utf8Len l
apply Nat.add_comm
no goals
l m r : List Char
h✝ : ¬utf8Len l ≥ utf8Len l + utf8Len m
⊢ utf8Len l = utf8Len l + 0.byteIdx
rfl